プログラムのロジックとセマンティクスは、シーケンシャルの構成について親切に説明してくれます。 (𝑆1; 𝑆2) を実行する場合、最初に 𝑆1 を実行してから 𝑆2 を実行します。しかし、パフォーマンスを向上するために、プロセッサは命令を記述された順番と関係なく (アウトオブオーダー) 実行し、コンパイラーはさらにより劇的にプログラムを並べ替えます。設計上、シングルスレッドのシステムではこれらの並べ替えは観測できません。しかし、マルチスレッドのシステムでは可能であるため、実行順序についての理解が大幅に難しくなります。結果として生じる混乱を理解しようとすることは、正式には「リラックスメモリモデル」として知られています。

以前のモデルでは、シーケンシャルの構成に直接対応したり、プロセッサおよびコンパイラーを過度に制限したり、実際には観測不可能な、意味をなさないどこからともなく発生する動作を許可することはできませんでした。最新のハードウェアをターゲットにしながらシーケンシャル構成をサポートするために、標準のイベントベースのアプローチを述語変換の前提条件およびファミリーで強化します。(𝑆1; 𝑆2) の意味を計算する場合、𝑆2 からのイベント 𝑒 に適用される述語変換は、𝑒 が依存する 𝑆1 でのイベントセットに基づいて選択されます。

• プロジェクトのリポジトリ