Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Wmm

A Formal Hierachy of Weak Memory Models

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.

Sketches of the proofs

We provide the sketches of the proofs to the interested reader, as well as the detail of the diy tool code generation phase.

Guided tour of the development

The whole development (.tar) amounts to 3025 lines of specifications and 7829 lines of proofs. We used Coq version 8.2 (February 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 uniproc contains several statements of the uniproc condition which we show equivalent.

Library hierarchy contains the definition of the predicate weaker, and the properties of validity w.r.t weaker. It contains the generic barriers and weaker barriers guarantees.

Library sc contains our implementation of SC, together with a formal definition of the native one. It contains the proof of their equivalence, the characterisation theorem, and the specification of the SC-restoring barriers with the proof that they restore SC.

Library tso contains our implementation of Sparc TSO, together with a formal definition of the native one. It contains the proof of their equivalence, the characterisation theorem, and the specification of the TSO-restoring barriers with the proof that they restore TSO.

A handy Makefile.