CppMem - 概要

CppMem は、C++ メモリ モデルの小さなコード スニペットの動作を調査するための対話型ツールです。メモリ モデルを真剣に扱う各プログラマーのツールボックスにある必要があります。

オンライン ツール CppMem は、2 つの方法で非常に価値のあるサービスを提供します。

<オール>
  • CppMem は、小さなコード スニペットの明確に定義された動作を検証します。このツールは、C++ メモリ モデルに基づいて、可能なすべてのスレッドのインターリーブを実行し、それぞれをグラフに視覚化し、これらのグラフに追加の詳細で注釈を付けます
  • CppMem の非常に正確な分析により、C++ メモリ モデルを深く理解できます。短くするために。 CppMem は、C++ メモリ モデルをよりよく理解するためのツールです。
  • もちろん、物事の性質上、最初はいくつかのハードルを乗り越えなければなりません。物事の性質は、CppMem が非常に困難なトピックの詳細をすべて提供し、高度に構成可能であることです。そこで、私の計画は、PC にもインストールできるツールのコンポーネントを紹介することです。

    概要

    私の簡略化された概要では、既定の構成を使用します。この概要は、さらなる実験の基礎となるはずです。

    簡単にするために、スクリーンショットの赤い数字に従います。

    <オール>
  • モデル
    • C++ メモリ モデルを指定します。 優先 C++ メモリ モデルです。
  • プログラム
    • C または C++ 構文の実行可能プログラムです。
    • CppMem は、一連のプログラムをマルチスレッドの典型的なシナリオに置き換えます。これらのプログラムの詳細については、非常によく書かれた記事「Mathematizing C++ Concurrency」をお読みください。もちろん、独自のコードを使用することもできます。
    • CppMem はマルチスレッドに関するものなので、2 つの専門分野があります。
      • 記号 {{{ ... ||| で 2 つのスレッドを簡単に定義できます。 ...}}}。 3 つのドット (...) は、2 つのスレッドの作業パッケージです。
      • x.readvalue(1) を使用することにより、スレッドの実行が x の値 1 を与えるこれらのインターリービングに、スレッドの可能なインターリービングを減らします。
  • 表示関係
    • アトミック操作、フェンス、およびロックの読み取り、書き込み、読み書き変更間の関係について説明します。
    • スイッチを使用して、注釈付きグラフの関係を明示的に有効にすることができます。
    • 関係には 3 つのクラスがあります。私の見解では、元の関係と派生した関係の間のより粗い区別が最も興味深いものです。デフォルト値は次のとおりです。
      • 元の関係:
        • sb :前に配列
        • rf: から読む
        • :変更命令
        • sc :順次整合
        • こんにちは :ロック順序
      • 派生関係:
        • sw: と同期
        • ドブ :依存関係の順序付け前
        • unsequenced_races :シングルスレッドでレース
        • data_races
  • 表示レイアウト
    • このスイッチで、どの Doxygraph グラフを使用するかを選択できます。
  • モデルの述語
    • 正直に言うと、このスイッチが何を意味するのか、私には接着剤がありません。ドキュメントにも何も見つかりませんでした。
  • より深い洞察については、公式ドキュメントがあります。だから、それは出発点として十分です。いよいよ実行ボタンを押します。

    テスト実行

    実行ボタンはすぐにそれを示します。データ競合があります。

    <オール>
  • データ競合は非常に簡単に確認できます。あるスレッドが x (x =3) を書き込み、非同期の別のスレッドが x (x==3) を読み取ります。それはうまくいきません。
  • C++ メモリ モデルにより、スレッドの 2 つのインターリーブが可能です。そのうちの 1 つだけが一貫しています。これは、式 x==3 で x の値がメイン関数の式 int x =2 から書き込まれている場合です。グラフは、rf と sw の注釈が付けられたエッジにこの関係を示しています。
  • スレッドの異なるインターリーブを切り替えるのは非常に興味深いことです。
  • グラフは、表示関係で有効にしたすべての関係をフォーマット表示レイアウトで表示します。
    • a:Wna x=2 は a のグラフィックにあります - 番目のステートメント。 n その他 a トミック書き込み。
    • グラフのキー エッジは、x の書き込み (b:Wna) と x の読み取り (C:Rna) の間のエッジです。これが x:(data_race(dr)) のデータ競合です。
  • 次は?

    それが試運転でした。次の投稿では、CppMem を使用して簡単なプログラムを分析します。このプログラムには未定義の動作があります。