[interpreter] implement atomic.wait and atomic.notify

[conrad-watt]

also split out relevant tests into a separate file

[rossberg]

I'm somewhat confused, where is the notion of signal coming from? Is that an encoding of the reaction rules from the paper?

I would have expected a more direct implementation with administrative instructions wait' and notify', as on paper. And then perhaps auxiliary functions like the following to implement context matching:

match_wait' : code -> (memory_instance * address * f64 * (code -> code)) option
match_notify' : code -> (memory_instance * address * i64 * (code -> code)) option

(where the returned functions are "plug" function generated on the way to replace the found instruction with new code).

Also, the step function as written seems to initiate all reactions eagerly in a meta-level loop, whereas each wait/notify match is a separate step in the paper rules.

[conrad-watt]

We discussed before that we wanted to shift away from the paper formulation to an axiomatic specification for wait/notify - i.e. emitting actions without blocking that then get resolved consistently in the memory model. These "signals" are intended to try to reflect the actions relevant for wait/notify in that formulation. I guess I could rename the datatype here to "action" to make the correspondance clearer.

[rossberg]

Ah okay, that probably was a long time ago, so I don't recall. :) What would the reduction rules look like? If these signals correspond to actions, why do they become part of the thread representation in the interpreter?

[conrad-watt]

I think you're right - they shouldn't be part of the thread representation. I've just changed things up to introduce an explicit suspend administrative instruction, and tweaked the step function to now return a pair of thread * action, removing the action from the thread representation itself.

The reduction rules will look something like (roughly)

wait -> i32 1
with act = load... (not matching)

wait -> suspend
with act = load... (matching) + wait ...

suspend -> i32 0
with act = woken ...

suspend -> i32 2
with <some timeout handling>

notify -> i32 n
with act = wakes n...

and then in the axiomatic memory model, all the wait, woken, and wakes actions have to satisfy a queue specification.

[conrad-watt]

@rossberg apologies that I let this lie for so long, but PTAL

[conrad-watt]

@rossberg friendly ping

[rossberg]

If WaitAction is not distinguished here, why is it actually needed?

[conrad-watt]

Fine with removing it - I added it to more closely match the paper but since Notify_actions are being dealt with operationally here it doesn't have any direct purpose.

[rossberg]

Okay, we may want to think about getting the interpreter closer to the spec somehow wrt the actions it emits, and possibly how it uses them. But let's land this for now.

[rossberg]

Good question, it should correspond to what we using on paper. Is that a real number?

[conrad-watt]

@rossberg ptal