{"id":4834,"date":"2016-07-30T20:02:16","date_gmt":"2016-07-30T20:02:16","guid":{"rendered":"https:\/\/www.modernescpp.com\/index.php\/cppmem-an-overview\/"},"modified":"2023-06-26T12:48:27","modified_gmt":"2023-06-26T12:48:27","slug":"cppmem-an-overview","status":"publish","type":"post","link":"https:\/\/www.modernescpp.com\/index.php\/cppmem-an-overview\/","title":{"rendered":"CppMem &#8211; An Overview"},"content":{"rendered":"<p><a href=\"http:\/\/svr-pes20-cppmem.cl.cam.ac.uk\/cppmem\/\">CppMem<\/a> 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.<\/p>\n<p><!--more--><\/p>\n<p>&nbsp;<\/p>\n<p>The online tool CppMem provides in a twofold way very valuable services.<\/p>\n<ol>\n<li>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<\/li>\n<li>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.<\/li>\n<\/ol>\n<p>Of course, it&#8217;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&#8217;s components, which you can also install on your PC.<\/p>\n<\/p>\n<h2>The overview<\/h2>\n<p>My simplified overview uses the default configuration. This overview should give you the base for further experiments.<\/p>\n<p>&nbsp;<img loading=\"lazy\" decoding=\"async\" class=\" size-full wp-image-4832\" src=\"https:\/\/www.modernescpp.com\/wp-content\/uploads\/2016\/07\/CppMemUeberblickNumbers.png\" alt=\"CppMemUeberblickNumbers\" width=\"800\" height=\"523\" style=\"margin: 15px;\" srcset=\"https:\/\/www.modernescpp.com\/wp-content\/uploads\/2016\/07\/CppMemUeberblickNumbers.png 1067w, https:\/\/www.modernescpp.com\/wp-content\/uploads\/2016\/07\/CppMemUeberblickNumbers-300x196.png 300w, https:\/\/www.modernescpp.com\/wp-content\/uploads\/2016\/07\/CppMemUeberblickNumbers-1024x669.png 1024w, https:\/\/www.modernescpp.com\/wp-content\/uploads\/2016\/07\/CppMemUeberblickNumbers-768x502.png 768w\" sizes=\"auto, (max-width: 800px) 100vw, 800px\" \/><\/p>\n<p>For simplicity reasons, I will follow the red numbers in the screenshot.&nbsp;<\/p>\n<ol>\n<li><strong>Model<\/strong>\n<ul>\n<li>Specifies the C++ memory model. <em>preferred<\/em> is the C++ memory model.<\/li>\n<\/ul>\n<\/li>\n<li><strong>Program<\/strong>\n<ul>\n<li>Is the executable program in C or C++ syntax?<\/li>\n<li>CppMem covers a bunch of programs for typical scenarios of multithreading. To get the details of these programs, read the well-written article <a href=\"http:\/\/www.cl.cam.ac.uk\/~pes20\/cpp\/popl085ap-sewell.pdf\">Mathematizing C++ Concurrency<\/a>. Of course, you can also use your code.<\/li>\n<li>CppMem is about multithreading, so there are two specialties.\n<ul>\n<li>You can easily define two threads by the symbols <span style=\"font-family: courier new,courier;\">{{{&nbsp; &#8230; ||| &#8230; }}}<\/span>.&nbsp;The three dots (&#8230;) are the work packages of the two threads.<\/li>\n<li>By using <span style=\"font-family: courier new,courier;\">x.readvalue(1)<\/span>, you reduce the possible interleavings of the threads to these interleavings, for which the thread execution gives the value 1 for x.<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<\/li>\n<li><strong>Display Relations<\/strong>\n<ul>\n<li>Describes the relations between the read, write, and read-write modifications on atomic operations, fences, and locks.&nbsp;<\/li>\n<li>You can explicitly enable the relations in the annotated graph with the switches.<\/li>\n<li>There are three classes of <a href=\"http:\/\/svr-pes20-cppmem.cl.cam.ac.uk\/cppmem\/help.html\">relations<\/a>. From my perspective, the coarser distinction between original and derived relations is the most interesting. Here are the default values.\n<ul>\n<li>Original relations:\n<ul>\n<li><strong>sb<\/strong>: sequenced-before<\/li>\n<li><strong>rf:<\/strong> read from<\/li>\n<li><strong>mo<\/strong>: modification order<\/li>\n<li><strong>sc<\/strong>: sequentially consistent<\/li>\n<li><strong>lo<\/strong>: lock order<\/li>\n<\/ul>\n<\/li>\n<li>Derived relations:\n<ul>\n<li><strong>sw:<\/strong> synchronises-with<\/li>\n<li><strong>dob<\/strong>: dependency-ordered-before<\/li>\n<li><strong>unsequenced_races<\/strong>: races in a single thread<\/li>\n<li><strong>data_races<\/strong><\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<\/li>\n<li><strong>Display Layout<\/strong>\n<ul>\n<li>You can choose with this switch which <a href=\"https:\/\/sourceforge.net\/projects\/doxygraph\/\">Doxygraph<\/a> graph is used.<\/li>\n<\/ul>\n<\/li>\n<li><strong>Model Predicates<\/strong>\n<ul>\n<li>I have no clue what this switch means. I didn&#8217;t find anything in the documentation either.<\/li>\n<\/ul>\n<\/li>\n<\/ol>\n<p>For a deeper insight, you have the official <a href=\"http:\/\/svr-pes20-cppmem.cl.cam.ac.uk\/cppmem\/help.html\">documentation.<\/a> So, that&#8217;s enough as starting point. Now it&#8217;s time to press the run button.&nbsp;<\/p>\n<h2>The test run<\/h2>\n<p>The run button shows it immediately. There is a<a href=\"https:\/\/www.modernescpp.com\/index.php\/threads-sharing-data\"> data race<\/a>.<\/p>\n<p>&nbsp;<img loading=\"lazy\" decoding=\"async\" class=\" size-full wp-image-4833\" src=\"https:\/\/www.modernescpp.com\/wp-content\/uploads\/2016\/07\/CppMemUeberblickNumbersRun.png\" alt=\"CppMemUeberblickNumbersRun\" width=\"800\" height=\"600\" style=\"margin: 15px;\" srcset=\"https:\/\/www.modernescpp.com\/wp-content\/uploads\/2016\/07\/CppMemUeberblickNumbersRun.png 960w, https:\/\/www.modernescpp.com\/wp-content\/uploads\/2016\/07\/CppMemUeberblickNumbersRun-300x225.png 300w, https:\/\/www.modernescpp.com\/wp-content\/uploads\/2016\/07\/CppMemUeberblickNumbersRun-768x576.png 768w\" sizes=\"auto, (max-width: 800px) 100vw, 800px\" \/>&nbsp;<\/p>\n<ol>\n<li>The data race is relatively easy to see. A thread writes x (<span style=\"font-family: courier new,courier;\">x = 3<\/span>), and another thread unsynchronized reads x (<span style=\"font-family: courier new,courier;\">x==3<\/span>). That can not work.<\/li>\n<li>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 <span style=\"font-family: courier new,courier;\">x==3<\/span> the value of x is written from the expression&nbsp;<span style=\"font-family: courier new,courier;\">int x = 2 <\/span>in the <span style=\"font-family: courier new,courier;\">main<\/span> function. The graph displays this relation in the edge annotated with <span style=\"color: #ff0000;\">rf<\/span> and sw.<\/li>\n<li>It is extremely interesting to switch between the different interleaving of the threads.<\/li>\n<li>The graph shows all relations in the format display layout, which you enabled in the Display Relations.\n<ul>\n<li><span style=\"color: #ff0000;\">a<\/span>:<span style=\"color: #00ff00;\"><span style=\"color: #339966;\"> W<\/span><\/span><span style=\"color: #0000ff;\">na<\/span> x=2 is in the graphic the <span style=\"color: #ff0000;\"><strong>a<\/strong><\/span>-th statement, which is a<strong><span style=\"color: #0000ff;\"> n<\/span><\/strong><span style=\"color: #0000ff;\"><span style=\"color: #000000;\">ot<\/span><\/span> <span style=\"color: #0000ff;\"><strong>a<\/strong><span style=\"color: #000000;\">tomic<\/span><\/span><span style=\"color: #000000;\"> W<\/span>rite.<\/li>\n<li>The key edge in the graph is the edge between the writing of x (b:Wna) and the reading of x (C:Rna). That&#8217;s the data race on x: (data_race(<span style=\"color: #ff9900;\">dr<\/span>)).<\/li>\n<\/ul>\n<\/li>\n<\/ol>\n<h2>What&#8217;s next?<\/h2>\n<p>That was the test run. In the next post, I will analyze the <a href=\"https:\/\/www.modernescpp.com\/index.php\/relaxed-semantic\">simple program<\/a> with the help of CppMem. You know, this program has undefined behavior.<\/p>\n<p>&nbsp;<\/p>\n<p>&nbsp;<\/p>\n<p>&nbsp;<\/p><\/p>\n","protected":false},"excerpt":{"rendered":"<p>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.<\/p>\n","protected":false},"author":21,"featured_media":4832,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[369],"tags":[434,486],"class_list":["post-4834","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-multithreading-application","tag-atomics","tag-cppmem"],"_links":{"self":[{"href":"https:\/\/www.modernescpp.com\/index.php\/wp-json\/wp\/v2\/posts\/4834","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.modernescpp.com\/index.php\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.modernescpp.com\/index.php\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.modernescpp.com\/index.php\/wp-json\/wp\/v2\/users\/21"}],"replies":[{"embeddable":true,"href":"https:\/\/www.modernescpp.com\/index.php\/wp-json\/wp\/v2\/comments?post=4834"}],"version-history":[{"count":1,"href":"https:\/\/www.modernescpp.com\/index.php\/wp-json\/wp\/v2\/posts\/4834\/revisions"}],"predecessor-version":[{"id":6960,"href":"https:\/\/www.modernescpp.com\/index.php\/wp-json\/wp\/v2\/posts\/4834\/revisions\/6960"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.modernescpp.com\/index.php\/wp-json\/wp\/v2\/media\/4832"}],"wp:attachment":[{"href":"https:\/\/www.modernescpp.com\/index.php\/wp-json\/wp\/v2\/media?parent=4834"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.modernescpp.com\/index.php\/wp-json\/wp\/v2\/categories?post=4834"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.modernescpp.com\/index.php\/wp-json\/wp\/v2\/tags?post=4834"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}