Explaining relaxed memory models with program transformations
Version 1.0, released 2016-05-31
Basic properties of relations
Lemmas about cycles
Definition of actions
Lemmas about access types
Memory model definitions
Sequential consistency (SC)
Release-acquire (RA)
Strong release-acquire (SRA)
Total store order (TSO)
Plain executions
Basic properties of the definitions
Results about sequential consistency
Equivalent SC definitions
Results about RA and SRA
Results about TSO
Equivalent TSO definitions
Reducing TSO to SC
Soundness and completeness of write-read reordering
Soundness and completeness of read-after-write elimination
Equivalent TSO definition in terms of transformations
The Power memory model
Power memory model definition
Basic properties of the model
A stronger acyclicity condition
Soundness and completeness of reorderings
Reduction of the Power memory model
This page has been generated by
coqdoc