c11comp : Formalisation of theorems about the C11 memory model

Version 1.0, released 2014-10-28

Definition of C11 actions
- Lemmas about access types
C11 concurrency model definition
Formalisation of opsemsets
- Definition of opsems
- Opsem sets axioms
Properties of execution prefixes
A concurrent WHILE language
Monotonicity
Alternative coherence axioms
"Roach motel" reorderings
Reorderings with respect to fence operations
- read(acquire) ; fence(acquire) → read(acquire) || fence(acquire)
- fence(release) ; write(release) → fence(release) || write(release)
Elimination of redundant memory accesses

This page has been generated by coqdoc