Paper Info
Title
WOMM: a weak operational memory model
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.
Year
DOI
Venue
2010
10.1007/978-3-642-16558-0_43
ISoLA (1)
Keywords
Field
DocType
weak operational memory model,concurrent program,memory model,weak memory model,intuitive sequential consistency semantics,shared memory,hardware memory model,shared memory location,operational semantics,weakly consistent memory,sequential consistency semantics,sequential consistency
Operational semantics,Sequential consistency,Programming language,Shared memory,Computer science,Theoretical computer science,Memory model,Memory management,Memory map,Distributed shared memory,Flat memory model
Conference
Volume
ISSN
ISBN
6415
0302-9743
3-642-16557-5
Citations 
PageRank 
References 
0
0.34
8
Authors
3
Name
Order
Citations
PageRank
Arnab De1271.93
Abhik Roychoudhury22449122.18
Deepak D'souza323917.90