Stability in Weak Memory Models
Long version of the paper with proofs, and supplementary tables
Offence
See here for the sources and
documentation of offence, and the experimental details.
Guided tour of the development
We build on a generic framework which embraces Sequential Consistency, SUN TSO, PSO and RMO, Alpha, and Power (see the development).
The whole development (.tar) amounts to 4351
lines of specifications and 8945 lines of proofs. We used Coq version 8.2pl1 (November 2009).
- Library util contains auxiliaries on relations and sets.
- Library wmm contains the generic framework specification.
- Library basic contains basic facts about the objects of the framework.
- Library hierarchy contains the definition of the predicate weaker, and the properties of validity w.r.t weaker.
- Library sc contains our implementation of SC, together with a formal definition of the native one. It contains the proof of their equivalence.
- Library valid shows that a linear extension of any partial order compatible with ppo2 leads to an execution valid on A2.
- Library stable shows that a covering relation ensures stability.
- Library drf contains the DRF guarantee.
- Library racy contains the lock-free guarantee.
- Library locks shows that Power's locks ensure the DRF guarantee.
- Library rmw shows that Power's read-modify-writes coupled with non-cumulative barriers ensure stability.
- Libraries crit and shasha contain our generalisation of D. Shasha and M. Snir critical cycles.
- Library stable contains our characterisation of the stable executions.