Skip to content

Commit 1bf3c74

Browse files
sygsyg
committed
Add memory model changes
1 parent 29962b7 commit 1bf3c74

File tree

1 file changed

+213
-0
lines changed

1 file changed

+213
-0
lines changed

‎spec/index.html

+213
Original file line numberDiff line numberDiff line change
@@ -1056,4 +1056,217 @@ <h1>Runtime Semantics: Evaluation</h1>
10561056
</emu-clause>
10571057
</ins>
10581058
</emu-clause>
1059+
1060+
<emu-clause id="sec-changes-to-memory-model">
1061+
<h1>Changes to the Memory Model</h1>
1062+
<emu-clause id="sec-memory-model-fundamentals">
1063+
<h1>Memory Model Fundamentals</h1>
1064+
<p>Shared memory accesses (reads and writes) are divided into two groups, atomic accesses and data accesses, defined below. Atomic accesses are sequentially consistent, i.e., there is a strict total ordering of events agreed upon by all agents in an agent cluster. Non-atomic accesses do not have a strict total ordering agreed upon by all agents, i.e., unordered.</p>
1065+
<emu-note>
1066+
<p>No orderings weaker than sequentially consistent and stronger than unordered, such as release-acquire, are supported.</p>
1067+
</emu-note>
1068+
<ins class="block">
1069+
<p>A <dfn variants="Shared Memory Storage Records">Shared Memory Storage Record</dfn> is either a <dfn>SharedBlockStorage</dfn> or <dfn>SharedStructStorage</dfn> Record.</p>
1070+
1071+
<emu-table id="table-sharedblockstorage-fields" caption="SharedBlockStorage Fields">
1072+
<table>
1073+
<thead>
1074+
<tr>
1075+
<th>Field Name</th>
1076+
<th>Value</th>
1077+
<th>Meaning</th>
1078+
</tr>
1079+
<tr>
1080+
<td>[[Block]]</td>
1081+
<td>a Shared Data Block</td>
1082+
<td>The block the event operates on.</td>
1083+
</tr>
1084+
<tr>
1085+
<td>[[ByteIndex]]</td>
1086+
<td>a non-negative integer</td>
1087+
<td>The byte address of the access in [[Block]].</td>
1088+
</tr>
1089+
<tr>
1090+
<td>[[ElementSize]]</td>
1091+
<td>a non-negative integer</td>
1092+
<td>The size of the access.</td>
1093+
</tr>
1094+
</thead>
1095+
</table>
1096+
</emu-table>
1097+
1098+
<emu-table id="table-sharedstructstorage-fields" caption="SharedStructStorage Fields">
1099+
<table>
1100+
<thead>
1101+
<tr>
1102+
<th>Field Name</th>
1103+
<th>Value</th>
1104+
<th>Meaning</th>
1105+
</tr>
1106+
<tr>
1107+
<td>[[Struct]]</td>
1108+
<td>a Shared Struct</td>
1109+
<td>The shared struct the event operates on.</td>
1110+
</tr>
1111+
<tr>
1112+
<td>[[Field]]</td>
1113+
<td>a property key</td>
1114+
<td>The field that is accessed in [[Struct]].</td>
1115+
</tr>
1116+
</thead>
1117+
</table>
1118+
</emu-table>
1119+
</ins>
1120+
1121+
<p>A <dfn variants="Shared Data Block events">Shared Data Block event</dfn> is either a <dfn>ReadSharedMemory</dfn>, <dfn>WriteSharedMemory</dfn>, or <dfn>ReadModifyWriteSharedMemory</dfn> Record.</p>
1122+
1123+
<emu-table id="table-readsharedmemory-fields" caption="ReadSharedMemory Event Fields">
1124+
<table>
1125+
<thead>
1126+
<tr>
1127+
<th>Field Name</th>
1128+
<th>Value</th>
1129+
<th>Meaning</th>
1130+
</tr>
1131+
</thead>
1132+
<tr>
1133+
<td>[[Order]]</td>
1134+
<td>~seq-cst~ or ~unordered~</td>
1135+
<td>The weakest ordering guaranteed by the memory model for the event.</td>
1136+
</tr>
1137+
<tr>
1138+
<td>[[NoTear]]</td>
1139+
<td>a Boolean</td>
1140+
<td>Whether this event is allowed to read from multiple write events with equal range as this event.</td>
1141+
</tr>
1142+
<tr>
1143+
<td><del>[[Block]]</del></td>
1144+
<td><del>a Shared Data Block</del></td>
1145+
<td><del>The block the event operates on.</del></td>
1146+
</tr>
1147+
<tr>
1148+
<td><del>[[ByteIndex]]</del></td>
1149+
<td><del>a non-negative integer</del></td>
1150+
<td><del>The byte address of the read in [[Block]].</del></td>
1151+
</tr>
1152+
<tr>
1153+
<td><del>[[ElementSize]]</del></td>
1154+
<td><del>a non-negative integer</del></td>
1155+
<td><del>The size of the read.</del></td>
1156+
</tr>
1157+
<tr>
1158+
<td><ins>[[Storage]]</ins></td>
1159+
<td><ins>a Shared Memory Storage Record</ins></td>
1160+
<td><ins>The storage of memory that is read.</ins></td>
1161+
</tr>
1162+
</table>
1163+
</emu-table>
1164+
1165+
<emu-table id="table-writesharedmemory-fields" caption="WriteSharedMemory Event Fields">
1166+
<table>
1167+
<thead>
1168+
<tr>
1169+
<th>Field Name</th>
1170+
<th>Value</th>
1171+
<th>Meaning</th>
1172+
</tr>
1173+
</thead>
1174+
<tr>
1175+
<td>[[Order]]</td>
1176+
<td>~seq-cst~, ~unordered~, or ~init~</td>
1177+
<td>The weakest ordering guaranteed by the memory model for the event.</td>
1178+
</tr>
1179+
<tr>
1180+
<td>[[NoTear]]</td>
1181+
<td>a Boolean</td>
1182+
<td>Whether this event is allowed to be read from multiple read events with equal range as this event.</td>
1183+
</tr>
1184+
<tr>
1185+
<td><del>[[Block]]</del></td>
1186+
<td><del>a Shared Data Block</del></td>
1187+
<td><del>The block the event operates on.</del></td>
1188+
</tr>
1189+
<tr>
1190+
<td><del>[[ByteIndex]]</del></td>
1191+
<td><del>a non-negative integer</del></td>
1192+
<td><del>The byte address of the write in [[Block]].</del></td>
1193+
</tr>
1194+
<tr>
1195+
<td><del>[[ElementSize]]</del></td>
1196+
<td><del>a non-negative integer</del></td>
1197+
<td><del>The size of the write.</del></td>
1198+
</tr>
1199+
<tr>
1200+
<td><ins>[[Storage]]</ins></td>
1201+
<td><ins>a Shared Memory Storage Record</ins></td>
1202+
<td><ins>The storage of memory that is written.</ins></td>
1203+
</tr>
1204+
<tr>
1205+
<td>[[Payload]]</td>
1206+
<td>a List of byte values</td>
1207+
<td>The List of byte values to be read by other events.</td>
1208+
</tr>
1209+
</table>
1210+
</emu-table>
1211+
1212+
<emu-table id="table-rmwsharedmemory-fields" caption="ReadModifyWriteSharedMemory Event Fields">
1213+
<table>
1214+
<thead>
1215+
<tr>
1216+
<th>Field Name</th>
1217+
<th>Value</th>
1218+
<th>Meaning</th>
1219+
</tr>
1220+
</thead>
1221+
<tr>
1222+
<td>[[Order]]</td>
1223+
<td>~seq-cst~</td>
1224+
<td>Read-modify-write events are always sequentially consistent.</td>
1225+
</tr>
1226+
<tr>
1227+
<td>[[NoTear]]</td>
1228+
<td>*true*</td>
1229+
<td>Read-modify-write events cannot tear.</td>
1230+
</tr>
1231+
<tr>
1232+
<td><del>[[Block]]</del></td>
1233+
<td><del>a Shared Data Block</del></td>
1234+
<td><del>The block the event operates on.</del></td>
1235+
</tr>
1236+
<tr>
1237+
<td><del>[[ByteIndex]]</del></td>
1238+
<td><del>a non-negative integer</del></td>
1239+
<td><del>The byte address of the read-modify-write in [[Block]].</del></td>
1240+
</tr>
1241+
<tr>
1242+
<td><del>[[ElementSize]]</del></td>
1243+
<td><del>a non-negative integer</del></td>
1244+
<td><del>The size of the read-modify-write.</del></td>
1245+
</tr>
1246+
<tr>
1247+
<td><ins>[[Storage]]</ins></td>
1248+
<td><ins>a Shared Memory Storage Record</ins></td>
1249+
<td><ins>The storage of memory of the read-modify-write.</ins></td>
1250+
</tr>
1251+
<tr>
1252+
<td>[[Payload]]</td>
1253+
<td>a List of byte values</td>
1254+
<td>The List of byte values to be passed to [[ModifyOp]].</td>
1255+
</tr>
1256+
<tr>
1257+
<td>[[ModifyOp]]</td>
1258+
<td>a read-modify-write modification function</td>
1259+
<td>An abstract closure that returns a modified List of byte values from a read List of byte values and [[Payload]].</td>
1260+
</tr>
1261+
</table>
1262+
</emu-table>
1263+
1264+
<p>These events are introduced by abstract operations or by methods on the Atomics object.</p>
1265+
<p>Some operations may also introduce <dfn>Synchronize</dfn> events. A <dfn variants="Synchronize events">Synchronize event</dfn> has no fields, and exists purely to directly constrain the permitted orderings of other events.</p>
1266+
<p>In addition to Shared Data Block and Synchronize events, there are host-specific events.</p>
1267+
<p><ins>If the [[Storage]] field of a ReadSharedMemory, WriteSharedMemory, or ReadModifyWriteSharedMemory event is a SharedBlockStorage, then </ins><del>L</del><ins>l</ins>et <del>the</del><ins>its</ins> range of <del>a ReadSharedMemory, WriteSharedMemory, or ReadModifyWriteSharedMemory event</del> be the Set of contiguous integers from its <ins>[[Storage]].</ins>[[ByteIndex]] to <ins>[[Storage]].</ins>[[ByteIndex]] + <ins>[[Storage]].</ins>[[ElementSize]] - 1. Two events' ranges are equal when the events <ins>have a SharedBlockStorage in their [[Storage]] field,</ins> have the same <ins>[[Storage]].</ins>[[Block]], and the ranges are element-wise equal. Two events' ranges are overlapping when the events have the same <ins>[[Storage]].</ins>[[Block]], the ranges are not equal and their intersection is non-empty. Two events' ranges are disjoint when the events do not <ins>both have a SharedBlockStorage in their [[Storage]] field, do not</ins> have the same <ins>[[Storage]].</ins>[[Block]]<ins>,</ins> or their ranges are neither equal nor overlapping.</p>
1268+
<p><ins>If the [[Storage]] field of a ReadSharedMemory, WriteSharedMemory, or ReadModifyWriteSharedMemory event is a SharedStructStorage, then let its range be the value of the [[Storage]] field. Two events' ranges are equal when the events have a SharedStructStorage in their [[Storage]] field, have the same [[Storage]].[[Struct]] and the same [[Storage]].[[Field]]. Two events' ranges that both have a SharedStructStorage in their [[Storage]] field are never overlapping. Two events' ranges are disjoint when the events do not both have a SharedStructStorage in their [[Storage]] Field, or do not have the same [[Storage]].[[Struct]] or the same [[Storage]].[[Field]].</ins></p>
1269+
</emu-clause>
1270+
</emu-clause>
1271+
<p>For brevity, the refactoring of the memory model relations to use SharedStructStorage and the modified definition of event ranges is omitted.</p>
10591272
</emu-clause>

0 commit comments

Comments
 (0)