Yep, it sounds ambiguous. So if there's potentially unsafety allowed in the semantics it would already be interesting. If it turns out that the specification p

Yep, it sounds ambiguous. So if there's potentially unsafety allowed in the semantics it would already be interesting. If it turns out that the specification permits "all bets are off" in OOM, eg if it can create conditions where an adversary can gain control of execution in some way, like can happen with synchronisation bugs on some (eg Go) runtimes.