[tetha]

> The non-volatile read is _allowed_ to see the non-volatile write (i.e. such an execution exists, this is the question I ask in the exercise), but it doesn't have to.

And this is why debugging this kind of issue in practice is fun: You have very little or non-obvious guarantees here.

If you think about constructing adversary proofs or decided that your program is a little gnome bound to make you insane, this can be rephrased as: In this example, the nonvolatile read can choose any value of any write as long as it is in a happened before relationship to the nv-read. It might pick every value, every second value, or just that one troublesome valu and never change again.