29 Memory Model

memory consistency model、またはmemory modelは、SharedArrayBufferにbackされたTypedArray instancesへのaccessおよびAtomics object上のmethodsを介して生じるShared Data Block eventsの可能なorderingsをspecifiedする。programにdata races（以下で定義）がない場合、eventsのorderingはsequentially consistentとして現れる、すなわち各agentからのactionsのinterleavingとして現れる。programにdata racesがある場合、shared memory operationsはsequentially inconsistentに見えることがある。例えば、programsはcausality-violating behaviourやその他のastonishmentsを示すことがある。これらのastonishmentsはcompiler transformsおよびCPUsのdesign（例：out-of-order executionおよびspeculation）から生じる。memory modelは、programがsequentially consistent behaviourを示すprecise conditionsと、data racesからreadされ得るpossible valuesの両方をdefineする。すなわち、undefined behaviourは存在しない。

memory modelは、evaluation中にSharedArrayBuffer上のabstract operationsまたはAtomics object上のmethodsによって導入されるMemory eventsに対するrelational constraintsとして定義される。

Note

このsectionは、SharedArrayBuffers上のabstract operationsによって導入されるMemory eventsに関するaxiomatic modelを提供する。強調すべき点として、このmodelは、本仕様の他の部分と異なり、algorithmicallyに表現できない。abstract operationsによるeventsのnondeterministic introductionは、ECMAScript evaluationのoperational semanticsとmemory modelのaxiomatic semanticsとの間のinterfaceである。これらのeventsのsemanticsは、evaluation内のすべてのeventsのgraphsをconsiderすることで定義される。これらはStatic SemanticsでもRuntime Semanticsでもない。demonstrated algorithmic implementationは存在せず、代わりにparticular event graphがallowedまたはdisallowedかをdetermineするconstraintsのsetが存在する。

29.1 Memory Modelの基礎

Shared memory accesses（readsおよびwrites）は、以下で定義されるatomic accessesとdata accessesという2つのgroupsに分けられる。Atomic accessesはsequentially consistentである、すなわちagent cluster内のすべてのagentsによって合意されるeventsのstrict total orderingが存在する。Non-atomic accessesには、すべてのagentsによって合意されるstrict total orderingは存在しない、すなわちunorderedである。

Note 1

release-acquireなど、sequentially consistentより弱くunorderedより強いorderingsはsupportされない。

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

Table 97: ReadSharedMemory Event Fields
Field Name Value Meaning
[[Order]] seq-cst or unordered memory modelによってeventにguaranteedされる最もweakなordering。
[[NoTear]] Boolean このeventが、このeventとequal memory rangeを持つ複数のwrite eventsからreadすることをallowedされるかどうか。
[[Block]] Shared Data Block eventがoperateするblock。
[[ByteIndex]] non-negative integer [[Block]]内のreadのbyte address。
[[ElementSize]] non-negative integer readのsize。
Table 98: WriteSharedMemory Event Fields
Field Name Value Meaning
[[Order]] seq-cst, unordered, or init memory modelによってeventにguaranteedされる最もweakなordering。
[[NoTear]] Boolean このeventが、このeventとequal memory rangeを持つ複数のread eventsからreadされることをallowedされるかどうか。
[[Block]] Shared Data Block eventがoperateするblock。
[[ByteIndex]] non-negative integer [[Block]]内のwriteのbyte address。
[[ElementSize]] non-negative integer writeのsize。
[[Payload]] byte valuesのList 他のeventsによってreadされるbyte valuesのList。
Table 99: ReadModifyWriteSharedMemory Event Fields
Field Name Value Meaning
[[Order]] seq-cst Read-modify-write eventsは常にsequentially consistentである。
[[NoTear]] true Read-modify-write eventsはtearできない。
[[Block]] Shared Data Block eventがoperateするblock。
[[ByteIndex]] non-negative integer [[Block]]内のread-modify-writeのbyte address。
[[ElementSize]] non-negative integer read-modify-writeのsize。
[[Payload]] byte valuesのList [[ModifyOp]]に渡されるbyte valuesのList。
[[ModifyOp]] read-modify-write modification function readされたbyte valuesのListおよび[[Payload]]からmodified byte valuesのListを返すAbstract Closure。

Shared Data Block eventsは、abstract operationsまたはAtomics object上のmethodsによってcandidate execution Agent Events Recordsに導入される。一部のoperationsは、Synchronize eventsも導入する。これらはfieldsを持たず、他のeventsのpermitted orderingsを直接constrainするためだけに存在する。そして最後に、host-specific eventsが存在する。Memory eventは、Shared Data Block event、Synchronize event、またはそのようなhost-specific eventのいずれかである。

Shared Data Block event eのmemory rangeを、e.[[ByteIndex]]（inclusive）からe.[[ByteIndex]] + e.[[ElementSize]]（exclusive）までのinterval内のすべてのintegersのSetとする。2つのeventsのmemory rangesは、eventsが同じ[[Block]]、[[ByteIndex]]、および[[ElementSize]]を持つときequalである。2つのeventsのmemory rangesは、eventsが同じ[[Block]]を持ち、rangesがequalでなく、かつそのintersectionがnon-emptyであるときoverlappingである。2つのeventsのmemory rangesは、eventsが同じ[[Block]]を持たないか、またはそれらのrangesがequalでもoverlappingでもないときdisjointである。

Note 2

考慮されるべきhost-specific synchronizing eventsの例は：SharedArrayBufferをあるagentから別のagentへ送信すること（例：browserにおけるpostMessage）、agentsのstartingおよびstopping、ならびにshared memory以外のchannelsを介したagent cluster内のcommunicationである。particular execution executionについて、それらのeventsはhost-synchronizes-with strict partial orderを介してhostによって提供される。さらに、hostsはis-agent-order-before Relationにparticipateするために、host-specific synchronizing eventsをexecution.[[EventList]]に追加できる。

Eventsは、以下で定義されるrelationsによってcandidate executions内でorderedされる。

29.2 Agent Events Records

Agent Events Recordは、以下のfieldsを持つRecordである。

Table 100: Agent Events Record Fields
Field Name Value Meaning
[[AgentSignifier]] agent signifier このorderingをevaluationのresultとして生じさせたagent。
[[EventList]] Memory eventsのList Eventsはevaluation中にlistへappendされる。
[[AgentSynchronizesWith]] Synchronize eventsのpairsのList operational semanticsによって導入されたSynchronize relationships。

29.3 Chosen Value Records

Chosen Value Recordは、以下のfieldsを持つRecordである。

Table 101: Chosen Value Record Fields
Field Name Value Meaning
[[Event]] Shared Data Block event このchosen valueのために導入されたReadSharedMemoryまたはReadModifyWriteSharedMemory event。
[[ChosenValue]] byte valuesのList evaluation中にnondeterministically chosenされたbytes。

29.4 Candidate Executions

agent clusterのevaluationのcandidate executionは、以下のfieldsを持つRecordである。

Table 102: Candidate Execution Record Fields
Field Name Value Meaning
[[EventsRecords]] Agent Events RecordsのList agentを、evaluation中にappendedされたMemory eventsのListsへmapする。
[[ChosenValues]] Chosen Value RecordsのList ReadSharedMemoryまたはReadModifyWriteSharedMemory eventsを、evaluation中にchosenされたbyte valuesのListへmapする。

empty candidate executionは、そのfieldsがempty Listsであるcandidate execution Recordである。

29.5 Memory ModelのAbstract Operations

29.5.1 EventSet ( execution )

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

  1. eventsをempty Setとする。
  2. execution.[[EventsRecords]]の各Agent Events Record eventsRecordについて、
    1. eventsRecord.[[EventList]]の各Memory event eventについて、
      1. eventをeventsにaddする。
  3. eventsを返す。

29.5.2 SharedDataBlockEventSet ( execution )

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

  1. eventsをempty Setとする。
  2. EventSet(execution)の各Memory event eventについて、
    1. eventがShared Data Block eventなら、eventをeventsにaddする。
  3. eventsを返す。

29.5.3 HostEventSet ( execution )

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

  1. EventSet(execution)のうちSharedDataBlockEventSet(execution)に含まれないすべてのelementsを含むnew Setを返す。

29.5.4 ComposeWriteEventBytes ( execution, byteIndex, writes )

The abstract operation ComposeWriteEventBytes takes arguments execution (a candidate execution), byteIndex (a non-negative integer), and writes (a List of either WriteSharedMemory or ReadModifyWriteSharedMemory events) and returns a List of byte values. It performs the following steps when called:

  1. byteLocationをbyteIndexとする。
  2. bytesReadをnew empty Listとする。
  3. writesの各element writeEventについて、
    1. Assert: writeEventはそのmemory range内にbyteLocationを持つ。
    2. payloadIndexをbyteLocation - writeEvent.[[ByteIndex]]とする。
    3. writeEventがWriteSharedMemory eventなら、
      1. byteをwriteEvent.[[Payload]][payloadIndex]とする。
    4. そうでなければ、
      1. Assert: writeEventはReadModifyWriteSharedMemory eventである。
      2. bytesをValueOfReadEvent(execution, writeEvent)とする。
      3. bytesModifiedをwriteEvent.[[ModifyOp]](bytes, writeEvent.[[Payload]])とする。
      4. byteをbytesModified[payloadIndex]とする。
    5. byteをbytesReadにappendする。
    6. byteLocationをbyteLocation + 1に設定する。
  4. bytesReadを返す。
 Note 1

read-modify-write modification [[ModifyOp]]は、ReadModifyWriteSharedMemory eventsを導入するAtomics object上のfunction propertiesによって与えられる。

 Note 2

このabstract operationは、write eventsのListをbyte valuesのListへcomposeする。これはReadSharedMemoryおよびReadModifyWriteSharedMemory eventsのevent semanticsで使用される。

29.5.5 ValueOfReadEvent ( execution, readEvent )

The abstract operation ValueOfReadEvent takes arguments execution (a candidate execution) and readEvent (a ReadSharedMemory or ReadModifyWriteSharedMemory event) and returns a List of byte values. It performs the following steps when called:

  1. writesをexecutionにおけるreads-bytes-from(readEvent)とする。
  2. Assert: writesは、lengthがreadEvent.[[ElementSize]]にequalなWriteSharedMemoryまたはReadModifyWriteSharedMemory eventsのListである。
  3. ComposeWriteEventBytes(execution, readEvent.[[ByteIndex]], writes)を返す。

29.6 Candidate ExecutionsのRelations

以下のrelationsおよびmathematical functionsは、particular candidate executionにparameterizedされ、そのMemory eventsをorderする。

29.6.1 is-agent-order-before

candidate execution executionについて、そのis-agent-order-before Relationは、以下をsatisfyするMemory events上のleast Relationである。

  • events eventAおよびeventBについて、execution.[[EventsRecords]]内に、eventAとeventBの両方を含むeventsRecord.[[EventList]]を持つ何らかのAgent Events Record eventsRecordがあり、かつeventsRecord.[[EventList]]のList orderにおいてeventAがeventBより前であるなら、eventAはexecutionにおいてeventBのis-agent-order-beforeである。
Note

各agentはevaluation中にper-agent strict total orderでeventsを導入する。これはそれらのstrict total ordersのunionである。

29.6.2 reads-bytes-from

candidate execution executionについて、そのreads-bytes-from functionは、SharedDataBlockEventSet(execution)内のMemory eventsをSharedDataBlockEventSet(execution)内のeventsのListsへmappingするmathematical functionであり、以下のconditionsをsatisfyする。

candidate executionは常にreads-bytes-from functionをadmitする。

29.6.3 reads-from

candidate execution executionについて、そのreads-from Relationは、以下をsatisfyするMemory events上のleast Relationである。

  • events readEventおよびwriteEventについて、SharedDataBlockEventSet(execution)がreadEventとwriteEventの両方を含み、かつexecutionにおけるreads-bytes-from(readEvent)がwriteEventを含むなら、readEventはexecutionにおいてwriteEventからreads-fromする。

29.6.4 host-synchronizes-with

candidate execution executionについて、そのhost-synchronizes-with Relationは、少なくとも以下をsatisfyするhost-provided strict partial order on host-specific Memory eventsである。

  • eventAがexecutionにおいてeventBとhost-synchronizes-withであるなら、HostEventSet(execution)はeventAおよびeventBを含む。
  • executionにおけるhost-synchronizes-withとis-agent-order-beforeのunionにcycleは存在しない。
Note 1

candidate execution execution内の2つのhost-specific events eventAおよびeventBについて、eventAがexecutionにおいてeventBとhost-synchronizes-withであることは、eventAがexecutionにおいてeventBのhappens-beforeであることをimplyする。

 Note 2

このRelationは、hostがHTML workers間のpostMessageなどの追加のsynchronization mechanismsを提供することをallowする。

29.6.5 synchronizes-with

candidate execution executionについて、そのsynchronizes-with Relationは、以下をsatisfyするMemory events上のleast Relationである。

  • events readEventおよびwriteEventについて、readEventがexecutionにおいてwriteEventからreads-fromし、readEvent.[[Order]]がseq-cstであり、writeEvent.[[Order]]がseq-cstであり、かつreadEventとwriteEventがequal memory rangesを持つなら、writeEventはexecutionにおいてreadEventとsynchronizes-withである。
  • execution.[[EventsRecords]]の各element eventsRecordについて、以下がtrueである。
    • events eventAおよびeventBについて、eventsRecord.[[AgentSynchronizesWith]]が(eventA, eventB)を含むなら、eventAはexecutionにおいてeventBとsynchronizes-withである。
  • イベント eventA および eventB について、execution 内で eventA が eventB と host-synchronizes-with する場合、execution 内で eventA は eventB と synchronizes-with する。
Note 1

memory model literatureにおけるconventionにより、candidate execution executionにおいては、read eventsがwrite eventsとsynchronizes-withするのではなく、write eventsがread eventsとsynchronizes-withする。

 Note 2

candidate execution executionにおいて、init eventsはこのRelationにparticipateせず、代わりにhappens-beforeによって直接constrainedされる。

 Note 3

candidate execution executionにおいて、reads-fromによってrelatedされるすべてのseq-cst eventsがsynchronizes-withによってrelatedされるわけではない。equal memory rangesも持つeventsだけがsynchronizes-withによってrelatedされる。

 Note 4

candidate execution execution内のShared Data Block events readEventおよびwriteEventについて、writeEventがreadEventとsynchronizes-withである場合、readEventはwriteEvent以外のwritesからreads-fromすることがある。

29.6.6 happens-before

candidate execution executionについて、そのhappens-before Relationは、以下をsatisfyするMemory events上のleast Relationである。

  • events eventAおよびeventBについて、以下のconditionsのいずれかがtrueなら、eventAはexecutionにおいてeventBのhappens-beforeである。

    • eventAはexecutionにおいてeventBのis-agent-order-beforeである。
    • eventAはexecutionにおいてeventBとsynchronizes-withである。
    • SharedDataBlockEventSet(execution)がeventAとeventBの両方を含み、eventA.[[Order]]がinitであり、かつeventAとeventBがoverlapping memory rangesを持つ。
    • executionにおいて、eventAがeventCのhappens-beforeであり、かつeventCがeventBのhappens-beforeであるようなevent eventCが存在する。
Note

happens-beforeはagent-orderのsupersetであるため、candidate executionはECMAScriptのsingle-thread evaluation semanticsとconsistentである。

29.7 Valid Executionsのプロパティ

29.7.1 Valid Chosen Reads

candidate execution executionは、以下のalgorithmがtrueを返すならvalid chosen readsを持つ。

  1. SharedDataBlockEventSet(execution)の各ReadSharedMemoryまたはReadModifyWriteSharedMemory event readEventについて、
    1. chosenValueRecordを、[[Event]] fieldがreadEventであるexecution.[[ChosenValues]]のelementとする。
    2. chosenValueをchosenValueRecord.[[ChosenValue]]とする。
    3. readValueをValueOfReadEvent(execution, readEvent)とする。
    4. chosenLengthをchosenValue内のelementsの数とする。
    5. readLengthをreadValue内のelementsの数とする。
    6. chosenLength ≠ readLengthなら、
      1. falseを返す。
    7. 0（inclusive）からchosenLength（exclusive）までのinterval内の何らかのinteger iについて、chosenValue[i] ≠ readValue[i]なら、
      1. falseを返す。
  2. trueを返す。

29.7.2 Coherent Reads

candidate execution executionは、以下のalgorithmがtrueを返すならcoherent readsを持つ。

  1. SharedDataBlockEventSet(execution)の各ReadSharedMemoryまたはReadModifyWriteSharedMemory event readEventについて、
    1. writesをexecutionにおけるreads-bytes-from(readEvent)とする。
    2. byteLocationをreadEvent.[[ByteIndex]]とする。
    3. writesの各element writeEventについて、
      1. readEventがexecutionにおいてwriteEventのhappens-beforeであるなら、
        1. falseを返す。
      2. byteLocationをそのmemory range内に持つWriteSharedMemoryまたはReadModifyWriteSharedMemory event valueであって、executionにおいてwriteEventがvalueのhappens-beforeであり、かつvalueがreadEventのhappens-beforeであるものが存在するなら、
        1. falseを返す。
      3. byteLocationをbyteLocation + 1に設定する。
  2. trueを返す。

29.7.3 Tear Free Reads

candidate execution executionは、以下のalgorithmがtrueを返すならtear free readsを持つ。

  1. SharedDataBlockEventSet(execution)の各ReadSharedMemoryまたはReadModifyWriteSharedMemory event readEventについて、
    1. readEvent.[[NoTear]]がtrueなら、
      1. Assert: readEvent.[[ByteIndex]]をreadEvent.[[ElementSize]]でdivideしたremainderは0である。
      2. executionにおいてreadEventがwriteEventからreads-fromし、かつwriteEvent.[[NoTear]]がtrueであるような各Memory event writeEventについて、
        1. readEventとwriteEventがequal memory rangesを持ち、valueとwriteEventがequal memory rangesを持ち、value.[[NoTear]]がtrueであり、writeEventとvalueが同じShared Data Block eventではなく、かつexecutionにおいてreadEventがvalueからreads-fromするようなMemory event valueが存在するなら、
          1. falseを返す。
  2. trueを返す。
 Note

Shared Data Block eventの[[NoTear]] fieldは、そのeventがinteger TypedArrayへのaccessを介して導入されたときtrueであり、floating point TypedArrayまたはDataViewへのaccessを介して導入されたときfalseである。

直観的には、このrequirementは、memory rangeがinteger TypedArrayを介してaligned fashionでaccessされる場合、そのrange上のsingle write eventが、equal rangesを持つ他のwrite eventsとのdata raceにおいて“win”しなければならない、ということを述べている。よりpreciselyには、このrequirementは、aligned read eventが、すべてequal rangesを持つ複数のdifferent write eventsからのbytesでcomposeされたvalueをreadできない、ということを述べている。ただし、aligned read eventがoverlapping rangesを持つ複数のwrite eventsからreadすることは可能である。

29.7.4 Sequentially Consistent Atomics

candidate execution executionについて、is-memory-order-beforeは、以下をsatisfyするEventSet(execution)内のすべてのMemory eventsのstrict total orderである。

  • events eventAおよびeventBについて、eventAがexecutionにおいてeventBのhappens-beforeであるなら、eventAはexecutionにおいてeventBのis-memory-order-beforeである。

  • executionにおいてreadEventがwriteEventからreads-fromするようなevents readEventおよびwriteEventについて、SharedDataBlockEventSet(execution)内にWriteSharedMemoryまたはReadModifyWriteSharedMemory event valueであって、value.[[Order]]がseq-cstであり、writeEventがexecutionにおいてvalueのis-memory-order-beforeであり、valueがexecutionにおいてreadEventのis-memory-order-beforeであり、かつ以下のconditionsのいずれかがtrueであるものは存在しない。

    • writeEventがexecutionにおいてreadEventとsynchronizes-withであり、かつvalueとreadEventがequal memory rangesを持つ。
    • writeEventがreadEventのhappens-beforeであり、かつvalueがexecutionにおいてreadEventのhappens-beforeであり、writeEvent.[[Order]]がseq-cstであり、かつwriteEventとvalueがequal memory rangesを持つ。
    • writeEventがreadEventのhappens-beforeであり、かつwriteEventがexecutionにおいてvalueのhappens-beforeであり、readEvent.[[Order]]がseq-cstであり、かつvalueとreadEventがequal memory rangesを持つ。
    Note 1

    このclauseはさらにequal memory ranges上のseq-cst eventsをconstrainする。

  • SharedDataBlockEventSet(execution)内の各WriteSharedMemoryまたはReadModifyWriteSharedMemory event writeEventについて、writeEvent.[[Order]]がseq-cstなら、equal memory rangeを持ち、writeEventのmemory-order beforeであるReadSharedMemoryまたはReadModifyWriteSharedMemory eventsがSharedDataBlockEventSet(execution)内にinfinite number存在する、ということはない。

    Note 2

    このclauseはagentsに関するforward progress guaranteeと合わせて、equal memory rangeを持つseq-cst writesがfinite time内にseq-cst readsにvisibleになるというliveness conditionをensureする。

candidate executionは、is-memory-order-before Relationをadmitするならsequentially consistent atomicsを持つ。

Note 3

is-memory-order-beforeはEventSet(execution)内のすべてのeventsを含むが、executionにおいてhappens-beforeまたはsynchronizes-withによってconstrainedされていないものは、order内のどこに現れてもallowedされる。

29.7.5 Valid Executions

candidate execution executionは、以下のすべてがtrueであるならvalid execution（または単にexecution）である。

すべてのprogramsには少なくとも1つのvalid executionが存在する。

29.8 Races

execution executionと、SharedDataBlockEventSet(execution)に含まれるevents eventAおよびeventBについて、以下のalgorithmがtrueを返すなら、eventAとeventBはraceにある。

  1. eventAとeventBが同じShared Data Block eventでないなら、
    1. executionにおいてeventAがeventBのhappens-beforeであり、かつeventBがeventAのhappens-beforeである、ということが成り立たないなら、
      1. eventAがWriteSharedMemoryまたはReadModifyWriteSharedMemory eventのいずれかであり、eventBがWriteSharedMemoryまたはReadModifyWriteSharedMemory eventのいずれかであり、かつeventAとeventBがdisjoint memory rangesを持たないなら、
        1. trueを返す。
      2. eventAがexecutionにおいてeventBからreads-fromする、またはeventBがexecutionにおいてeventAからreads-fromするなら、
        1. trueを返す。
  2. falseを返す。

29.9 Data Races

execution executionと、SharedDataBlockEventSet(execution)に含まれるevents eventAおよびeventBについて、以下のalgorithmがtrueを返すなら、eventAとeventBはdata raceにある。

  1. eventAとeventBがexecutionにおいてraceにあるなら、
    1. eventA.[[Order]]がseq-cstでない、またはeventB.[[Order]]がseq-cstでないなら、
      1. trueを返す。
    2. eventAとeventBがoverlapping memory rangesを持つなら、
      1. trueを返す。
  2. falseを返す。

29.10 Data Race Freedom

execution executionは、SharedDataBlockEventSet(execution)内にdata raceにある2つのeventsが存在しないなら、data race freeである。

programは、そのすべてのexecutionsがdata race freeであるならdata race freeである。

memory modelは、data race free programsについて、すべてのeventsのsequential consistencyをguaranteeする。

29.11 Shared Memory Guidelines

Note 1

以下は、shared memoryを扱うECMAScript programmers向けのguidelinesである。

programsはdata race freeに保つこと、すなわち同じmemory location上でconcurrent non-atomic operationsが発生することがimpossibleになるようにすることを推奨する。Data race free programsは、各agentのevaluation semanticsにおける各stepが互いにinterleavedされるinterleaving semanticsを持つ。data race free programsについては、memory modelのdetailsを理解する必要はない。そのdetailsは、より良いECMAScriptを書く助けとなるintuitionを構築する可能性が低い。

より一般には、programがdata race freeでない場合でも、atomic operationsがdata racesに関与せず、raceするoperationsがすべて同じaccess sizeを持つ限り、predictable behaviourを持つことがある。atomicsがracesに関与しないようにarrangeする最も単純な方法は、atomic operationsとnon-atomic operationsによってdifferent memory cellsが使用され、異なるsizesのatomic accessesが同じcellsを同時にaccessするために使用されないことをensureすることである。Effectively、programはshared memoryを可能な限りstrongly typedとして扱うべきである。raceするnon-atomic accessesのorderingおよびtimingに依存することは依然としてできないが、memoryがstrongly typedとして扱われるなら、racing accessesは“tear”しない（それらのvaluesのbitsが混ざらない）。

 Note 2

以下は、shared memoryを使用するprogramsに対するcompiler transformationsを書くECMAScript implementers向けのguidelinesである。

multi-agent program内の各agentのperformanceがsingle-agent settingにおけるperformanceと同じくらい良くなることをensureするために、single-agent settingでvalidなほとんどのprogram transformationsをmulti-agent settingでもallowすることが望ましい。しばしばこれらのtransformationsはjudgeしにくい。ここでは、normativeとして扱われることを意図した（memory modelによってimpliedされる、またはmemory modelがimplyするものよりstrongerであるという意味で）program transformationsに関するいくつかのrulesをoutlineするが、exhaustiveではない可能性が高い。これらのrulesは、is-agent-order-before Relationを構成するMemory eventsのintroductionsにprecedeするprogram transformationsにapplyされることを意図している。

agent-order sliceを、single agentにpertainingするis-agent-order-before Relationのsubsetとする。

read eventのpossible read valuesを、すべてのvalid executionsにわたるそのeventについてのValueOfReadEventのすべてのvaluesのsetとする。

shared memoryがない場合にvalidなagent-order sliceの任意のtransformationは、以下のexceptionsを除き、shared memoryがある場合にもvalidである。

  • Atomics are carved in stone：Program transformationsは、[[Order]]がseq-cstであるShared Data Block eventsをis-agent-order-before Relationからremoveさせてはならず、互いに対してreorderedさせてはならず、また[[Order]]がunorderedであるeventsに対してagent-order slice内でreorderedさせてはならない。

    （実際には、reorderingsの禁止は、compilerに、すべてのseq-cst operationがsynchronizationであり、final is-memory-order-before Relationにincludedされるとassumeすることを強制する。これは通常、inter-agent program analysisがない場合にいずれにせよassumeしなければならないことである。また、calleeのmemory-orderへのeffectsがunknownであるすべてのcallがseq-cst operationsを含む可能性があるとcompilerにassumeさせる。）

  • Reads must be stable：任意のgiven shared memory readは、execution内でsingle valueのみをobserveしなければならない。

    （例えば、program内でsemanticallyにはsingle readであるものが複数回executedされた場合、その後programはreadされたvaluesのうち1つだけをobserveすることをallowedされる。rematerializationとして知られるtransformationはこのruleにviolateする可能性がある。）

  • Writes must be stable：shared memoryへのすべてのobservable writesは、execution内のprogram semanticsからfollowしなければならない。

    （例えば、transformationは、より小さいdatumを書くためにより大きなlocation上のread-modify-write operationsを使用すること、programがwriteできなかったvalueをmemoryにwriteすること、またはreadされたlocationがread後に別のagentによってoverwrittenされた可能性がある場合に、そのlocationへjust-read valueを書き戻すことなどにより、特定のobservable writesをintroduceしてはならない。）

  • Possible read values must be non-empty：Program transformationsは、shared memory readのpossible read valuesをemptyにしてはならない。

    （counterintuitively、このruleはeffectとしてwrites上のtransformationsを制限する。なぜなら、writesはread eventsによってreadされる限りにおいてmemory model内でforceを持つからである。例えば、writesは2つのseq-cst operationsの間でmovedおよびcoalescedされ、時にはreorderedされることがあるが、transformationはlocationをupdatesするすべてのwritesをremoveしてはならない；何らかのwriteはpreservedされなければならない。）

validのままであるtransformationsの例は：同じlocationからの複数のnon-atomic readsをmergeすること、non-atomic readsをreorderすること、speculative non-atomic readsをintroduceすること、同じlocationへの複数のnon-atomic writesをmergeすること、different locationsへのnon-atomic writesをreorderすること、およびterminationに影響する場合でもnon-atomic readsをloopsの外へhoistすること、である。一般に、aliased TypedArraysによりlocationsがdifferentであることをproveしにくくなる点に注意。

 Note 3

以下は、shared memory accessesのためにmachine codeを生成するECMAScript implementers向けのguidelinesである。

memory modelsがARMまたはPowerのものと同程度以上にweakでないarchitecturesについては、non-atomic storesおよびloadsはtarget architecture上のbare storesおよびloadsへcompileしてよい。Atomic storesおよびloadsはsequential consistencyをguaranteeするinstructionsへcompileされてよい。そのようなinstructionsが存在しない場合、bare storeまたはloadの両側にbarriersを配置するなど、memory barriersをemployすることになる。Read-modify-write operationsは、x86上のLOCK-prefixed instructions、ARM上のload-exclusive/store-exclusive instructions、およびPower上のload-link/store-conditional instructionsなど、target architecture上のread-modify-write instructionsへcompileされてよい。

Specifically、memory modelは以下のようなcode generationをallowすることを意図している。

  • program内のすべてのatomic operationはnecessaryであるとassumedされる。
  • Atomic operationsは互いに、またはnon-atomic operationsとrearrangedされない。
  • Functionsは常にatomic operationsをperformするとassumedされる。
  • Atomic operationsは、larger data上のread-modify-write operationsとしては決してimplementedされず、platformがappropriate sizeのatomic operationsを持たない場合にはnon-lock-free atomicsとしてimplementedされる。（すべてのplatformがevery interesting sizeのnormal memory access operationsを持つことは既にassumeしている。）

Naive code generationはこれらのpatternsを使用する：

  • Regular loadsおよびstoresはsingle loadおよびstore instructionsへcompileされる。
  • Lock-free atomic loadsおよびstoresは、full（sequentially consistent）fence、regular loadまたはstore、およびfull fenceへcompileされる。
  • Lock-free atomic read-modify-write accessesは、full fence、atomic read-modify-write instruction sequence、およびfull fenceへcompileされる。
  • Non-lock-free atomicsは、spinlock acquire、full fence、一連のnon-atomic loadおよびstore instructions、full fence、およびspinlock releaseへcompileされる。

そのmappingは、memory range上のatomic operationがnon-atomic writeまたはdifferent sizeのatomic operationとraceしない限りcorrectである。ただし、それで必要十分である：memory modelは、raceにinvolvedしたatomic operationsをeffectively non-atomic statusへdemoteする。一方で、naive mappingはかなりstrongである：atomic operationsをsequentially consistent fencesとして使用することをallowするが、memory modelは実際にはそれをguaranteeしない。

memory modelのconstraintsに従う限り、それらのbasic patternsへのlocal improvementsもallowedされる。例えば：

  • redundant fencesをremoveする明らかなplatform-dependent improvementsが存在する。例えば、x86ではlock-free atomic loadsおよびstoresの周囲のfencesは、storeにfollowingするfenceを除き常にomittedでき、lock-free read-modify-write instructionsにはfenceはneededでない。これらはすべてLOCK-prefixed instructionsを使用するからである。多くのplatformsにはseveral strengthsのfencesがあり、sequential consistencyをdestroyしない特定のcontextsではweaker fencesを使用できる。
  • Most modern platformsは、ECMAScript atomicsによってrequiredされるすべてのdata sizesについてlock-free atomicsをsupportする。non-lock-free atomicsが必要な場合、atomic operationのbodyをsurroundするfencesは通常、lockおよびunlock stepsにfoldできる。non-lock-free atomicsの最も単純なsolutionは、SharedArrayBufferごとにsingle lock wordを持つことである。
  • code analysisを必要とする、よりcomplicatedなplatform-dependent local improvementsも存在する。例えば、back-to-backの2つのfencesはしばしばsingle fenceと同じeffectを持つため、sequence内の2つのatomic operationsのためにcodeがgeneratedされる場合、それらをseparateするfenceはsingle fenceだけでよい。x86では、atomic storesをseparatingするsingle fenceでさえomittedできる。なぜならstoreにfollowingするfenceは、storeをsubsequent loadからseparateするためにのみneededだからである。