Skip to Main content Skip to Navigation
New interface
Conference papers

An Extended Buffered Memory Model With Full Reorderings

Gurvan Cabon 1 David Cachera 2 David Pichardie 2 
2 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Modern multicore processor architectures and compilers of shared-memory concurrent programming languages provide only weak memory consistency guarantees. A memory model specifies which write action can be seen by a read action between concurrent threads. The most well known memory model is the sequentially consistent (SC) model but, to improve performance, modern architectures and languages employ relaxed memory models where a read may not see the most recent write that has been performed by other threads. These models come in different formalization styles (axiomatic, operational) and have their own advantages and disadvantages. In a POPL'13 paper, Demange et al [12], proposed an alternative style that is fully characterized in terms of the reorderings it allows. This Buffered Memory Model (BMM) targets the Java programming language. It is strictly less relaxed than the Java Memory Model. It is shown equivalent to an operational model but is restricted to TSO relaxations. This paper extends the BMM in order to allow more re-orderings. We present the new set of memory event reorder-ings rules that fully characterize the model and an alternative operational model that is again shown equivalent.
Document type :
Conference papers
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download
Contributor : Gurvan Cabon Connect in order to contact the contributor
Submitted on : Tuesday, October 25, 2016 - 3:56:34 PM
Last modification on : Saturday, June 25, 2022 - 7:40:44 PM
Long-term archiving on: : Saturday, February 4, 2017 - 7:23:13 PM


Files produced by the author(s)



Gurvan Cabon, David Cachera, David Pichardie. An Extended Buffered Memory Model With Full Reorderings. FtFjp - Ecoop workshop, Jul 2016, Rome, Italy. pp.1 - 6, ⟨10.1145/2955811.2955816⟩. ⟨hal-01379514⟩



Record views


Files downloads