Supervisor

Suitable for

Abstract

Concurrent programs on modern architectures can often behave in surprising ways: the presence of caches means that writes can take time to propagate from one thread to another; the compiler can perform optimisations that cause operations to be re-ordered; similarly, the hardware may execute operations out of order.

For example, given the Scala program var x = 0; var y = 0 def P = { val r1 = x; y = 1 } def Q = { val r2 = y; x = 1 }

Executing P and Q in parallel may lead to a state where r1 = r2 = 1, counter-intuitively, for example as a result of P's two statements being re-ordered.

The Java Memory Model (JMM) gives a formal definition of the behaviours that are allowed for such programs. Unfortunately, the definition is convoluted and hard to understand. The aim of this project is to aid better understanding of the JMM, by producing a tool that, given a small program (like the one above or the ones in [4]), returns all its valid executions.

References:

[1] Java Memory Model Pragmatics (transcript), Aleksey Shipilev, http://shipilev.net/blog/2014/jmm-pragmatics.

[2] Formalising Java's Data Race Free Guarantee, David Aspinall and Jaroslav Sevcik.

[3] Jeremy Manson, William Pugh and Sarita Adve, The Java Memory Model.

[4] William Pugh and Jeremy Manson, Java memory model causality test cases (2004), http://www.cs.umd.edu/~pugh/java/memoryModel/CausalityTestCases.html.