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.


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.


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


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 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.

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: Finally there are derived relations, calculated by the model from the relations above:

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.


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.