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.

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

Model
- Specifies the C++ memory model. preferred is the C++ memory model.
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.
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
Display Layout
- You can choose with this switch which Doxygraph graph is used.
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.

Modernes C++ Mentoring

"Fundamentals for C++ Professionals" (open)

"Design Patterns and Architectural Patterns with C++" (open)

"C++20: Get the Details" (open)

"Concurrency with Modern C++" (open)

"Generic Programming (Templates) with C++": October 2024

"Embedded Programming with Modern C++": October 2024

"Clean Code: Best Practices for Modern C++": March 2025

Do you want to stay informed: Subscribe.

The test run

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

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.
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.
It is extremely interesting to switch between the different interleaving of the threads.
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.

Post Views: 6,090

Thanks a lot to my Patreon Supporters: Matt Braun, Roman Postanciuc, Tobias Zindl, G Prvulovic, Reinhold Dröge, Abernitzke, Frank Grimm, Sakib, Broeserl, António Pina, Sergey Agafyin, Андрей Бурмистров, Jake, GS, Lawton Shoemake, Jozo Leko, John Breland, Venkat Nandam, Jose Francisco, Douglas Tinkham, Kuchlong Kuchlong, Robert Blanch, Truels Wissneth, Mario Luoni, Friedrich Huber, lennonli, Pramod Tikare Muralidhara, Peter Ware, Daniel Hufschläger, Alessandro Pezzato, Bob Perry, Satish Vangipuram, Andi Ireland, Richard Ohnemus, Michael Dunsky, Leo Goodstadt, John Wiederhirn, Yacob Cohen-Arazi, Florian Tischler, Robin Furness, Michael Young, Holger Detering, Bernd Mühlhaus, Stephen Kelley, Kyle Dean, Tusar Palauri, Juan Dent, George Liao, Daniel Ceperley, Jon T Hess, Stephen Totten, Wolfgang Fütterer, Matthias Grün, Phillip Diekmann, Ben Atakora, Ann Shatoff, Rob North, Bhavith C Achar, Marco Parri Empoli, Philipp Lenk, Charles-Jianye Chen, Keith Jeffery,and Matt Godbolt.

Thanks, in particular, to Jon Hess, Lakshman, Christian Wittenhorst, Sherhy Pyton, Dendi Suhubdy, Sudhakar Belagurusamy, Richard Sargeant, Rusty Fleming, John Nebel, Mipko, Alicja Kaminska, Slavko Radman, and David Poole.

My special thanks to Embarcadero
My special thanks to PVS-Studio
My special thanks to Tipi.build
My special thanks to Take Up Code
My special thanks to SHAVEDYAKS