Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-642-16558-0_43
Title: WOMM: A weak operational memory model
Authors: De, A.
Roychoudhury, A. 
D'Souza, D.
Issue Date: 2010
Source: De, A., Roychoudhury, A., D'Souza, D. (2010). WOMM: A weak operational memory model. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 6415 LNCS (PART 1) : 519-534. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-642-16558-0_43
Abstract: Memory models of shared memory concurrent programs define the values a read of a shared memory location is allowed to see. Such memory models are typically weaker than the intuitive sequential consistency semantics to allow efficient execution. In this paper, we present WOMM (abbreviation for Weak Operational Memory Model) that formally unifies two sources of weak behavior in hardware memory models: reordering of instructions and weakly consistent memory. We show that a large number of optimizations are allowed by WOMM. We also show that WOMM is weaker than a number of hardware memory models. Consequently, if a program behaves correctly under WOMM, it will be correct with respect to those hardware memory models. Hence, WOMM can be used as a formally specified abstraction of the hardware memory models. Moreover, unlike most weak memory models, WOMM is described using operational semantics, making it easy to integrate into a model checker for concurrent programs. We further show that WOMM has an important property - it has sequential consistency semantics for datarace-free programs. © 2010 Springer-Verlag.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: http://scholarbank.nus.edu.sg/handle/10635/42045
ISBN: 3642165575
ISSN: 03029743
DOI: 10.1007/978-3-642-16558-0_43
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

1
checked on Dec 14, 2017

Page view(s)

78
checked on Dec 17, 2017

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.