Remote-scope promotion: clarified, rectified, and verified

This webpage contains additional material for the OOPSLA 2015 paper Remote-Scope Promotion: Clarified, Rectified, and Verified by John Wickerson, Mark Batty, Bradford M. Beckmann, and Alastair F. Donaldson.

OpenCL+RSP memory modelling in Herd (Sections 3 and 4)

The following instructions should enable reproduction of the claims in Sections 3 and 4 of the paper that (a) we have extended the Herd simulator with support for remote-scope promotion, (b) this allows investigation of the remote-scope promotion litmus tests, confirming the issues we reported in the paper, and (c) one of these tests captures the bug we found in the work-stealing queue implementation.

Getting started with Herd (virtual machine)

  1. Download the virtual machine and proceed to step number 4 below. (The username is herd and the password is letmein.)

Getting started with Herd (from source)

  1. Download the source code from Github.
  2. In the herdtools directory, run make. This assumes that OCaml, version 4.00 or greater, is installed.
  3. In the herd directory, run ./herd ‑help to check that Herd has been built correctly.
  4. The herd/testsuite/RSPTests directory contains 14 .litmus tests, 12 of which correspond to the test suite of the original RSP developers, and 2 of which were extracted from the work-stealing queue implementation of Orr et al.
  5. In the herd directory, the opencl_rem.cat file contains our formalisation of the OpenCL+RSP memory model.
  6. To use Herd to explore the behaviour of a litmus test P.litmus with respect to a model M.cat, run ./herd ‑initwrites true ‑model M.cat P.litmus. For example, to simulate the first RSP litmus test, run the following command.
    ./herd -initwrites true -model opencl_rem.cat testsuite/RSPTests/RSP_Test1.litmus
    This should produce output that includes the following lines.
    States 16
    Positive: 1 Negative: 15
    Bad executions (0 in total):
    This output indicates that Herd has found 16 executions of this test that are consistent with the memory model, that one of these executions satisfies the litmus test's postcondition, and that none of the executions are racy. The postcondition of a litmus test expresses a condition that is expected never to hold, so this output tells us that the test's postcondition is too strong: it is forbidding outcomes that OpenCL+RSP actually allows.
  7. Bonus step. If you have gv and graphviz installed, you can make use of the graphical user interface that Herd provides. To see the 16 executions of the first RSP litmus test, run the following command.
    ./herd -model opencl_rem.cat -initwrites true -show all -gv -graph columns -showinitwrites false -squished true -scale 2 -symetric dr testsuite/RSPTests/RSP_Test1.litmus

Results

We list here the results that we obtained. We report 'postcondition violated' when Herd's output includes Positive: n for some n>0. We report 'races found' when Herd's output includes Bad executions (n in total) for some n>0. We also report the approximate time taken, in seconds, to simulate the test on a 3.1 GHz MacBook Pro. These results can be recreated on our virtual machine (see link above) by running the script runtests.sh in the home directory.

Test Postcondition violated? Races found? Simulation time /s
RSPTest1 yes no 0
RSPTest2 no no 0
RSPTest3 no no 0
RSPTest4 no yes 0
RSPTest5 no no 0
RSPTest6 no no 0
RSPTest7 yes yes 0
RSPTest8 no no 145
RSPTest9 no yes 119
RSPTest10 no no 0
RSPTest11 yes no 34
RSPTest12 none given yes* 0
WSQ1 no no 0
WSQ2 no yes 0
*NB: Test RSPTest12 has a deliberate data race.

In summary, tests RSPTest1 and RSPTest11 have postconditions that rule out behaviours that OpenCL+RSP actually allows, while tests RSPTest4, RSPTest7 and RSPTest9 all have inadvertent data races. The data race in test WSQ2 corresponds to the bug discovered in the work-stealing queue implementation of Orr et al (Section 4.3).

Isabelle formalisation (Section 5)

The following instructions should enable reproduction of the claim, in Section 5 of the paper, that we have formalised Orr et al.'s implementation of remote-scope promotion in Isabelle. Our formalisation comprises a mathematical model of a simple GPU device, the semantics of a minimal assembly language for this device, and a scheme for compiling OpenCL+RSP to this assembly language.

We have formalised in Isabelle the statement of the soundness theorem for the implementation of OpenCL+RSP, but we have only proved this theorem by hand. We do not claim in the paper to have mechanised the proof.

Getting started

  1. Download Isabelle2015.
  2. Download the Isabelle formalisation.

Commentary

The Isabelle formalisation is split into several files. We name and describe each below.