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 metadatas

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/inria-00604656
Contributor : Assia Mahboubi <>
Submitted on : Wednesday, June 29, 2011 - 2:31:55 PM
Last modification on : Wednesday, March 27, 2019 - 4:41:28 PM
Long-term archiving on : Monday, November 12, 2012 - 9:46:59 AM

File

itp.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00604656, version 1

Collections

Citation

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

Share

Metrics

Record views

479

Files downloads

219