{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreihe4ag2pixhau3afmpy4ygiusoclkd7w63dvypnivb3mb6kbf3a5u",
    "uri": "at://did:plc:ivbknywyskln22er3nkssdhl/app.bsky.feed.post/3mn5kpg5wmvn2"
  },
  "path": "/t/include-racy-reads-in-rust-memory-model-with-maybeinvalid-t/24289?page=2#post_28",
  "publishedAt": "2026-05-31T10:34:17.000Z",
  "site": "https://internals.rust-lang.org",
  "tags": [
    "story"
  ],
  "textContent": "ais523:\n\n> So it turns out that this paper _already proves_ a model in which racing an _atomic_ read against a non-atomic write produces an undefined value rather than undefined behaviour,\n\nI don't think this is right. The model uses catch-fire semantics where any data race is UB. Where are you getting this from?\n\nNote in particular that the proof of Lemma D.1 relies on executions with unordered non-atomic read-write pairs to be UB.\n\nais523:\n\n> Fortunately, LLVM is intended to do so (its documentation specifically states that a raced read reads `undef` rather than producing undefined behavior), so this is another problem which turns out to already have been solved in advance.\n\nIt hasn't been solved. The LLVM model is not even precisely specified, let alone proven correct.\n\nnewpavlov:\n\n> At the risk of rehashing one of our previous discussions, I believe that inline assembly is a perfectly valid escape hatch for SeqLock. In other words, something like this could be considered sound in the context of SeqLock:\n\nI don't agree since I don't think you can write a sound story for this inline asm block. You might be tempted to pick the story \"picks an arbitrary value that satisfies the validity invariant of `T`\" (after proving that such a value exists), but then clients using this library could not, for soundness purposes, rely on actually getting back the value they wrote. If you come up with a story, you have to use the same story consistently for all Rust-level reasoning.\n\nais523:\n\n> the proofs about the memory model don't rely on it\n\nYes they do. The paper explicitly mentions this:",
  "title": "Include racy reads in Rust memory model with `MaybeInvalid<T>`"
}