Extended memory model

[wks]

The current memory model is designed according to the C11/C++11 standard. It involves atomic memory access, locks and threads.

However, there are issues which C11 and C++11 do not address. They are:

• [x] Futex: Futex wait implies an atomic load-compare-sleep operation. (See spec)
• [x] Trap/watchpoint/osr: They involves stack binding/unbinding. Just make more things explicit. (See spec)
• [x] Swap-stack: C11 does not address swap-stack, but swap-stack operations in different threads may conflict and visibility issues involved in swap-stack operations should be clarified. (making racing swap-stack operations undefined behaviours is okay) (See spec)
• [X] Foreign language interface: When parallel µVM programs runs together with parallel native programs, we need a way to synchronise the two worlds. This also involves object pinning. See https://github.com/microvm/microvm-meta/issues/37 (It ends up that Mu cannot make much guarantees known that the worst case of native memory access is segmentation fault. This thing must be very implementation-specific.)

Current ideas:

Futex: (open question) Should futex_wake happen before the next instruction after the futex_wait that actually wakes up? Probably yes.

int shared_state = 42;

atomic_int thread1_wake = 0;
futex thread1_futex;

thread1:
    while(load(ACQUIRE, &thread1_wake)!=1) { // OP4
        futex_wait(thread1_futex);  // OP5
    }
    int s = shared_state // OP6

thread2:
    shared_state = 99; // OP1
    store(RELEASE, &thread1_wake, 1); // OP2
    futex_wake(thread1_futex);  // OP3

According to the semantic of RELEASE and ACQUIRE, if OP4 sees the store by OP2, then OP6 must see the store of OP1.

The problem is, if the OP3 futex_wake is not guaranteed to happen before the waking of OP5 futex_wait, then the next OP4 in the loop may not see the store by OP2 at all, and may go to sleep another time. Then it will be sleeping forever.

stack binding/unbinding cannot be atomic. Swap-stack is a combination of two and cannot be atomic, either.

We may require the language implementer to correctly use other synchronisations to make sure racy swap-stack operations do not happen.

[wks]

A separate file https://github.com/microvm/microvm-spec/wiki/memory-model-refined is created for drafting this change.

[wks]

The https://github.com/microvm/microvm-spec/wiki/memory-model-refined page now addresses futex and stack operations.