Fences and Synchronisation Idioms in Weak Memory Models

Abstract : We present an axiomatic framework, implemented in the Coq proof assistant, to define weak memory models in terms of several parameters: local reorderings of reads and writes, and visibility of inter and intra processor communications through memory, including full store atomicity relaxation. Thereby, we give a formal hierarchy of weak memory models, in which we provide a formal study of what should be the action and placement of fences to restore a given model such as SC from a weaker one. Finally, we provide formal requirements for abstract locks that guarantee SC semantics to data race free programs, and show that a particular implementation of locks matches these requirements.
Complete list of metadatas

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/inria-00440863
Contributor : Alglave Jade <>
Submitted on : Saturday, December 12, 2009 - 5:53:01 PM
Last modification on : Friday, May 25, 2018 - 12:02:03 PM
Long-term archiving on : Thursday, June 17, 2010 - 11:37:37 PM

File

rr-7152.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00440863, version 1

Collections

Citation

Jade Alglave, Luc Maranget. Fences and Synchronisation Idioms in Weak Memory Models. [Research Report] RR-7152, INRIA. 2009. ⟨inria-00440863⟩

Share

Metrics

Record views

169

Files downloads

113