A Generic Formalised Framework for Reasoning About Weak Memory Models

Jade Alglave (1, 2) , Assia Mahboubi (3, 4, 5)

1 MOSCOVA - Mobililty, security, concurrence, verification and analysis
2 OUCL - Computing Laboratory
3 MSR - INRIA - Microsoft Research - Inria Joint Centre
4 TYPICAL - Types, Logic and computing
5 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]

This paper describes Coq libraries devoted to the semantic of relaxed memory models. These libraries formalise a framework which covers a large class of industrial models. Implementing this framework inside a proof assistant has significantly helped improving its design and crafting the most concise and relevant specifications. Similarly the use of a proof assistant has been instrumental in the study of the semantic of synchronisation primitives, which we illustrate by the formal proof of a barrier placement theorem. We explain the choices we made to re-design our Coq libraries, and in particular what we gained from adopting a small-scale reflection methodology.

Domaines: Logique en informatique [cs.LO]

Jade Alglave, Assia Mahboubi. A Generic Formalised Framework for Reasoning About Weak Memory Models. 2011. ⟨inria-00604656⟩