We offer here a formal hierarchy of weak memory models implemented in Coq, which we show how to instantiate to obtain Sequential Consistency (SC) and Sparc Total Store Ordering (TSO). We provide the proofs of equivalences of these instantiations with the native models, as well as characterisation criteria. We show theorems about the strength and placement of memory barriers to regain a strong model from a weaker one.
You will find two different developments on this page.
You will also find a supplementary table of the relations that we use in our papers.
The first development is the one associated to our CAV 2010 paper. It has been been developed in the Coq proof assistant, version 8.2 (February 2009).
Additionally, we provide the sketches of the proofs of the CAV 2010 paper, as well as the detail of the diy tool code generation phase.
The second development is our ongoing rewriting of the first development using the ssreflect library.
This self contained archive is based the ssreflect library and Coq extension (see the INSTALL file).
The theories directory includes some .v files of the 1.3pl1 ssreflect distribution needed for compilation, plus the files extrarel.v, wmm.v, sc.v and hierarchy.v, formalising respectively extra results on boolean relations, the framework for weak memory models, the sequential consistency model, and the barrier theorem.
Here it is.