Title
Correctness of Concurrent Objects 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.
Year
DOI
Venue
2018
10.4204/EPTCS.282.5
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE
Field
DocType
Volume
Programming language,Computer science,Correctness,Theoretical computer science,Memory model,Semantics
Journal
abs/1810.09612
Issue
ISSN
Citations 
282
2075-2180
0
PageRank 
References 
Authors
0.34
5
3
Name
Order
Citations
PageRank
Graeme Smith134834.02
Kirsten Winter2132.06
Robert Colvin3688.67