“uninitialized” is the term I usually use. Or if you want to say it returns an unspecified sequence of bits, the result is “picked non-deterministically”.
I’ve changed that to “picked non-deterministically”. but maybe we should give these values a name (non-deterministic value). I suspect we would it at least use it for defining
freeze. Are we using these terms in some other parts of the documentation already?
Your data race semantics only cover volatile-volatile pairs of accesses, why that?
Logic bug, fixed. EDIT: with “When volatile reads participate in data-races with any write operation, the result of what is read is picked non-deterministically. When volatile writes participate in data-races with other volatile-write operations, the result that is written is picked non-deterministically. If volatile writes participate in data-races with non-volatile write operations, the behavior is undefined.”
The use of the term “atomic” is a bit confusing since the operation is not atomic in the sense of having an atomic memory ordering.
- Volatile reads always return frozen data. (This seems to be the case in current LLVM but I have seen no documentation that this is more than an accident.)
You are assuming that we would lower these to
stores in LLVM-IR. While we could do that, we don’t have to. These are architecture specific, so we can always just insert the right machine code using
asm!(... : "volatile"). That would have the defined semantics, although it might inhibit more optimizations than necessary. We could lower them to
store, and then “launder” the
undef (e.g. by using
freeze if we ever get that, or by using an
asm! block just for that.
- Volatile writes do not cause UB when being in a race with another write. (I wouldn’t even know how to check if LLVM currently does this the way we want.)
The documentation does not mention anywhere that write-write races are undefined behavior either. The only thing that AFAIK is currently documented is a load-write race makes the load return
undef, which would be ok for us (see above). FYI I’ve opened an bug in the LLVM documentation about this, but I don’t expect this bug to be resolved any time soon: https://bugs.llvm.org/show_bug.cgi?id=42435
Worst case, we can prevent all re-ordering by using inline assembly as well to implement the writes.