Skip to content

Normative: fix axiomatic model to be SC-DRF, and allow ARMv8 compilation #1511

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
ljharb merged 4 commits into from
May 2, 2019
Merged

Normative: fix axiomatic model to be SC-DRF, and allow ARMv8 compilation #1511

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
01d950f
Normative: strengthen model to be SC-DRF (#1511)
conrad-watt Apr 17, 2019
448a356
Normative: weaken model to allow ARMv8 compilation (#1511)
conrad-watt Apr 17, 2019
ecb5860
Editorial: simplify synchronizes-with due to new rules (#1511)
conrad-watt Apr 16, 2019
5527c80
Editorial: add non-normative note on synchronizes-with and Init event…
conrad-watt Apr 25, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 11 additions & 8 deletions spec.html
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39402,13 +39402,7 @@ <h1>synchronizes-with</h1>
<p>For a candidate execution _execution_, _execution_.[[SynchronizesWith]] is the least Relation on events that satisfies the following.</p>
<ul>
<li>
For each pair (_R_, _W_) in _execution_.[[ReadsFrom]], (_W_, _R_) is in _execution_.[[SynchronizesWith]] if all the following are true.
<ul>
<li>_R_.[[Order]] is `"SeqCst"`.</li>
<li>_W_.[[Order]] is `"SeqCst"` or `"Init"`.</li>
<li>If _W_.[[Order]] is `"SeqCst"`, then _R_ and _W_ have equal ranges.</li>
<li>If _W_.[[Order]] is `"Init"`, then for each event _V_ such that (_R_, _V_) is in _execution_.[[ReadsFrom]], _V_.[[Order]] is `"Init"`.</li>
</ul>
For each pair (_R_, _W_) in _execution_.[[ReadsFrom]], (_W_, _R_) is in _execution_.[[SynchronizesWith]] if _R_.[[Order]] is `"SeqCst"`, _W_.[[Order]] is `"SeqCst"`, and _R_ and _W_ have equal ranges.
</li>
<li>
For each element _eventsRecord_ of _execution_.[[EventsRecords]], the following is true.
Expand All @@ -39423,6 +39417,10 @@ <h1>synchronizes-with</h1>
<p>Owing to convention, write events synchronizes-with read events, instead of read events synchronizes-with write events.</p>
</emu-note>

<emu-note>
<p>`"Init"` events do not participate in synchronizes-with, and are instead constrained directly by happens-before.</p>
</emu-note>

<emu-note>
<p>Not all `"SeqCst"` events related by reads-from are related by synchronizes-with. Only events that also have equal ranges are related by synchronizes-with.</p>
</emu-note>
Expand Down Expand Up @@ -39511,7 +39509,12 @@ <h1>Sequentially Consistent Atomics</h1>
<ul>
<li>For each pair (_E_, _D_) in _execution_.[[HappensBefore]], (_E_, _D_) is in memory-order.</li>
<li>
<p>For each pair (_E_, _D_) in _execution_.[[SynchronizesWith]], (_E_, _D_) is in memory-order if there is no WriteSharedMemory or ReadModifyWriteSharedMemory event _W_ in SharedDataBlockEventSet(_execution_) with equal range as _D_ such that _W_ is not _E_, and the pairs (_E_, _W_) and (_W_, _D_) are in memory-order.</p>
<p>For each pair (_R_, _W_) in _execution_.[[ReadsFrom]], there is no WriteSharedMemory or ReadModifyWriteSharedMemory event _V_ in SharedDataBlockEventSet(_execution_) such that _V_.[[Order]] is `"SeqCst"`, the pairs (_W_, _V_) and (_V_, _R_) are in memory-order, and any of the following conditions are true.</p>
<ul>
<li>The pair (_W_, _R_) is in _execution_.[[SynchronizesWith]], and _V_ and _R_ have equal ranges.</li>
<li>The pairs (_W_, _R_) and (_V_, _R_) are in _execution_.[[HappensBefore]], _W_.[[Order]] is `"SeqCst"`, and _W_ and _V_ have equal ranges.</li>
<li>The pairs (_W_, _R_) and (_W_, _V_) are in _execution_.[[HappensBefore]], _R_.[[Order]] is `"SeqCst"`, and _V_ and _R_ have equal ranges.</li>
</ul>
<emu-note>
<p>This clause additionally constrains `"SeqCst"` events on equal ranges.</p>
</emu-note>
Expand Down