Correctness of Concurrent Objects under Weak Memory Models

TL;DR

This paper develops a generic theory for the correctness of concurrent objects under weak memory models, focusing on observations that determine when effects become visible, and introduces object refinement as a foundational correctness notion.

Contribution

It introduces a parameterized theory of correctness for concurrent objects under weak memory models based on observations and object refinement.

Findings

Defines a generic correctness notion called object refinement.

Enforces minimal constraints on observations and object semantics.

Provides a foundation for sound and complete proof methods under weak memory models.

Abstract

In this paper we develop a theory for correctness of concurrent objects under weak memory models. Central to our definitions is the concept of observations which determine when effects of operations become visible, and hence determine the semantics of objects, under a given memory model. The resulting notion of correctness, called object refinement, is generic as it is parameterised by the memory model under consideration. Our theory enforces the minimal constraints on the placing of observations and on the semantics of objects that underlie object refinement. Object refinement is suitable as a reference for correctness when proving new proof methods for objects under weak memory models to be sound and complete.