A framework for correctness criteria on weak memory models

Derrick, John and Smith, Graeme (2015). A framework for correctness criteria on weak memory models. In: Nikolaj Bjørner and Frank de Boer, FM 2015: Formal Methods. 20th International Symposium on Formal Methods, FM 2015, Oslo, Norway, (178-194). 25-26 June 2015. doi:10.1007/978-3-319-19249-9_12

Author Derrick, John
Smith, Graeme
Title of paper A framework for correctness criteria on weak memory models
Conference name 20th International Symposium on Formal Methods, FM 2015
Conference location Oslo, Norway
Conference dates 25-26 June 2015
Convener Einar Broch Johnsen
Proceedings title FM 2015: Formal Methods   Check publisher's open access policy
Journal name Lecture Notes in Computer Science   Check publisher's open access policy
Series Lecture Notes in Computer Science
Place of Publication Heidelberg, Germany
Publisher Springer
Publication Year 2015
Year available 2015
Sub-type Fully published paper
DOI 10.1007/978-3-319-19249-9_12
Open Access Status Not yet assessed
ISBN 9783319192482
ISSN 1611-3349
Editor Nikolaj Bjørner
Frank de Boer
Volume 9109
Start page 178
End page 194
Total pages 17
Chapter number 12
Total chapters 44
Collection year 2016
Language eng
Abstract/Summary The implementation of weak (or relaxed) memory models is standard practice in modern multiprocessor hardware. For efficiency, these memory models allow operations to take effect in shared memory in a different order from that which they occur in a program. A number of correctness criteria have been proposed for concurrent objects operating on such memory models, each reflecting different constraints on the objects which can be proved correct. In this paper, we provide a framework in which correctness criteria are defined in terms of two components: the first defining the particular criterion (as it would be defined in the absence of a weak memory model), and the second defining the particular weak memory model. The framework facilitates the definition and comparison of correctness criteria, and encourages reuse of existing definitions. The latter enables properties of the criteria to be proved using existing proofs. We illustrate the framework via the definition of correctness criteria on the TSO (Total Store Order) weak memory model.
Q-Index Code C1
Q-Index Status Confirmed Code
Institutional Status UQ

Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 0 times in Thomson Reuters Web of Science Article
Scopus Citation Count Cited 0 times in Scopus Article
Google Scholar Search Google Scholar
Created: Tue, 11 Aug 2015, 02:53:30 EST by System User on behalf of School of Information Technol and Elec Engineering