Include racy reads in Rust memory model with `MaybeInvalid<T>`

[RalfJung]

@ais523

Or in other words, I don't see the angelic choices as being made immediately. Rather, I think that sort of choice works like variables in Prolog:

You are describing something more akin to symbolic execution than angelic choice. Symbolic execution is indeed a way to approximate or even implement angelic choice. But having that in an actual program run (rather than in a program analyzer) requires explicitly adding symbolic state to the program state, which in turn affects everything else that reasons about the program state.

For ptr2int casts specifically, the PNVI-ae-udi model in C does pretty much that: the "udi" mechanism introduces a symbolic form of provenance that approximates the angelic semantics. Sadly it does not easily work with more complicated models such as Stacked/Tree Borrows, or even with restrict in C.

[ProgramCrafter]

@RalfJung

FWIW, I think the reason that "seqlock with inline asm for the data reads and writes" works in practice is that there is another story, one that actually works in my framework (assuming a language extension to Rust that we'll hopefully get one day): consider those accesses to be relaxed bytewise atomic.

@newpavlov

We could move the validity check into the assembly block, but honestly it feels like an unnecessary (and error-prone) busy-work to create a purer "story".

When the check is moved inside, then there is effectively equivalent Rust code which explains what happens:

use std::hint::black_box;
use std::sync::RwLock;

struct SeqlockStory<T>(RwLock<T>);

impl<T: Clone + Default> SeqlockStory<T> {
    fn load(&self) -> T {
        if let Ok(v) = self.0.try_read() { return v.clone(); }
        return black_box(T::default());  // outer code can't rely on
                                         // the exact returned value
    }
    fn store(&self, value: T) {
        *self.0.write().unwrap() = value;
    }
}

[RalfJung]

black_box is a NOP opsem-wise, so it doesn't ever make sense in a story. It's either unnecessary in your story or the story doesn't quite work.

Also what's try_read? You can't just access MiniRust here. As mentioned above, the correctness argument for the "story" approach relies on the story being expressible in regular Rust code.

[programmerjake]

pub fn try_read(&self) -> TryLockResult<RwLockReadGuard<'_, T>> - RwLock in...

[RalfJung]

Oh sorry, I missed the RwLock. That has a different size than T so this doesn't literally work, but I guess we could imagine that the RwLock state is stored out-of-band.

The return T::default() is wrong though since the asm code may return a different value.

And generally that story is pretty far from what the asm actually does so arguing that the asm is a refinement of this code is far from trivial. For instance, the story code performs a bunch of synchronization (the try_read internally does an "acquire"), while the asm code doesn't do the same synchronization -- but for the story to be valid the asm code has to perform at least as much synchronization as the story.

[ProgramCrafter]

@RalfJung

The return T::default() is wrong though since the asm code may return a different value.

True. There should be some source of nondet (demonic permitted)... well for any T that can be constructed from byte array (like std::vec::Vec<u8>, impl bytemuck::AnyBitPattern or impl arbitrary::Arbitrary) there is one: allocate a few blocks and use the pointer addresses to generate the instance.

@RalfJung

but for the story to be valid the asm code has to perform at least as much synchronization as the story.

I believe the asm code must do similar synchronization (including the Release fence between data read and check if someone wrote in parallel, which happens here on automatic unlock), and will leave that question to whoever writes the actual implementation.

@RalfJung

That has a different size than T so this doesn't literally work, but I guess we could imagine that the RwLock state is stored out-of-band.

Notably, SeqLock is also T plus a counter integer so it should work out.

[RalfJung]

Oh you were imagining the inline asm to contain the entire seqlock, not just the racy read and write? Okay that changes things, I didn't think that variant through yet.

[ProgramCrafter]

More precisely, I should've written the equivalent as follows: Rust Playground.

Though I do like the bytewise-atomic memcpy more than this justification. (If only it was defined behavior on hardware specification side...)

[RalfJung]

@ProgramCrafter

Though I do like the bytewise-atomic memcpy more than this justification. (If only it was defined behavior on hardware specification side...)

Atomic bytewise memcpy (in its most restricted form, that is still sufficient for SeqLocks) does not require mixed-size accesses, so there's no problem from the hardware side.

[ais523]

It's worth noting that (in a previous program that I'm no longer working on) I ended up with a use case for after-the-fact-verfieid racy reads, seqlock style, for which the atomic-bytewise approach wouldn't work: I was writing an async-signal-safe memory allocator (i.e. it can allocate from a signal handler, even if the signal interrupted a use of the allocator), which stored its freelist in the free allocations themselves. Allocating would work like this:

1. Read the pointer to the head of the freelist;
2. Read the memory it points to in order to discover the next entry of the freelist – the pointer found there will be the new head of the freelist if step 3 succeeds;
3. Atomically swap the head of the freelist with the pointer that was read in step 2, only if the head of the freelist has not changed since step 1 (not even changed and changed back, to avoid the ABA problem).

Because the allocator is async-signal-safe, it is possible that, between step 1 and 2, a signal handler (or another thread) will allocate the first block of memory on the freelist. In this situation, step 2 will read from memory that has already been allocated and is already in use by the signal handler or other thread. The result will then be discarded in step 3 (due to the head of the freelist having changed) and will not be used for anything, but it was still actually read at the hardware level. Additionally, you can't rely on the writing code to use only atomic writes to the memory, because in this case the memory has been returned as an apparently normal allocation.

I no longer actually need to use this style of memory allocator for anything (I changed other parts of my design so that the ability to do this sort of thing wasn't necessary), but maybe someone else does. As such, I would if possible prefer a model which makes this sort of code legal, not just seqlocks.