29 メモリモデル

メモリ一貫性モデル、またはメモリモデルは、SharedArrayBuffer によって裏付けられた TypedArray インスタンスへのアクセス、および Atomics オブジェクト上のメソッドを介して生じる Shared Data Block イベントの可能な順序付けを指定する。プログラムにデータ競合(以下で定義)がない場合、イベントの順序付けは逐次一貫であるように、すなわち各エージェントからの動作のインターリーブとして現れる。プログラムにデータ競合がある場合、共有メモリ操作は逐次一貫でないように現れ得る。例えば、プログラムは因果性に反する振る舞いやその他の驚くべき振る舞いを示し得る。これらの驚きは、コンパイラ変換および CPU の設計(例えば、アウトオブオーダー実行や投機)から生じる。メモリモデルは、プログラムが逐次一貫な振る舞いを示す正確な条件と、データ競合から読み取られる可能な値の両方を定義する。すなわち、未定義動作は存在しない。

メモリモデルは、評価中に SharedArrayBuffer 上の抽象操作または Atomics オブジェクト上のメソッドによって導入される Memory event に対する関係的制約として定義される。

Note

この節は、SharedArrayBuffer 上の抽象操作によって導入される Memory event に対する公理的モデルを提供する。このモデルは、この仕様の他の部分とは異なり、アルゴリズムとして表現できないことを強調しておく。抽象操作によるイベントの非決定的な導入は、ECMAScript 評価の操作的意味論とメモリモデルの公理的意味論との間のインターフェイスである。これらのイベントの意味論は、評価におけるすべてのイベントのグラフを考慮することによって定義される。これらは Static Semantics でも Runtime Semantics でもない。実証されたアルゴリズム的実装は存在せず、代わりに特定のイベントグラフが許可されるか禁止されるかを決定する制約の集合が存在する。

29.1 メモリモデルの基礎

共有メモリアクセス(読み取りおよび書き込み)は、以下で定義される 2 つのグループ、atomic access と data access に分けられる。atomic access は逐次一貫であり、すなわちエージェントクラスタ内のすべてのエージェントが合意するイベントの厳密な全順序が存在する。非 atomic access には、すべてのエージェントが合意する厳密な全順序は存在しない、すなわち unordered である。

Note 1

release-acquire のような、逐次一貫より弱く unordered より強い順序付けはサポートされない。

Shared Data Block イベントは、ReadSharedMemoryWriteSharedMemory、または ReadModifyWriteSharedMemory Record のいずれかである。read event は、ReadSharedMemory または ReadModifyWriteSharedMemory のいずれかである。write event は、WriteSharedMemory または ReadModifyWriteSharedMemory のいずれかである。

Table 92: ReadSharedMemory イベントのフィールド
フィールド名 意味
[[Order]] seq-cst または unordered そのイベントについてメモリモデルが保証する最も弱い順序付け。
[[NoTear]] Boolean このイベントが、このイベントと等しいメモリ範囲を持つ複数の write event から読み取ることを許されるかどうか。
[[Block]] Shared Data Block そのイベントが操作するブロック。
[[ByteIndex]] 非負整数 [[Block]] 内の読み取りのバイトアドレス。
[[ElementSize]] 非負整数 読み取りのサイズ。
Table 93: WriteSharedMemory イベントのフィールド
フィールド名 意味
[[Order]] seq-cstunordered、または init そのイベントについてメモリモデルが保証する最も弱い順序付け。
[[NoTear]] Boolean このイベントが、このイベントと等しいメモリ範囲を持つ複数の read event から読み取られることを許されるかどうか。
[[Block]] Shared Data Block そのイベントが操作するブロック。
[[ByteIndex]] 非負整数 [[Block]] 内の書き込みのバイトアドレス。
[[ElementSize]] 非負整数 書き込みのサイズ。
[[Payload]] バイト値の List 他のイベントによって読み取られるバイト値の List
Table 94: ReadModifyWriteSharedMemory イベントのフィールド
フィールド名 意味
[[Order]] seq-cst read-modify-write イベントは常に逐次一貫である。
[[NoTear]] true read-modify-write イベントは tear しない。
[[Block]] Shared Data Block そのイベントが操作するブロック。
[[ByteIndex]] 非負整数 [[Block]] 内の read-modify-write のバイトアドレス。
[[ElementSize]] 非負整数 read-modify-write のサイズ。
[[Payload]] バイト値の List [[ModifyOp]] に渡されるバイト値の List
[[ModifyOp]] read-modify-write 変更関数 読み取られたバイト値の List[[Payload]] から変更されたバイト値の List を返す Abstract Closure

Shared Data Block イベントは、抽象操作または Atomics オブジェクト上のメソッドによって candidate execution Agent Events Record に導入される。一部の操作は、Synchronize イベントも導入する。これはフィールドを持たず、他のイベントの許可される順序付けを直接制約するためだけに存在する。最後に、host-specific イベントがある。Memory event は、Shared Data Block イベント、Synchronize イベント、またはそのような host-specific イベントのいずれかである。

Shared Data Block イベント eメモリ範囲を、e.[[ByteIndex]](含む)から e.[[ByteIndex]] + e.[[ElementSize]](含まない)までの区間内のすべての整数の Set とする。2 つのイベントのメモリ範囲は、それらのイベントが同じ [[Block]][[ByteIndex]]、および [[ElementSize]] を持つとき等しい。2 つのイベントのメモリ範囲は、それらのイベントが同じ [[Block]] を持ち、範囲が等しくなく、かつそれらの共通部分が空でないとき重なっている。2 つのイベントのメモリ範囲は、それらのイベントが同じ [[Block]] を持たないか、またはそれらの範囲が等しくも重なってもいないとき、互いに素である。

Note 2

考慮されるべき host-specific synchronizing event の例には、あるエージェントから別のエージェントへ SharedArrayBuffer を送信すること(例えば、ブラウザにおける postMessage による)、エージェントの開始と停止、および共有メモリ以外のチャネルを介したエージェントクラスタ内での通信がある。特定の execution execution について、それらのイベントは host-synchronizes-with strict partial order を介してホストによって提供される。さらに、ホストは is-agent-order-before Relation に参加するために、host-specific synchronizing event を execution.[[EventList]] に追加できる。

イベントは、以下で定義される関係によって candidate execution 内で順序付けられる。

29.2 Agent Events Record

Agent Events Record は、次のフィールドを持つ Record である。

Table 95: Agent Events Record のフィールド
フィールド名 意味
[[AgentSignifier]] agent signifier この順序付けを生じさせた評価を行ったエージェント。
[[EventList]] Memory eventList イベントは評価中にこのリストへ追加される。
[[AgentSynchronizesWith]] Synchronize イベントのペアの List 操作的意味論によって導入される Synchronize 関係。

29.3 Chosen Value Record

Chosen Value Record は、次のフィールドを持つ Record である。

Table 96: Chosen Value Record のフィールド
フィールド名 意味
[[Event]] Shared Data Block イベント この chosen value のために導入された ReadSharedMemory または ReadModifyWriteSharedMemory イベント。
[[ChosenValue]] バイト値の List 評価中に非決定的に選ばれたバイト。

29.4 Candidate Execution

エージェントクラスタの評価のcandidate execution は、次のフィールドを持つ Record である。

Table 97: Candidate Execution Record のフィールド
フィールド名 意味
[[EventsRecords]] Agent Events RecordList エージェントを、評価中に追加された Memory eventList に対応付ける。
[[ChosenValues]] Chosen Value RecordList ReadSharedMemory または ReadModifyWriteSharedMemory イベントを、評価中に選ばれたバイト値の List に対応付ける。

空の candidate execution は、そのフィールドが空の List である candidate execution Record である。

29.5 メモリモデルのための抽象操作

29.5.1 EventSet ( execution )

The abstract operation EventSet takes argument execution (candidate execution) and returns Memory event の Set. It performs the following steps when called:

  1. events を空の Set とする。
  2. execution.[[EventsRecords]] の各 Agent Events Record aer について、次を行う:
    1. aer.[[EventList]] の各 Memory event event について、次を行う:
      1. eventevents に追加する。
  3. events を返す。

29.5.2 SharedDataBlockEventSet ( execution )

The abstract operation SharedDataBlockEventSet takes argument execution (candidate execution) and returns Shared Data Block event の Set. It performs the following steps when called:

  1. events を空の Set とする。
  2. EventSet(execution) の各 Memory event event について、次を行う:
    1. eventShared Data Block イベントならば、eventevents に追加する。
  3. events を返す。

29.5.3 HostEventSet ( execution )

The abstract operation HostEventSet takes argument execution (candidate execution) and returns Memory event の Set. It performs the following steps when called:

  1. EventSet(execution) の要素のうち、SharedDataBlockEventSet(execution) に含まれないすべての要素を含む新しい Set を返す。

29.5.4 ComposeWriteEventBytes ( execution, byteIndex, writes )

The abstract operation ComposeWriteEventBytes takes arguments execution (candidate execution), byteIndex (非負整数), and writes (WriteSharedMemory または ReadModifyWriteSharedMemory イベントの List) and returns バイト値の List. It performs the following steps when called:

  1. byteLocationbyteIndex とする。
  2. bytesRead を新しい空の List とする。
  3. writes の各要素 writeEvent について、次を行う:
    1. Assert: writeEvent はそのメモリ範囲内に byteLocation を持つ。
    2. payloadIndexbyteLocation - writeEvent.[[ByteIndex]] とする。
    3. writeEventWriteSharedMemory イベントであるならば、
      1. bytewriteEvent.[[Payload]][payloadIndex] とする。
    4. そうでなければ、
      1. Assert: writeEventReadModifyWriteSharedMemory イベントである。
      2. bytesValueOfReadEvent(execution, writeEvent) とする。
      3. bytesModifiedwriteEvent.[[ModifyOp]](bytes, writeEvent.[[Payload]]) とする。
      4. bytebytesModified[payloadIndex] とする。
    5. bytebytesRead に追加する。
    6. byteLocationbyteLocation + 1 に設定する。
  4. bytesRead を返す。
Note 1

read-modify-write 変更 [[ModifyOp]] は、ReadModifyWriteSharedMemory イベントを導入する Atomics オブジェクト上の関数プロパティによって与えられる。

Note 2

この抽象操作は、write eventList をバイト値の List に合成する。これは ReadSharedMemory および ReadModifyWriteSharedMemory イベントのイベント意味論で使用される。

29.5.5 ValueOfReadEvent ( execution, readEvent )

The abstract operation ValueOfReadEvent takes arguments execution (candidate execution) and readEvent (ReadSharedMemory または ReadModifyWriteSharedMemory イベント) and returns バイト値の List. It performs the following steps when called:

  1. writesexecution における reads-bytes-from(readEvent) とする。
  2. Assert: writes は、長さが readEvent.[[ElementSize]] と等しい WriteSharedMemory または ReadModifyWriteSharedMemory イベントの List である。
  3. ComposeWriteEventBytes(execution, readEvent.[[ByteIndex]], writes) を返す。

29.6 Candidate Execution の関係

次の関係および数学的関数は、特定の candidate execution によってパラメータ化され、その Memory event を順序付ける。

29.6.1 is-agent-order-before

candidate execution execution について、その is-agent-order-before Relation は、次を満たす Memory event 上の最小の Relation である。

  • イベント eventA および eventB について、execution.[[EventsRecords]] 内にある Agent Events Record aer が存在し、aer.[[EventList]]eventAeventB の両方を含み、かつ aer.[[EventList]]List 順序において eventAeventB より前である場合、execution において eventAeventB より is-agent-order-before である。
Note

各エージェントは、評価中にエージェントごとの厳密な全順序でイベントを導入する。これはそれらの厳密な全順序の和集合である。

29.6.2 reads-bytes-from

candidate execution execution について、その reads-bytes-from 関数は、SharedDataBlockEventSet(execution) 内の Memory event を、SharedDataBlockEventSet(execution) 内のイベントの List に写像する数学的関数であり、次の条件を満たす。

candidate execution は常に reads-bytes-from 関数を認める。

29.6.3 reads-from

candidate execution execution について、その reads-from Relation は、次を満たす Memory event 上の最小の Relation である。

  • イベント readEvent および writeEvent について、SharedDataBlockEventSet(execution) が readEventwriteEvent の両方を含み、かつ execution における reads-bytes-from(readEvent) が writeEvent を含む場合、execution において readEventwriteEvent から reads-from する。

29.6.4 host-synchronizes-with

candidate execution execution について、その host-synchronizes-with Relation は、少なくとも次を満たす host-specific Memory event 上の、ホストが提供する strict partial order である。

  • execution において eventAeventB と host-synchronizes-with するならば、HostEventSet(execution) は eventAeventB を含む。
  • execution において host-synchronizes-with と is-agent-order-before の和集合に cycle は存在しない。
Note 1

candidate execution execution 内の 2 つの host-specific イベント eventA および eventB について、execution において eventAeventB と host-synchronizes-with することは、execution において eventAeventB より happens-before であることを含意する。

Note 2

この Relation により、ホストは HTML worker 間の postMessage などの追加の同期機構を提供できる。

29.6.5 synchronizes-with

candidate execution execution について、その synchronizes-with Relation は、次を満たす Memory event 上の最小の Relation である。

  • イベント readEvent および writeEvent について、execution において readEventwriteEvent から reads-from し、readEvent.[[Order]]seq-cst であり、writeEvent.[[Order]]seq-cst であり、かつ readEventwriteEvent が等しいメモリ範囲を持つ場合、execution において writeEventreadEvent と synchronizes-with する。
  • execution.[[EventsRecords]] の各要素 eventsRecord について、次が真である。
    • イベント eventA および eventB について、eventsRecord.[[AgentSynchronizesWith]] が (eventA, eventB) を含む場合、execution において eventAeventB と synchronizes-with する。
  • イベント eventA および eventB について、execution.[[HostSynchronizesWith]] が (eventA, eventB) を含む場合、execution において eventAeventB と synchronizes-with する。
Note 1

メモリモデル文献における慣例により、candidate execution execution においては、read eventwrite event と synchronizes-with するのではなく、write eventread event と synchronizes-with する。

Note 2

candidate execution execution において、init イベントはこの Relation に参加せず、代わりに happens-before によって直接制約される。

Note 3

candidate execution execution において、reads-from によって関連付けられるすべての seq-cst イベントが synchronizes-with によって関連付けられるわけではない。等しいメモリ範囲も持つイベントのみが synchronizes-with によって関連付けられる。

Note 4

candidate execution execution 内の Shared Data Block イベント readEvent および writeEvent について、writeEventreadEvent と synchronizes-with する場合、readEventwriteEvent 以外の write から reads-from してよい。

29.6.6 happens-before

candidate execution execution について、その happens-before Relation は、次を満たす Memory event 上の最小の Relation である。

  • イベント eventA および eventB について、次の条件のいずれかが真である場合、execution において eventAeventB より happens-before である。

    • execution において eventAeventB より is-agent-order-before である。
    • execution において eventAeventBsynchronizes-with する。
    • SharedDataBlockEventSet(execution) が eventAeventB の両方を含み、eventA.[[Order]]init であり、かつ eventAeventB が重なっているメモリ範囲を持つ。
    • execution において eventAeventC より happens-before であり、かつ eventCeventB より happens-before であるようなイベント eventC が存在する。
Note

happens-before は agent-order の上位集合であるため、candidate execution は ECMAScript の単一スレッド評価意味論と一貫している。

29.7 Valid Execution の性質

29.7.1 Valid Chosen Reads

candidate execution execution は、次のアルゴリズムが true を返すならば valid chosen reads を持つ。

  1. SharedDataBlockEventSet(execution) の各 ReadSharedMemory または ReadModifyWriteSharedMemory イベント readEvent について、次を行う:
    1. chosenValueRecord を、[[Event]] フィールドが readEvent である execution.[[ChosenValues]] の要素とする。
    2. chosenValuechosenValueRecord.[[ChosenValue]] とする。
    3. readValueValueOfReadEvent(execution, readEvent) とする。
    4. chosenLenchosenValue 内の要素数とする。
    5. readLenreadValue 内の要素数とする。
    6. chosenLenreadLen ならば、
      1. false を返す。
    7. 0(含む)から chosenLen(含まない)までの区間内のある整数 i について chosenValue[i] ≠ readValue[i] であるならば、
      1. false を返す。
  2. true を返す。

29.7.2 Coherent Reads

candidate execution execution は、次のアルゴリズムが true を返すならば coherent reads を持つ。

  1. SharedDataBlockEventSet(execution) の各 ReadSharedMemory または ReadModifyWriteSharedMemory イベント readEvent について、次を行う:
    1. writesexecution における reads-bytes-from(readEvent) とする。
    2. byteLocationreadEvent.[[ByteIndex]] とする。
    3. writes の各要素 writeEvent について、次を行う:
      1. execution において readEventwriteEvent より happens-before であるならば、
        1. false を返す。
      2. byteLocation をそのメモリ範囲内に持つ WriteSharedMemory または ReadModifyWriteSharedMemory イベント value が存在し、execution において writeEventvalue より happens-before であり、かつ valuereadEvent より happens-before であるならば、
        1. false を返す。
      3. byteLocationbyteLocation + 1 に設定する。
  2. true を返す。

29.7.3 Tear Free Reads

candidate execution execution は、次のアルゴリズムが true を返すならば tear free reads を持つ。

  1. SharedDataBlockEventSet(execution) の各 ReadSharedMemory または ReadModifyWriteSharedMemory イベント readEvent について、次を行う:
    1. readEvent.[[NoTear]]true であるならば、
      1. Assert: readEvent.[[ByteIndex]]readEvent.[[ElementSize]] で割った余りは 0 である。
      2. execution において readEventwriteEvent から reads-from し、かつ writeEvent.[[NoTear]]true である各 Memory event writeEvent について、次を行う:
        1. readEventwriteEvent が等しいメモリ範囲を持ち、かつ valuewriteEvent が等しいメモリ範囲を持ち、value.[[NoTear]]true であり、writeEventvalue が同じ Shared Data Block イベントではなく、かつ execution において readEventvalue から reads-from するような Memory event value が存在するならば、
          1. false を返す。
  2. true を返す。
Note

Shared Data Block イベント[[NoTear]] フィールドは、そのイベントが整数 TypedArray へのアクセスを介して導入された場合に true であり、浮動小数点 TypedArray または DataView へのアクセスを介して導入された場合に false である。

直感的には、この要件は、メモリ範囲が整数 TypedArray を介してアラインされた方法でアクセスされる場合、等しい範囲を持つ他の write event とのデータ競合において、その範囲上の単一の write event が「勝た」なければならないことを述べている。より正確には、この要件は、アラインされた read event が、すべて等しい範囲を持つ複数の異なる write event からのバイトで構成された値を読み取ることができないことを述べている。ただし、アラインされた read event が、重なり合う範囲を持つ複数の write event から読み取ることは可能である。

29.7.4 逐次一貫 Atomic

candidate execution execution について、is-memory-order-beforeEventSet(execution) 内のすべての Memory eventstrict total order であり、次を満たす。

  • イベント eventA および eventB について、execution において eventAeventB より happens-before である場合、execution において eventAeventB より is-memory-order-before である。
  • execution において readEventwriteEvent から reads-from するようなイベント readEvent および writeEvent について、SharedDataBlockEventSet(execution) 内に、value.[[Order]]seq-cst であり、execution において writeEventvalue より is-memory-order-before であり、valuereadEvent より is-memory-order-before であり、かつ次の条件のいずれかが真であるような WriteSharedMemory または ReadModifyWriteSharedMemory イベント value は存在しない。

    • execution において writeEventreadEventsynchronizes-with し、かつ valuereadEvent が等しいメモリ範囲を持つ。
    • execution において writeEventreadEvent より happens-before であり、かつ valuereadEvent より happens-before であり、writeEvent.[[Order]]seq-cst であり、かつ writeEventvalue が等しいメモリ範囲を持つ。
    • execution において writeEventreadEvent より happens-before であり、かつ writeEventvalue より happens-before であり、readEvent.[[Order]]seq-cst であり、かつ valuereadEvent が等しいメモリ範囲を持つ。
    Note 1

    この節はさらに、等しいメモリ範囲上の seq-cst イベントを制約する。

  • SharedDataBlockEventSet(execution) 内の各 WriteSharedMemory または ReadModifyWriteSharedMemory イベント writeEvent について、writeEvent.[[Order]]seq-cst であるならば、等しいメモリ範囲を持ち、かつ writeEvent より memory-order before である ReadSharedMemory または ReadModifyWriteSharedMemory イベントが SharedDataBlockEventSet(execution) 内に無限個存在する、ということはない。

    Note 2

    この節は、エージェントに対する forward progress 保証とともに、等しいメモリ範囲を持つ seq-cst write が有限時間で seq-cst read に見えるようになるという liveness 条件を保証する。

candidate execution は、is-memory-order-before Relation を認める場合、sequentially consistent atomics を持つ。

Note 3

is-memory-order-before は EventSet(execution) 内のすべてのイベントを含むが、execution において happens-before または synchronizes-with によって制約されないイベントは、その順序のどこに現れてもよい。

29.7.5 Valid Executions

candidate execution execution は、次のすべてが真である場合、valid execution(または単に execution)である。

  • ホストが execution に対して host-synchronizes-with Relation を提供する。
  • executionstrict partial order である happens-before Relation を認める。
  • execution は valid chosen reads を持つ。
  • execution は coherent reads を持つ。
  • execution は tear free reads を持つ。
  • execution は sequentially consistent atomics を持つ。

すべてのプログラムは少なくとも 1 つの valid execution を持つ。

29.8 Races

execution execution および SharedDataBlockEventSet(execution) に含まれるイベント eventAeventB について、次のアルゴリズムが true を返すならば、eventAeventBrace状態にある。

  1. eventAeventB が同じ Shared Data Block イベントでないならば、
    1. execution において eventAeventB より happens-before であり、かつ eventBeventA より happens-before である、ということが成り立たないならば、
      1. eventAWriteSharedMemory または ReadModifyWriteSharedMemory イベントのいずれかであり、eventBWriteSharedMemory または ReadModifyWriteSharedMemory イベントのいずれかであり、かつ eventAeventB が互いに素なメモリ範囲を持たない場合、
        1. true を返す。
      2. execution において eventAeventB から reads-from する、または eventBeventA から reads-from するならば、
        1. true を返す。
  2. false を返す。

29.9 Data Races

execution execution および SharedDataBlockEventSet(execution) に含まれるイベント eventAeventB について、次のアルゴリズムが true を返すならば、eventAeventBdata race状態にある。

  1. execution において eventAeventBrace 状態にあるならば、
    1. eventA.[[Order]]seq-cst でないか、または eventB.[[Order]]seq-cst でないならば、
      1. true を返す。
    2. eventAeventB が重なり合うメモリ範囲を持つならば、
      1. true を返す。
  2. false を返す。

29.10 Data Race Freedom

execution execution は、SharedDataBlockEventSet(execution) 内に data race 状態にある 2 つのイベントが存在しない場合、data race free である。

プログラムは、そのすべての execution が data race free である場合、data race free である。

メモリモデルは、data race free プログラムについて、すべてのイベントの逐次一貫性を保証する。

29.11 共有メモリの指針

Note 1

以下は、共有メモリを扱う ECMAScript プログラマーのための指針である。

プログラムを data race free に保つこと、すなわち同じメモリロケーションに対する並行する非 atomic 操作が存在し得ないようにすることを推奨する。Data race free プログラムは、各エージェントの評価意味論における各ステップが互いにインターリーブされるインターリーブ意味論を持つ。Data race free プログラムについては、メモリモデルの詳細を理解する必要はない。その詳細が、ECMAScript をよりよく書くための直感を構築する可能性は低い。

より一般に、プログラムが data race free でなくても、atomic 操作がどの data race にも関与せず、競合する操作がすべて同じアクセスサイズを持つ限り、予測可能な振る舞いを持ち得る。atomic が race に関与しないようにする最も単純な方法は、atomic 操作と非 atomic 操作で異なるメモリセルを使用し、異なるサイズの atomic access が同じセルへ同時にアクセスするために使用されないようにすることである。実質的に、プログラムは共有メモリを可能な限り強く型付けされたものとして扱うべきである。競合する非 atomic access の順序付けやタイミングに依存することは依然としてできないが、メモリが強く型付けされたものとして扱われるならば、競合する access は「tear」しない(その値のビットが混ざらない)。

Note 2

以下は、共有メモリを使用するプログラムに対するコンパイラ変換を書く ECMAScript 実装者のための指針である。

単一エージェント設定で有効なほとんどのプログラム変換を、マルチエージェント設定でも許可することが望ましい。これは、マルチエージェントプログラム内の各エージェントの性能が単一エージェント設定と同程度に良好であることを保証するためである。しばしば、これらの変換は判断が難しい。ここでは、(メモリモデルによって含意される、またはメモリモデルが含意するものより強いという意味で)規範的であることを意図しているが、おそらく網羅的ではない、プログラム変換に関するいくつかの規則を概説する。これらの規則は、is-agent-order-before Relation を構成する Memory event の導入に先立つプログラム変換に適用されることを意図している。

agent-order slice を、単一のエージェントに関係する is-agent-order-before Relation の部分集合とする。

read eventpossible read valuesを、そのイベントについて、すべての valid execution にわたる ValueOfReadEvent のすべての値の集合とする。

共有メモリが存在しない場合に有効な agent-order slice の任意の変換は、次の例外を除き、共有メモリが存在する場合にも有効である。

  • Atomics are carved in stone:プログラム変換は、[[Order]]seq-cst である Shared Data Block イベントis-agent-order-before Relation から取り除いたり、それらを互いに対して並べ替えたり、エージェント順序スライス内で [[Order]]unordered であるイベントに対して並べ替えたりしてはならない。

    (実際には、並べ替えの禁止により、コンパイラはすべての seq-cst 操作が同期であり、最終的な is-memory-order-before Relation に含まれると仮定せざるを得なくなる。これは、エージェント間プログラム解析がない場合には、通常いずれにせよ仮定しなければならないことである。また、メモリ順序への効果が不明な呼び出し先を持つすべての呼び出しが seq-cst 操作を含み得ると仮定することもコンパイラに強制する。)

  • Reads must be stable:任意の与えられた共有メモリ読み取りは、1 回の execution において単一の値のみを観測しなければならない。

    (例えば、プログラム内で意味論的に単一の読み取りであるものが複数回実行された場合、その後プログラムは読み取られた値のうち 1 つだけを観測することが許される。rematerialization と呼ばれる変換はこの規則に違反し得る。)

  • Writes must be stable:共有メモリへのすべての観測可能な書き込みは、execution におけるプログラム意味論から従わなければならない。

    (例えば、変換は、より小さいデータを書き込むためにより大きなロケーション上の read-modify-write 操作を使用すること、プログラムが書き込めなかった値をメモリに書き込むこと、または読み取られたロケーションが読み取り後に別のエージェントによって上書きされ得た場合に、読み取ったばかりの値をそのロケーションへ書き戻すことなど、特定の観測可能な書き込みを導入してはならない。)

  • Possible read values must be non-empty:プログラム変換は、共有メモリ読み取りの possible read values を空にしてはならない。

    (直感に反するが、この規則は、read event によって読み取られる限りで write がメモリモデルにおいて効力を持つため、実質的に write に対する変換を制限する。例えば、write は移動および併合され、時には 2 つの seq-cst 操作の間で並べ替えられることもあるが、その変換はあるロケーションを更新するすべての write を取り除いてはならず、何らかの write が保持されなければならない。)

有効なままである変換の例には、同じロケーションからの複数の非 atomic read のマージ、非 atomic read の並べ替え、投機的な非 atomic read の導入、同じロケーションへの複数の非 atomic write のマージ、異なるロケーションへの非 atomic write の並べ替え、および終了性に影響しても非 atomic read をループ外へ巻き上げることがある。一般に、エイリアスされた TypedArray はロケーションが異なることを証明することを難しくする点に注意。

Note 3

以下は、共有メモリアクセスのための機械語コードを生成する ECMAScript 実装者のための指針である。

ARM または Power のメモリモデル以上に弱くないメモリモデルを持つアーキテクチャでは、非 atomic store および load はターゲットアーキテクチャ上の裸の store および load にコンパイルされてよい。Atomic store および load は、逐次一貫性を保証する命令へコンパイルされてよい。そのような命令が存在しない場合、裸の store または load の両側にバリアを置くなどして、メモリバリアが使用されるべきである。Read-modify-write 操作は、ターゲットアーキテクチャ上の read-modify-write 命令、例えば x86 上の LOCK プレフィックス付き命令、ARM 上の load-exclusive/store-exclusive 命令、および Power 上の load-link/store-conditional 命令にコンパイルされてよい。

具体的には、メモリモデルは次のようなコード生成を許可することを意図している。

  • プログラム内のすべての atomic 操作は必要であると仮定される。
  • Atomic 操作は、互いに対しても非 atomic 操作に対しても決して並べ替えられない。
  • 関数は常に atomic 操作を実行するものと仮定される。
  • Atomic 操作は、より大きなデータに対する read-modify-write 操作として実装されることはなく、プラットフォームが適切なサイズの atomic 操作を持たない場合は非 lock-free atomic として実装される。(すべてのプラットフォームが、重要なすべてのサイズの通常のメモリアクセス操作を持つことは既に仮定している。)

単純なコード生成では、次のパターンを使用する。

  • 通常の load および store は、単一の load 命令および store 命令にコンパイルされる。
  • Lock-free atomic load および store は、完全な(逐次一貫な)fence、通常の load または store、および完全な fence にコンパイルされる。
  • Lock-free atomic read-modify-write access は、完全な fence、atomic read-modify-write 命令列、および完全な fence にコンパイルされる。
  • 非 lock-free atomic は、spinlock acquire、完全な fence、一連の非 atomic load および store 命令、完全な fence、および spinlock release にコンパイルされる。

この写像は、あるメモリ範囲上の atomic 操作が非 atomic write や異なるサイズの atomic 操作と race しない限り正しい。ただし、必要なのはそれだけである。メモリモデルは、race に関与する atomic 操作を実質的に非 atomic 状態に降格する。一方で、単純な写像は非常に強い。これは、atomic 操作を逐次一貫 fence として使用することを許すが、メモリモデルは実際にはそれを保証していない。

これらの基本パターンへの局所的な改善も、メモリモデルの制約に従う限り許可される。例えば:

  • 冗長な fence を取り除く、明らかなプラットフォーム依存の改善がある。例えば、x86 では、lock-free atomic load および store の周囲の fence は、store 後の fence を除き常に省略でき、lock-free read-modify-write 命令には fence が不要である。これらはすべて LOCK プレフィックス付き命令を使用するためである。多くのプラットフォームには複数の強度の fence があり、特定の文脈では逐次一貫性を壊すことなくより弱い fence を使用できる。
  • ほとんどの現代的なプラットフォームは、ECMAScript atomics が要求するすべてのデータサイズについて lock-free atomics をサポートしている。非 lock-free atomic が必要な場合、atomic 操作本体を囲む fence は通常 lock および unlock 手順に畳み込める。非 lock-free atomics の最も単純な解決策は、SharedArrayBuffer ごとに単一の lock word を持つことである。
  • より複雑なプラットフォーム依存の局所的改善もあり、それには何らかのコード解析が必要である。例えば、連続する 2 つの fence はしばしば単一の fence と同じ効果を持つため、2 つの atomic 操作が連続してコード生成される場合、それらの間を隔てる fence は 1 つだけでよい。x86 では、atomic store を隔てる単一の fence でさえ省略できる。store 後の fence は、その store を後続の load から分離するためにのみ必要であるためである。