CppMem - An Overview

CppMem is an interactive tool for exploring the behavior of small code snippets of the C++ memory model. No, it should have to be in the toolbox of each programmer who deals seriously with the memory model.

The online tool CppMem provides in a twofold way very valuable services.

1. CppMem verifies the well-defined behavior of small code snippets. The tool performs on the basis of the C++ memory model all possible interleavings of threads, visuals each one in a graph, and annotates these graphs with additional details
2. The very accurate analysis of CppMem gives you a deep insight into the C++ memory model. To make it short. CppMem is the tool for a better understanding of the C++ memory model.

Of course, it's like the things you have first to overcome a few hurdles. The nature of the things is that CppMem gives you the whole details of the extremely challenging topic and is highly configurable. So, I plan to present the tool's components, which you can also install on your PC.

The overview

My simplified overview uses the default configuration. This overview should give you the base for further experiments.

For simplicity reasons, I will follow the red numbers in the screenshot. 

1. Model
   • Specifies the C++ memory model. preferred is the C++ memory model.
2. Program
   • Is the executable program in C or C++ syntax?
   • CppMem covers a bunch of programs for typical scenarios of multithreading. To get the details of these programs, read the well-written article Mathematizing C++ Concurrency. Of course, you can also use your code.
   • CppMem is about multithreading, so there are two specialties.
     
     • You can easily define two threads by the symbols {{{  ... ||| ... }}}. The three dots (...) are the work packages of the two threads.
     • By using x.readvalue(1), you reduce the possible interleavings of the threads to these interleavings, for which the thread execution gives the value 1 for x.
3. Display Relations
   • Describes the relations between the read, write, and read-write modifications on atomic operations, fences, and locks. 
   • You can explicitly enable the relations in the annotated graph with the switches.
   • There are three classes of relations. From my perspective, the coarser distinction between original and derived relations is the most interesting. Here are the default values.
     • Original relations:
       • sb: sequenced-before
       • rf: read from
       • mo: modification order
       • sc: sequentially consistent
       • lo: lock order
     • Derived relations:
       • sw: synchronises-with
       • dob: dependency-ordered-before
       • unsequenced_races: races in a single thread
       • data_races
4. Display Layout
   • You can choose with this switch which Doxygraph graph is used.
5. Model Predicates
   • I have no clue what this switch means. I didn't find anything in the documentation either.

For a deeper insight, you have the official documentation. So, that's enough as starting point. Now it's time to press the run button. 

The test run

The run button shows it immediately. There is a data race.

1. The data race is relatively easy to see. A thread writes x (x = 3), and another thread unsynchronized reads x (x==3). That can not work.
2. Two interleavings of threads are possible due to the C++ memory model. Only one of them is consistent. That is the case if in the expression x==3 the value of x is written from the expression int x = 2 in the main function. The graph displays this relation in the edge annotated with rf and sw.
3. It is extremely interesting to switch between the different interleaving of the threads.
4. The graph shows all relations in the format display layout, which you enabled in the Display Relations.
   • a: Wna x=2 is in the graphic the a-th statement, which is a not atomic Write.
   • The key edge in the graph is the edge between the writing of x (b:Wna) and the reading of x (C:Rna). That's the data race on x: (data_race(dr)).

What's next?

That was the test run. In the next post, I will analyze the simple program with the help of CppMem. You know, this program has undefined behavior.