Based on what I wrote here, one thing that volatile grants us is to "delay" giving a precise semantics to what happens on a memory access. We can basically delay until after the program was turned into assembly, which is what you need to talk about MMIO.
But when it is just two untrusted threads interacting with each other, what you need is formally called "robust safety", which intuitively means "being safe even when interacting with an adversary". I am not very familiar with the literature on that topic, here are some citations I took from a paper a colleague published in that area:
- Authenticity by typing (is that @asajeffrey on that author list?)
- Refinement types for secure implementations
- Robust and compositional verification of object capability patterns
The last paper shows how robust safety can be obtained by "sealing", which is a pattern Firefox uses for its JavaScript VM. But to my knowledge, none of them require the "externally observable" / "delayed semantics" aspect of volatile.
So, my current impression is that this is similar to how volatile can be used as a crude approximation of a "frozen load" (returning stable data, not undef). Using volatile for this purpose is possible but seems like taking a sledgehammer to crack a nut. volatile also does all sorts of other things that are entirely unnecessary when all you want is a frozen load.