tc39 / proposal-atomics-wait-async

"asynchronous atomic wait" for ECMAScript
https://tc39.github.io/proposal-atomics-wait-async/
Other
90 stars 18 forks source link

Write up detailed semantics #2

Closed lars-t-hansen closed 5 years ago

lars-t-hansen commented 7 years ago

Right now there's a section titled "Informal semantics (aka useful facts)" that hints at what the semantics should be, and then there's the polyfill implementing semantics roughly like that.

What we need is to pin down the semantics more thoroughly. Some of the clauses in the informal semantics are known to contradict each other (and there's a note to that effect in the text); this contradiction must be resolved. Mostly, the problems here surround the observable wakeup order, which is tricky because an agent waiting asynchronously can both wait several times (on the same and on different locations) and can even wake up sleeping instances of itself. Only by placing this proposal into the framework established by ES2017 (both for promises and for wait/wake) can we hope to get firm semantics.

lars-t-hansen commented 7 years ago

I think that in essence the semantics will be as follows. Recall that a WaiterList pertains to a particular word address in shared memory and is a FIFO of the agents that are waiting on that location.

An argument against breaking the FIFO order is that the FIFO order is easy to remember, and the polyfill models it properly, and we can simply pretend that each async wait forks off a new agent that performs the wait for it - a very simple model. But I still think this is wrong.

lars-t-hansen commented 7 years ago

Fleshing that out a bit: Consider an agent that can block. It performs asyncWait followed by wait (on the same location). Now another agent performs a single wake on that location, ie its count = 1. If the queue order is FIFO then the asyncWait will end, which is to say, a job is enqueued, but this job cannot run (because the agent is blocking). Then nothing happens until a later wake, at which point the wait ends, the agent runs to the end after the wait call, and then the enqueued job from the asyncWait is run. If the queue order is not FIFO but prioritizes the wait, actions in the waiting agent happen in the same order, but the wait is exited earlier. Of course, since there are effects to shared memory from other agents, the waiting agent may not run the same way if it wakes earlier, compared to how it runs if it wakes later.

lars-t-hansen commented 7 years ago

Complete draft semantics posted in PROPOSAL.md, subject to bugfixes etc...

littledan commented 5 years ago

This seems fixed, per https://github.com/tc39/proposal-atomics-wait-async/issues/2#issuecomment-330563854