CppMem - An Overview

Contents[Show]

CppMem is an interactive tool for exploring the behaviour of small code snippets of the C++ memory model. It should, no it has to be in the tool box of each programmer, who deals seriously with the memory model.

 

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

  1. CppMem verifies the well defined behaviour of small code snippets. The tool performs on the base 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 in 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 in the nature of the things, that you have at first to overcome a few hurdles. The nature of the things is, that CppMem give you the whole details to the extremely challenging topic and is highly configurable. So, my plan is to present you the components of the tool, 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.

 CppMemUeberblickNumbers

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 overs a bunch of programs to typical scenarios of multithreading. To get the details to these programs, read the very well written article Mathematizing C++ Concurrency. Of course you can also use your own code.
    • CppMem is about multithreading, so there are two specialities.
      • You can easily define two thread 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 this 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
      • Dervived 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
    • To be honest, I have no glue, 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 staring point. Now it's time to press the run button. 

The test run

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

 CppMemUeberblickNumbersRun 

  1. The data race is quite easy to see. A thread writes x (x = 3), an other 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 in the format display layout all relations, 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. I will in the next post analyse the simple program with the help of CppMem. You know, this program has undefined behaviour.

 

 

 

 

 

 

title page smalltitle page small Go to Leanpub/cpplibrary "What every professional C++ programmer should know about the C++ standard library".   Get your e-book. Support my blog.

 

Comments   

0 #21 Johnson 2017-01-03 11:27
Great web site you've got here.. It's difficult to find good quality writing like
yours these days. I really appreciate individuals like you!

Take care!!
Quote
0 #22 Ritchie Pettauer 2017-01-15 07:16
Just wanna state that this is invaluable, Thanks for taking your time
to write this.
Quote
0 #23 Edith 2017-01-21 17:04
Hello.magnificent job. I did not expet this. This is a excellent story.
Thanks!
Quote
0 #24 Kia 2017-01-27 06:09
Good day! I simply would like to give an enormous thumbs up
for the nice information you have right here on this post.
I will be coming back to your blog for extra
soon.
Quote
0 #25 เสื้อยืดชาย 2017-07-21 11:46
I constantly emailed this webpage post page to all my
friends, as if like to read it then my links will too.
Quote
0 #26 เสื้อโปโลราคาส่ง 2017-07-21 16:53
If you are going for best contents like
me, only pay a quick visit this site everyday as it gives quality contents,
thanks
Quote
0 #27 เสื้อยี่ห้อโปโล 2017-07-21 23:43
WOW just what I was searching for. Came here by
searching for mode
Quote

Add comment


My Newest E-Books

Latest comments

Subscribe to the newsletter (+ pdf bundle)

Blog archive

Source Code

Visitors

Today 786

All 386377

Currently are 213 guests and no members online