Operational semantics for `AtomicMaybeUninit::compare_exchange`

[RalfJung]

Rust currently has no way to do atomic operations on types that may contain uninitialized bytes. crossbeam's AtomicCell resorts to using the standard library Atomic* types instead, but that doesn't entirely work: load will be UB if there is any uninitialized byte, and store requires transmuting the to-be-stored T into an integer which is likewise UB if there are any uninitialized bytes. (Plus if there is pointer provenance, that is getting lost.)

(Note that (u16, u8) anyway cannot be used with atomic operations since it is insufficiently aligned. Generally atomic operations have alignment requirements equal to their size, so the only way for other types to have the right size and alignment is for them to be newtypes, or to use repr(align).)

So there is a clear demand for something like AtomicMaybeUninit. There even is an inline assembly implementation of it. It would be great if Rust could provide this natively. Mostly this is a libs-api question of how to best expose these operations, but for read-modify-write operations things are more interesting: what is AtomicMaybeUninit::compare_exchange supposed to behave like? Usually comparing uninit values leads to UB, even on the LLVM level.

Avoid the uninit comparison

One option would be to try and somehow entirely avoid comparisons of uninit memory. This would also avoid having to get any new guarantees from LLVM. An AtomicMaybeUninit type could have the invariant that the data inside it is always frozen; compare_exchange could freeze the provided value-to-compare, and then the comparison works on entirely well-defined bits.

However, this invariant is broken by get_mut, since that function could be used to de-initialize padding bytes. So maybe we don't have such an invariant but freeze the in-memory data before comparison? But then that freezing must somehow be atomic, and what if the comparison fails -- usually this would be just a read-only access, but now the freeze made this a write somehow?

Allow the uninit comparison

We could say that comparing data with uninit contents just leads non-deterministic results (and try to convince LLVM to add that to their concurrency spec). However this introduces liveness issues: always returning "inequal" would be a legal implementation if any of the in-memory bytes is uninitialized. And it seems like the C++ wording for compare_exchange_strong on unions indeed allows comparisons to always fail. For padding outside union types however C++ guarantees that comparison will ignore padding bytes; I have no idea how compilers are implementing this -- they might have to use locking?

[digama0]

We could say that comparing data with uninit contents just leads non-deterministic results (and try to convince LLVM to add that to their concurrency spec). However this introduces liveness issues: always returning "inequal" would be a legal implementation if any of the in-memory bytes is uninitialized.

I lean toward this option, it is equivalent to freezing the memory on load immediately before the compare. I don't think we can ensure that the memory is always frozen in the type, because we have to prepare for the case that it's just a random byte of memory that has been transmuted to AtomicMaybeUninit in order to do the operation, which I don't think should be UB, since it works and is used for other atomic types. It would be surprising if AtomicMaybeUninit can't actually be uninit.

So suppose there are actual uninit bytes in memory when you do a compare_exchange. We could do a freezing write as part of the compare_exchange, but this has atomics implications and unless the cache hierarchy treats a failing compare_exchange as a write (and I don't think they do) we probably can't do this either.

Which leaves us with the remaining option of making it potentially fail and return a value which could fail the next compare_exchange even without a write in between. One reason this is reasonable is that if the byte was hardware-uninit, e.g. a byte on a MADV_FREE page that will be zeroed shortly unless a write happens first, then you could indeed have that the OS zeroes the byte after the compare_exchange (which does not count as an action in the AM because there is no thread for it), and hence the second compare_exchange will fail. So this seems like the closest model to the actual hardware behavior.

[RalfJung]

I agree it is the "most direct to hardware" spec. However, that would make it impossible to prove liveness of compare_exchange loops that involve padding, and it would have to be taken into account when turning atomic RMWs into regular non-atomic operations (if that's a transformation that LLVM ever does).

I wonder if there's somehow a way that we can recover liveness by imposing some restriction on the non-determinism (similar-ish to scheduler fairness).

[digama0]

The hardware itself is pretty tame here, it would not be hard to have a clause along the lines "if you keep retrying it won't fail forever" which can be easily seen to be correct for hardware-uninit notions (e.g. the MADV_FREE zeroing thing can only happen once). The more difficult issue is from the compiler itself, because if it is able to determine that the byte is uninit and replaces the compare_exchange with constant false then of course no amount of spinning will help. Seems like you want some kind of volatile-like restriction to avoid the compiler from getting too clever about the results.

Re: hardware uninit, one way you could prank the process would be to put uninit over a byte which is actually MMIO and returns a different number each time you read it... That really would fail liveness.

[chorman0773]

Actually, I think my question is whether it's AtomicMaybeUninit that's desired, or freeze. The AtomicAggregate problem is solved by having freeze. That also trivially answers the compare_exchange issue.

xlang currently calls it UB to use cmpxchg atomic (and atomic fetch_assign/compound_assign) on an uninit dest (ignoring padding bytes of T - I have ideas for that).

Re: hardware uninit, one way you could prank the process would be to put uninit over a byte which is actually MMIO and returns a different number each time you read it... That really would fail liveness.

Or lift the atomic to a register that is electrically floating.

[digama0]

Or lift the atomic to a register that is electrically floating.

I think that this would not cause too many problems - it seems very unlikely if you read a register a million times in a spinloop that you will not get the same value twice. Even if it's floating there are manufacturing biases and so on, it's not a random number generator (or at least, not one with a particularly good source of entropy). You need something more deliberate than that to actually livelock, like MMIO hooked up to an actual random number generator or an alternating pattern.

[RalfJung]

The hardware itself is pretty tame here, it would not be hard to have a clause along the lines "if you keep retrying it won't fail forever" which can be easily seen to be correct for hardware-uninit notions (e.g. the MADV_FREE zeroing thing can only happen once).

I have no idea for how to add such a clause to our liveness guarantees, in a formally precise way. It has to somehow say that if you read an Uninit from memory and then compare that with the value still in memory, and you do that in a loop, then eventually this will turn out equal. But Uninit don't have an identity in the AM, so we cannot really express this notion of comparing that Uninit that you loaded -- and clearly if you compare any other Uninit then it is not live.

I don't want to add provenance to Uninit for this. 🙈

Re: hardware uninit, one way you could prank the process would be to put uninit over a byte which is actually MMIO and returns a different number each time you read it... That really would fail liveness.

That's just like memory where someone else keeps writing different values. Even without uninit, the compare_exchange loop does not always terminate. It only terminates if everyone else eventually stops writing. In the MMIO case, that condition is conceptually violated. So I am not concerned about this case.

The AtomicAggregate problem is solved by having freeze.

It's not, though? This is the alternative I described as "Avoid the uninit comparison" in the OP.

[comex]

For padding outside union types however C++ guarantees that comparison will ignore padding bytes; I have no idea how compilers are implementing this -- they might have to use locking?

Here's a test case.

GCC seems to handle this by zeroing out the padding bytes before storing a value to an atomic, as well as in the comparison value for compare_exchange_strong. But this approach can't work if you perform an atomic operation on memory which was previously initialized non-atomically with nonzero padding bytes. C++ used to disallow mixing atomic and non-atomic operations, but C++20 adds atomic_ref. While atomic_ref has multiple theoretical possible implementations, all of the compilers I tested implement it by performing atomic operations on the original memory. And despite atomic_ref having the same requirement to ignore padding bits according to cppreference, GCC does nothing to handle this and is apparently non-conforming.

MSVC has a better approach which doesn’t conflict with atomic_ref. (I tested 2022, and note this behavior only exists with C++20 mode enabled.) It does not zero out padding. Instead, for both atomic and atomic_ref, it implements compare_exchange_strong using a loop like this (pseudocode):

loop {
    match atomic.compare_exchange_weak(current, new) {
        Ok(_) => return true,
        Err(actual) => {
            if !is_equal_ignoring_padding_bits(actual, current) {
                return false;
            }
            current = actual;
        }
    }
}

This approach assumes that the memory contents will at least eventually settle, in the sense that the padding bytes will be equal on successive reads. I’m not sure what kind of MADV_FREE-like mechanisms exist in Windows, but it’s probably a reasonable assumption.

Clang with libc++ is the last compiler I tested and appears to be straight-up non-conforming even without atomic_ref, as it neither zeroes out the padding like GCC nor does a loop like MSVC.

[RalfJung]

MSVC has a better approach which doesn’t conflict with atomic_ref. (I tested 2022, and note this behavior only exists with C++20 mode enabled.) It does not zero out padding. Instead, for both atomic and atomic_ref, it implements compare_exchange_strong using a loop like this (pseudocode):

This is what AtomicCell does as well. The tricky part, as discussed above, is arguing that the loop will ever terminate. This is where making this a compiler primitive can actually be useful because then one can make this argument based on low-level hardware details.

Still this is probably more sensible than trying to ensure that padding bytes are zero.

We should probably file issues against GCC and clang...

[chorman0773]

This is what AtomicCell does as well. The tricky part, as discussed above, is arguing that the loop will ever terminate. This is where making this a compiler primitive can actually be useful because then one can make this argument based on low-level hardware details.

The best solution may just be to have a lower-level compiler primitive. This is how lccc's std::atomic<T> will work. Just lowers to atomic operations in XIR which handle padding properly. Since the actual padding-ignoring is being done during MCE, I can sidestep the "padding is uninit" issue, because MCE doesn't have uninit (unless you count MADV_FREE or floating registers). There, only MMIO is actually going to change, and xlang at least allows volatile accesses (reads and writes) to run a signal handler, which can 100% loop{}, so xlang isn't allowed to assume liveness after a volatile access.

Maybe AtomicAggregate<T> is what we want instead of AtomicMaybeUninit. The compare_exchange/compare_exchange_weak would just be defined in terms of is_structurally_equal and sidestep the padding issue.

[digama0]

The hardware itself is pretty tame here, it would not be hard to have a clause along the lines "if you keep retrying it won't fail forever" which can be easily seen to be correct for hardware-uninit notions (e.g. the MADV_FREE zeroing thing can only happen once).

I have no idea for how to add such a clause to our liveness guarantees, in a formally precise way. It has to somehow say that if you read an Uninit from memory and then compare that with the value still in memory, and you do that in a loop, then eventually this will turn out equal. But Uninit don't have an identity in the AM, so we cannot really express this notion of comparing that Uninit that you loaded -- and clearly if you compare any other Uninit then it is not live.

No no no, I definitely did not mean to have a notion of uninit identity, I really mean just a standard CAS loop where you take the value you receive from Err and use it in the next invocation, I claim that if you do that long enough (and no other threads are writing to this byte, or eventually stop without this thread proceeding) then it will proceed eventually without any claims about what is in memory, but in particular in the case where the memory holds the (canonical and only) uninit value.

I think there are other reasons to be unsatisfied with such a bolted on liveness condition, but for sufficiently permissive treatments of "eventually" it's almost always satisfied in practice, to the extent that people will build algorithms assuming it is the case.

Re: hardware uninit, one way you could prank the process would be to put uninit over a byte which is actually MMIO and returns a different number each time you read it... That really would fail liveness.

That's just like memory where someone else keeps writing different values. Even without uninit, the compare_exchange loop does not always terminate. It only terminates if everyone else eventually stops writing. In the MMIO case, that condition is conceptually violated. So I am not concerned about this case.

I agree, if there was a write, but there is no write in this scenario, there is a temperamental MMIO port and an AM that says that the byte holds uninit and therefore the tempermentality is consistent with the repeated freeze operation that happens on each CAS. The AM state is unchanged after each go around the loop (except for the value passed to the Err(n) return value of the CAS), it holds uninit the whole time.

[RalfJung]

I really mean just a standard CAS loop where you take the value you receive from Err and use it in the next invocation, I claim that if you do that long enough (and no other threads are writing to this byte, or eventually stop without this thread proceeding) then it will proceed eventually without any claims about what is in memory, but in particular in the case where the memory holds the (canonical and only) uninit value.

Sure, but making that formal is tricky at best. Do you want to syntactically match on the loop? So that if the user does some completely harmless tiny change, they lose the liveness promise? That seems bad.

I agree, if there was a write, but there is no write in this scenario, there is a temperamental MMIO port and an AM that says that the byte holds uninit and therefore the tempermentality is consistent with the repeated freeze operation that happens on each CAS. The AM state is unchanged after each go around the loop (except for the value passed to the Err(n) return value of the CAS), it holds uninit the whole time.

I'm saying there is a write. It's just not correct to model this with Uninit on the AM level. You have to model it with writes on the AM level.

[RalfJung]

Maybe AtomicAggregate is what we want instead of AtomicMaybeUninit. The compare_exchange/compare_exchange_weak would just be defined in terms of is_structurally_equal and sidestep the padding issue.

That doesn't help for unions though.

[digama0]

I'm saying there is a write. It's just not correct to model this with Uninit on the AM level. You have to model it with writes on the AM level.

Can you explain why? This is behavior which would otherwise be classified as "environment misbehavior", i.e. you have a byte that has a flaky value in it, which changes without any action on the part of the AM. However, because the AM says there is uninit in the byte, even a flaky value is a valid refinement of the AM model, and AFAIK this is a conforming execution.

[RalfJung]

Well, this thread is an example for why -- we want AM Uninit to be "eventually stable" which is not the case for your MMIO byte.

I'm anyway not sure if we should think of MMIO memory in this way. Really with MMIO memory, each read is just an external function call saying "please give me the current value". There's nothing odd with getting a different result each time. The odd thing is expecting to be able to do atomic operations on that memory...