CppMem - Ein Überblick

CppMem ist ein interaktives Werkzeug, um das Verhalten kleiner Codeschnipsel zum C++-Speichermodell zu verifizieren. Es gehört in die Werkzeugkiste jedes Programmierers, der sich mit dem C++-Speichermodell ernsthaft beschäftigt.

Das online-Werkzeug CppMem leistet in doppelter Hinsicht sehr wertvolle Dienste. 

1. CppMem verifiziert kleine Codeschnipsel auf ihre Wohldefiniertheit. Dabei führt das Werkzeug auf Grundlage des C++-Speichermodells alle möglichen verschränkten Ausführungen der Threads durch, visualisiert jede Ausführung als Graph und annotiert diesen Graphen mit Detailinformationen.
2. CppMem gibt durch seine sehr genaue Analyse einen tiefen Einblick in das C++-Speichermodell. Daher ist es das ideale Werkzeug für ein besseres Verständnis des C++-Speichermodells.

Es liegt in der Natur der Sache, das der Umgang mit CppMem ein paar Hürden in den Weg stellt. Die Natur der Sache ist es, dass CppMem die ganze Detailinformation zu dem sehr anspruchsvollen Thema bereitstellt und dazu noch hoch konfiguierbar ist. Daher werde ich die Komponenten des Werkzeugs, das sich auch auf dem eigenen PC installieren lässt, genauer vorstellen.

Der Überblick

Bei meinem einfachen Überblick gehe ich von der Standardkonfiguration aus. Dieser Überblick soll als Startpunkt für weitere Experimente dienen. 

Der Einfachheit halber folgt die Nummerierung den roten Zahlen in dem Screenshot.

1. Model
   • Spezifiziert das C++-Speichermodell. preferred entspricht dem C++-Speichermodell.
2. Program
   • Enthält das ausführbare Programm in C oder C++ Syntax.
   • CppMem bietet einen Satz an Programmen zu typischen Szenarien von Multithreading Programmen an. Genauer sind die in dem sehr lesenswerten Artikel Mathematizing C++ Concurrency beschrieben. Darüber hinaus lässt sich natürlich auch eigener Code ausführen. 
   • Da es um Threads bei CppMem geht, besitzt das Werkzeug zwei Besonderheiten.
     • Threads werden einfach durch die Symbole {{{  ... ||| ... }}} definiert. Dabei stehen die Ellipse (...) für das jeweilige Arbeitspaket der zwei Threads.
     • Durch x.readvalue(1) wird die Anzahl der verschränkten Threadausführungen auf die Möglichkeiten reduziert, für die die Threadausführung den Wert 1 für x ergibt.
3. Display Relations
   • Beschreibt die Beziehungen zwischen Lese, Schreibe und Lese-Schreibe-Modifikationen auf atomaren Operationen, Speicherbarrieren und Locks.
   • Die Beziehungen lassen sich explizit im annotierten Graphen mit den Schaltern auswählen.
   • Es gibt drei Gruppen von Beziehungen. Für mich ist aber die gröbere Unterscheidung in ursprüngliche bwz. abgeleiteten Beziehungen am interessantesten. Die Standardwerte werde ich kurz erläutern.
     • Ursprüngliche Beziehung:
       • sb: sequenced-before
       • rf: read from
       • mo: modification order
       • sc: sequentially consisten
       • lo: lock order
     • Abgeleitete Beziehung:
       • sw: sychronises-with
       • dob: dependency-ordered-before
       • unsequenced_races: Wettläufe innerhalb eines Threads
       • data_races: kritischer Wettlauf
4. Display Layout
   • Mit diesen Schaltern lässt sich steuern, welche Doxygraph-Graph zur Anwendung kommen soll.
5. Model Predicates
   • Von diesen Schaltern habe ich selber noch nie Gebrauch gemacht. In der Dokumentation werden sie auch nicht beschrieben.

Tiefere Einsichten gibt die offizielle Dokumentation. Als Startpunkt sollte mein einfacher Überblick genügen. Jetzt ist es an der Zeit, den run-Button zu drücken.

Der Probelauf

Der run-Button bringt es sofort auf den Punkt. Das Programm besitzten einen kritischen Wettlauf (data_race). 

1. Der kritische Wettlauf ist einfach in dem Beispiel zu identifizieren. Ein Thread schreibt x (x = 3), während der andere Thread x nicht synchronisiert liest (x==3). Das kann nicht gut gehen.
2. Zwei verschränkte Ausführungen von Threads sind aufgrund des C++-Speichermodells möglich. Eine Ausführung ist zu mindestens konsistent. Dies ist der Fall, wenn in dem Ausdruck x==3 der Wert von x von dem Ausdruck int x = 2 in der main-Funktion gelesen wird. Das stellt der Graph in der Kante in der rechten, oberen Kante dar, die mit rf und sw annotiert ist.
3. Sehr interessant ist, zwischen den verschiedenen verschränkten Ausführungen der Threads zu wechseln. 
4. Der Graph zeigt im Format Display Layout alle Beziehungen an, die in Display Relations gewählt wurden.
   • a:Wna x=2 steht steht in der Graphik für den a-ten Ausdruck, der ein nicht atomarer Write ist.
   • Die entscheidende Kanten in dem Graph ist die Kante zwischen dem Schreiben von x (b:Wna) und dem Lesen von x (C:Rna). Hier ist der kritische Wettlauf (data_race(dr)) um x.

Wie geht's weiter?

Das war der Probelauf. Im nächsten Artikel werde ich die Variationen des einfachen Programms aus der Minireihe Sukzessiver Optimierung mit CppMem genauer analysieren. 

Go to Leanpub/cpplibrary "What every professional C++ programmer should know about the C++ standard library".   Hole dir dein E-Book. Unterstütze meinen Blog.