Paper Info
Title
A formal hierarchy of weak memory models
Abstract
We present in this paper a formal generic framework, implemented in the Coq proof assistant, for defining and reasoning about weak memory models. We first present the three axioms of our framework, with several examples as illustration and justification. Then we show how to implement several existing weak memory models in our framework, and prove formally that our implementation is equivalent to the native definition for each of these models.
Year
DOI
Venue
2012
10.1007/s10703-012-0161-5
Formal Methods in System Design
Keywords
Field
DocType
Weak memory models,Semantics,Formal proofs
Computer science,Axiom,Theoretical computer science,Hierarchy,Semantics,Proof assistant
Journal
Volume
Issue
ISSN
41
2
0925-9856
Citations 
PageRank 
References 
21
0.79
21
Authors
1
Name
Order
Citations
PageRank
Jade Alglave160826.53