Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

A Generic Formalised Framework for Reasoning About Weak Memory Models

Abstract : 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.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [21 references]  Display  Hide  Download
Contributor : Assia Mahboubi Connect in order to contact the contributor
Submitted on : Wednesday, June 29, 2011 - 2:31:55 PM
Last modification on : Tuesday, January 11, 2022 - 11:16:20 AM
Long-term archiving on: : Monday, November 12, 2012 - 9:46:59 AM


Files produced by the author(s)


  • HAL Id : inria-00604656, version 1



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



Les métriques sont temporairement indisponibles