Actions associated with Atomics.wake/wait are not tracked in the axiomatic memory model, other than the initial read by wake. This means that other reads and writes are permitted to be re-ordered around these instructions in surprising ways.
In particular, with the current semantics it is not guaranteed that thread 1 will read 1 in the second line (assuming tA is initially zeroed).
| Line |
Thread 1 |
Thread 2 |
| 1 |
Atomics.wait(tA, 0, 0) |
tA[1] = 1 |
| 2 |
var x = tA[1]; |
Atomics.store(tA, 0, 1) |
| 3 |
- |
Atomics.wake(tA, 0, 1) |
This is because if thread 1 waits before thread 2 reaches line 2, no ordering constraint is induced between them by either thread 2's atomic store (which is never read from) or thread 2's wake, which does not induce any abstract action in the axiomatic model. Therefore, thread 1's non-atomic read is free to take the initial value of tA[1].
This is far weaker than the underlying OS calls that I assume wait/wake must be implemented using. On linux at least, when thread 1 sleeps, it will issue a full barrier. If thread 2 successfully wakes 1 or more threads, it will issue a write barrier (https://www.kernel.org/doc/Documentation/memory-barriers.txt). In my example, this is sufficient to guarantee that thread 1 will read 1 in the second line.
It also seems intuitive that wake should be used to indicate work completed on the part of the waking thread, but with the current semantics it is not guaranteed that this work will be visible.
I've previously discussed this over email with @lars-t-hansen, @syg, and @rossberg, and there seems to be a broad consensus that the semantics should be stronger. I personally believe that the act of waking and being woken should introduce abstract actions into the [[EventList]] of each thread such that the wake of thread 2 synchronizes-with a "being woken" action in thread 1. Indeed, based on our discussions, this may have been the informal intention of the spec during an earlier draft. However this might require additional barriers in some weaker architectures, and discussions in other possible specification solutions are still ongoing.
Actions associated with Atomics.wake/wait are not tracked in the axiomatic memory model, other than the initial read by wake. This means that other reads and writes are permitted to be re-ordered around these instructions in surprising ways.
In particular, with the current semantics it is not guaranteed that thread 1 will read 1 in the second line (assuming tA is initially zeroed).
This is because if thread 1 waits before thread 2 reaches line 2, no ordering constraint is induced between them by either thread 2's atomic store (which is never read from) or thread 2's wake, which does not induce any abstract action in the axiomatic model. Therefore, thread 1's non-atomic read is free to take the initial value of tA[1].
This is far weaker than the underlying OS calls that I assume wait/wake must be implemented using. On linux at least, when thread 1 sleeps, it will issue a full barrier. If thread 2 successfully wakes 1 or more threads, it will issue a write barrier (https://www.kernel.org/doc/Documentation/memory-barriers.txt). In my example, this is sufficient to guarantee that thread 1 will read 1 in the second line.
It also seems intuitive that wake should be used to indicate work completed on the part of the waking thread, but with the current semantics it is not guaranteed that this work will be visible.
I've previously discussed this over email with @lars-t-hansen, @syg, and @rossberg, and there seems to be a broad consensus that the semantics should be stronger. I personally believe that the act of waking and being woken should introduce abstract actions into the [[EventList]] of each thread such that the wake of thread 2 synchronizes-with a "being woken" action in thread 1. Indeed, based on our discussions, this may have been the informal intention of the spec during an earlier draft. However this might require additional barriers in some weaker architectures, and discussions in other possible specification solutions are still ongoing.