Correctness of Concurrent Objects under Weak Memory Models

Graeme Smith
Kirsten Winter
Robert J. Colvin

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.

In John Derrick, Brijesh Dongol and Steve Reeves: Proceedings 18th Refinement Workshop (Refine 2018), Oxford, UK, 18th July 2018, Electronic Proceedings in Theoretical Computer Science 282, pp. 53–67.
Published: 24th October 2018.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: