Write->read causality with futexWait returning NOTEQUAL

[lars-t-hansen]

Not sure if this is already implied by the current happens-before relation and other spec prose but I think it should be spelled out. There's already a happens-before relation from Atomics.futexWake to Atomics.futexWait if the wake does wake the waiter, ie, the futexWait returns OK. But what if futexWait returns NOTEQUAL? In that case that relation does not apply. However, it should be specified that futexWait does perform an atomic read of the location at the outset, so that if NOTEQUAL is returned there is a write->read relationship between the write that set the value and the futexWait. This means that the usual pattern, where a waking thread first updates the value and then calls futexWait, is in the proper relationship with a thread that calls futexWait regardless of whether futexWait returns with OK or NOTEQUAL.

(See a comment on Issue #56 for background.)

[jfbastien]

Not to belabor the point, but #12 synchronic's wording ensures this :-)

[lars-t-hansen]

That's right, rub it in :-)

The existing wording in the spec might even ensure this too, or it might ensure it with a little tweak that exposes the atomic read in futexWait.