Editorial: Improve Memory Model/SharedArrayBuffer auto-links - #3935
Editorial: Improve Memory Model/SharedArrayBuffer auto-links#3935gibson042 wants to merge 9 commits into
Conversation
|
The rendered spec preview for this PR is available as a single page at https://tc39.es/ecma262/pr/3935 and as multiple pages at https://tc39.es/ecma262/pr/3935/multipage . |
| 1. For each ReadSharedMemory or ReadModifyWriteSharedMemory event _readEvent_ of SharedDataBlockEventSet(_execution_) such that _readEvent_.[[NoTear]] is *true*, do | ||
| 1. Assert: The remainder of dividing _readEvent_.[[ByteIndex]] by _readEvent_.[[ElementSize]] is 0. | ||
| 1. For each WriteSharedMemory or ReadModifyWriteSharedMemory event _writeEvent_ such that _readEvent_ reads-from _writeEvent_ in _execution_, _readEvent_ and _writeEvent_ have equal memory ranges, and _writeEvent_.[[NoTear]] is *true*, do | ||
| 1. If there exists a WriteSharedMemory or ReadModifyWriteSharedMemory event _otherWriteEvent_ such that _readEvent_ reads-from _otherWriteEvent_ in _execution_, _readEvent_ and _otherWriteEvent_ have equal memory ranges, _otherWriteEvent_.[[NoTear]] is *true*, and _otherWriteEvent_ is not _writeEvent_, then |
There was a problem hiding this comment.
Since Events are Records, should this be
.. and _otherWriteEvent_ and _writeEvent_
are not the same Event
?
There was a problem hiding this comment.
Updated for internal consistency, but per Editorial Conventions: Comparisons I think all of the "x and y {are,are not} the same $RecordType" comparisons should be replaced with "x {is,is not} y". I count 14 instances, including this one.
There was a problem hiding this comment.
I think all of the "x and y {are,are not} the same $RecordType" comparisons should be replaced with "x {is,is not} y".
That's one of the things I proposed in PR #3206, but got editor pushback on it, so the "are the same X Record" wording remained. I'm not sure why the Editorial-Conventions don't cover it. (I asked in the Editors room, haven't got any replies yet.)
linusg
left a comment
linusg
left a comment
There was a problem hiding this comment.
One nit, otherwise LGTM (though I'm not very knowledgeable about this part of 262 so take that with a grain of salt 🙂)
| </li> | ||
| <li> | ||
| <p>For each WriteSharedMemory or ReadModifyWriteSharedMemory event _writeEvent_ in SharedDataBlockEventSet(_execution_), if _writeEvent_.[[Order]] is ~seq-cst~, then it is not the case that there is an infinite number of ReadSharedMemory or ReadModifyWriteSharedMemory events in SharedDataBlockEventSet(_execution_) with equal memory range that is memory-order before _writeEvent_.</p> | ||
| <p>For each WriteSharedMemory or ReadModifyWriteSharedMemory event _writeEvent_ in SharedDataBlockEventSet(_execution_), if _writeEvent_.[[Order]] is ~seq-cst~, then there are at most a finite count of ReadSharedMemory or ReadModifyWriteSharedMemory events _readEvent_ in SharedDataBlockEventSet(_execution_) such that _writeEvent_ and _readEvent_ have equal memory ranges and _readEvent_ is-memory-order-before _writeEvent_.</p> |
There was a problem hiding this comment.
This is awkward - singular writeEvent is extracted via for each, then there are [...] events readEvent doesn't really work.
There was a problem hiding this comment.
It's grammatically correct phrasing (in slightly simplified form: "For each writeEvent in SharedDataBlockEventSet(execution), if writeEvent.[[Order]] is ~seq-cst~, then there are at most $n other events readEvent in SharedDataBlockEventSet(execution) such that Relation $R contains (readEvent, writeEvent)").
However, I'm glad you commented on this bullet point, because regardless of phrasing, it strikes me as tautological... SharedDataBlockEventSet returns a Set which by the nature of ECMAScript computation and memory model cannot be infinite and therefore cannot contain a subset that doesn't satisfy the condition. The following note suggests what the bullet point might be trying to enforce, which relates to Forward Progress, but it's not clear to me how it can be fixed (maybe @syg has an idea?).
But regardless, I think this rephrasing improves clarity and is therefore worth keeping in this PR even if the final result is dramatically different.
There was a problem hiding this comment.
A little hard to parse IMO but after re-reading it makes sense now, thanks for clarifying!
There was a problem hiding this comment.
Yeah, the intention is liveness as the note says. So, I do think you're right in that at any particular point during Evaluation, a candidate execution is finite. This requirement is really about quantifying over all possible candidate executions, which is indeed infinite. You can explicitly quantify that here and wave over formally defining that quantification (I recommend you do, because I think formally defining it won't shed any additional light for readers, probably the opposite), maybe? Kinda like how we do it in WeakRef liveness.
There was a problem hiding this comment.
This requirement is really about quantifying over all possible candidate executions, which is indeed infinite. You can explicitly quantify that here and wave over formally defining that quantification (I recommend you do, because I think formally defining it won't shed any additional light for readers, probably the opposite), maybe? Kinda like how we do it in WeakRef liveness.
Any thoughts on how to do that, or where? The definitions of is-memory-order-before and sequentially consistent atomics and valid execution each apply to a single candidate execution, with the only further quantification being a normative requirement (or perhaps more accurately, an observation) that all programs have at least one valid execution. But since that quantification is already present in Valid Executions, I think that's probably the best location for this as well. But I'd really love some suggested text, because a useful explanation is eluding me. It seems like the relevant constraints here might actually be emergent, in which case normative text is not required and we could instead add a note (or add a note in addition to normative spec changes).
Regardless, I don't think this is fundamentally in scope here. We can address it independently of this PR, which I'm inclined to do unless you have an easy fix in mind.
| <li>If _eventA_ host-synchronizes-with _eventB_ in _execution_, HostEventSet(_execution_) contains _eventA_ and _eventB_.</li> | ||
| <li>There is no cycle in the union of host-synchronizes-with and is-agent-order-before in _execution_.</li> | ||
| <li>If _eventA_ host-synchronizes-with _eventB_ in _execution_, _eventA_ and _eventB_ are both Host memory events and elements of EventSet(_execution_).</li> | ||
| <li>The union of host-synchronizes-with and is-agent-order-before in _execution_ is a strict parital order. In particular, if (_eventA_, _eventB_) is a member of that union, then (_eventB_, _eventA_) is not.</li> |
There was a problem hiding this comment.
This is wrong. The only requirement on the union should be that it's acyclic. A strict partial order requires transitivity, which we don't need to impose on the union. That happens when they're composed together in happens-before.
efbe9e3 to
7689c23
Compare
4 participants
And gratuitously