CppMem: an interactive C/C++ memory model explorer

CppMem is a tool to let one explore the behaviour of small concurrent test programs in the relaxed memory model of the recent C11 and C++11 revisions of C and C++ [C++11 public draft N3376 (see 1.10, 29, 30)], [WG14] [WG21], Boehm and Adve, PLDI 2008], as formalised by Batty et al. [POPL 2011], which explains the model.

Usage

To start CppMem, simply click here. The basic usage is to select a model variant and test program, in the top left, and click run. The tool then computes the set of all candidate executions of that program, and whether each of them is consistent and race-free according to the model. You can then inspect the candidate executions one by one: for the current candidate, the tool shows its events and relations graphically in the bottom right, and shows the values of the model predicates for it in the top right. The next candidate and previous candidate buttons show the next or previous candidate, while the next consistent and previous consistent buttons skip to the next or previous consistent candidate. To change the program or model variant, one has to first click reset. To bring up this page, click help.

In the bottom left, the Display Relations, Display Layout, and edit display options let one fine-tune the graphical display. Clicking on the model predicates in the top right brings up another tab or window with their Lem definitions. Individual predicates can be ignored by clicking on the attached tick boxes, changing the behaviour of the next consistent and previous consistent buttons. The current execution can be exported in various formats with the Files: out.exc, out.dot, out.dsp, or out.tex links.

Model

CppMem supports the following versions of the C/C++11 model.

standard This is the memory model described by the 2011 C++11 standard. The mathematical definitions were constructed in discussion with the standardisation comittee, and there is a close correspondence between them and the standard text. This is essentially the same as the model described in our POPL 2011 paper, but with some light refactoring and improved lock and RMW semantics, as in our PLDI 2012 paper.
preferred (or no_vsse). This is a simplified variant of the standard model, that should be equivalent to it. It removes the complicated notion of visible sequences of side effects (VSSEs), whose force is covered by the coherence requirements. For those looking to work with general C or C++ concurrency, this is the preferred model.
tot This is a simpler model, for programs without consumes, relaxed, acquires or releases, that should be equivalent to the others for those. It has a single total order over all memory accesses.

Program

Test programs can be selected from a drop-down menu or typed directly into the window. They can be written in a small fragment of C/C++ including some of the C11/C++11 concurrency primitives. It also supports three non-standard extensions for writing concise tests: a parallel composition, written {{{ ... ||| ... }}}; constraints on read values such as x.readsvalue(1), which restricts attention to candidate executions in which that read of x reads the value 1; and dummy "thread-local" targets for reads, where we suppress the normal write events for variables starting with "r", e.g. in r1=x or r2=x.load(memory_order_relaxed). The tool calculates the set of all possible candidate executions for the test program, so tests should be relatively small and terminating. For some examples the interface will be unresponsive while it computes.

Instead of a program, one can also enter an execution (an .exc file), which directly specifies the actions and relations of some candidate execution of interest.

Display

Display Relations

The models use various binary relations over memory read, write, read-modify-write, lock, unlock, and fence actions. Clicking on these check boxes determines whether they are displayed in the graph, but does not affect the model. The first relations are determined by a choice of control-flow path for each thread, and the tool enumerates all possible alternatives using a thread-local semantics for the fragment of C/C++ supported.

sb sequenced-before relation
asw additional-synchronises-with
dd data-dependency
cd control-dependency

Next we have several relations that are existentially quantified: for each choice of control-flow paths, the tool enumerates all possible alternatives of the following:

rf The reads-from relation, from writes to all the reads that read from them
tot The total order of the tot model
mo The modification order (or coherence order) over writes to atomic locations, total per location
sc A total order over the sequentially consistent atomic actions
lo The lock order

Finally there are derived relations, calculated by the model from the relations above:

hb happens-before
vse visible side effects
vsses visible sequences of side effects
ithb inter-thread happens-before
dob dependency-ordered-before
cad carries-a-dependency-to
sw synchronises-with
hrs hypothetical release sequence
rs release sequence
data_races inter-thread data races
unsequenced_races intra-thread unsequenced races, unrelated by sb

Display Layout

There are several graph layout choices available: dot, neato_par, neato_par_init, and neato_downwards.

It is also possible to output the graph with tex labels.

Display Options

This lets one tune a variety of other display parameters, for font size, etc.

About

CppMem exists in web-interface and command-line versions. It is written in OCaml; the web-interface version uses js_of_ocaml to compile into JavaScript, with most of the computation running in the browser but graph layout on a server. The model definitions are written in Lem and compiled from that to OCaml code.