Skip to Main content Skip to Navigation

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 metadata

Cited literature [14 references]  Display  Hide  Download
Contributor : Alglave Jade Connect in order to contact the contributor
Submitted on : Saturday, December 12, 2009 - 5:53:01 PM
Last modification on : Thursday, February 3, 2022 - 11:14:18 AM
Long-term archiving on: : Thursday, June 17, 2010 - 11:37:37 PM


Files produced by the author(s)


  • HAL Id : inria-00440863, version 1



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



Record views


Files downloads