A Generic Formalised Framework for Reasoning About Weak Memory Models

Jade Alglave 1, 2 Assia Mahboubi 3, 4, 5
4 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR
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.
Type de document :
Pré-publication, Document de travail

Contributeur : Assia Mahboubi <>
Soumis le : mercredi 29 juin 2011 - 14:31:55
Dernière modification le : vendredi 10 février 2017 - 01:12:44
Document(s) archivé(s) le : lundi 12 novembre 2012 - 09:46:59


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00604656, version 1



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



Consultations de
la notice


Téléchargements du document