Programming Languages
「リーキー・セミコロン」
Author
Venue
ACMプログラミング言語会議 2021 論文集
Abstract
プログラム論理と意味論は、逐次合成について心地よい物語を語っている。すなわち、(S1; S2) を実行する際、まず S1 を実行し、次に S2 を実行するというものだ。しかし、パフォーマンスを向上させるため、プロセッサは命令を順不同で実行し、コンパイラはプログラムの順序をさらに劇的に再配置する。設計上、シングルスレッドシステムではこうした再配置を観察することはできないが、マルチスレッドシステムでは観察可能であり、その結果、物語は著しく不快なものとなる。 その結果生じる混乱を理解しようとする形式的な試みは、「緩和されたメモリモデル」として知られている。従来のモデルは、逐次合成を直接扱えていないか、プロセッサやコンパイラに過度な制約を課しているか、あるいは実際には観測不可能な、非現実的な「空想的な」挙動を許容しているかのいずれかである。現代のハードウェアを対象としつつ逐次合成をサポートするため、我々は標準的なイベントベースのアプローチを、前提条件と述語変換器のファミリーによって拡張する。 (S1;S2) の意味を計算する際、S2 からのイベント e の前提条件に適用される述語変換器は、e が依存する S1 内のイベントの集合に基づいて選択される。我々は、このアプローチを 2 つの既存のメモリモデルに適用する。
