正規の意味論

正規セマンティクスは、コンピュータ ハードウェアの 一貫性モデルです。これは、並列マシンまたは連携して動作するコンピュータ ネットワーク内の複数のプロセッサ コアによって共有されるプロセッサ レジスタによって提供される保証のタイプを表します。正規セマンティクスは、単一の書き込みと複数の読み取りを持つ変数に対して定義されます。これらのセマンティクスは、安全セマンティクスよりも強力ですが、アトミック セマンティクスよりも弱く、書き込み操作にリアルタイムと一致する完全な順序があること、および読み取り操作が読み取り開始前に完了した最後の書き込みの値、または読み取りと同時に実行される書き込みのいずれかの値を返すことを保証します。

正規セマンティクスは線形化可能性よりも弱い。以下に示す例を考えてみよう。ここで、横軸は時間を表し、矢印は読み取りまたは書き込み操作が行われる間隔を表す。正規レジスタの定義によれば、最初の読み取りは 5 または 2 を返す可能性があり、2 番目の読み取りも同様である。最初の読み取りは 2 を返し、2 番目の読み取りは 5 を返す可能性がある (新旧反転とも呼ばれる)。この動作はアトミック セマンティクスを満たさない。したがって、正規セマンティクスはアトミック セマンティクスよりも弱い特性である。一方、レスリー ランポートは、線形化可能なレジスタは、通常のレジスタよりも弱い安全なセマンティクスを持つレジスタから実装できることを証明した。^[1]

シングルライターマルチリーダー（SWMR）アトミックセマンティクスは、その実行履歴 H のいずれかが次のプロパティを満たす場合、SWMR レギュラーレジスタです。r1 と r2 は、任意の 2 つの読み取り呼び出しです。(r1 →H r2) ⇒ ¬π(r2) →H π(r1)

証明に入る前に、まず、新旧反転が何を意味するかを理解する必要があります。下の図に示すように、実行を見ると、通常の実行とアトミック実行の唯一の違いは、a = 0 と b = 1 の場合であることがわかります。この実行では、2 つの読み取り呼び出し R.read() → a とそれに続く R.read() → b を考えると、最初の値 (新しい値) は a = 0 で、2 番目の値 (古い値) は b=1 です。これが、実際にはアトミック性と規則性の主な違いです。

上記の定理は、新旧反転のないシングル ライター マルチリーダーの通常レジスタはアトミック レジスタであると述べています。この定理から、R.read() → a →H R.read() → b および R.write(1) →H R.write(0) では、実行がアトミックである場合、π (R.read() → b) =R.write(1) および π (R.read() → a) = R.write(0) になることはできません。上記の定理を証明するには、まずレジスタが安全で通常であり、アトミック性を証明する新旧反転を許可しないことを証明する必要があります。アトミック レジスタの定義により、シングル ライター マルチリーダー アトミック レジスタは通常であり、新旧反転なしのプロパティを満たしています。したがって、必要な証明は、新旧反転のない通常レジスタがアトミックであることを示すことだけです。

さらに、レジスタが正規で新旧反転がない場合の任意の 2 つの読み取り呼び出し (r1 および r2) について (r1 →H r2) ⇒sn(π(r1)) ≤ sn(π(r2))。任意の実行 (M) について、同じ操作呼び出しを含む全順序 (S) が存在します。S は次のように構築されると言えます。書き込み操作の全順序から始めて、次のように読み取り操作を挿入します。まず、読み取り操作 (r) は、関連付けられている書き込み操作 (π(r)) の後に挿入されます。次に、2 つの読み取り操作 (r1、r2) が同じ (sn(r1)=sn(r2)) である場合は、実行で最初に開始する操作を最初に挿入します。S には M のすべての操作呼び出しが含まれるため、S と M は同等であることがわかります。すべての操作はシーケンス番号に基づいて順序付けられるため、全順序がわずかに異なります。さらに、この全順序は、M の実行が M で重複している操作にのみ順序を追加するものです。読み取り操作と書き込み操作の間に重複がない場合、規則性とアトミック性の間に違いはありません。最後に、各読み取り操作は全順序でその前に来る最後の書き込み値を取得するため、S は正当であると述べることができます。したがって、対応する履歴は線形化可能です。この推論は特定の履歴 H に依存しないため、レジスタがアトミックであることを意味します。アトミック性 (線形化可能性) はローカル プロパティであるため、SWMR 通常レジスタのセットは、それぞれが新旧反転なしプロパティを満たすとすぐにアトミックに動作すると述べることができます。

• アトミックセマンティクス
• 安全なセマンティクス

• ランポート、レスリー「プロセス間通信について」 http://research.microsoft.com/en-us/um/people/lamport/pubs/interprocess.pdf (1986)