A Generic Formalised Framework for Reasoning About Weak Memory Models - Archive ouverte HAL Access content directly
Preprints, Working Papers, ... Year :

A Generic Formalised Framework for Reasoning About Weak Memory Models

(1, 2) , (3, 4, 5)
1
2
3
4
5

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.
Fichier principal
Vignette du fichier
itp.pdf (189.22 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00604656 , version 1 (29-06-2011)

Identifiers

  • HAL Id : inria-00604656 , version 1

Cite

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

Share

Gmail Facebook Twitter LinkedIn More