Blogs (28) >>
ECOOP 2016
Sun 17 - Fri 22 July 2016 Rome, Italy
Tue 19 Jul 2016 14:20 - 14:50 at Belli - Session 3 Chair(s): Davide Ancona

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 allows more reorderings. We present the new set of memory event reorderings rules that fully characterize the model and an alternative operational model that is again shown equivalent.

Tue 19 Jul

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:50 - 15:20
Session 3FTfJP at Belli
Chair(s): Davide Ancona University of Genova
13:50
30m
Talk
Generating Concurrency Checks Automatically
FTfJP
Jonathan Hoyland Royal Holloway University of London, Matthew Hague Royal Holloway University of London
14:20
30m
Talk
An Extended Buffered Memory Model With Full Reorderings
FTfJP
14:50
30m
Talk
Towards a Model of Corecursion with Default
FTfJP
Davide Ancona University of Genova, Francesco Dagnino , Elena Zucca University of Genova