{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreihm4skutn5tanawscqudxh7eyj7qmvo43nwrc7esvngxgdmkpnyee",
    "uri": "at://did:plc:ivbknywyskln22er3nkssdhl/app.bsky.feed.post/3mn5kpb4uurn2"
  },
  "path": "/t/include-racy-reads-in-rust-memory-model-with-maybeinvalid-t/24289?page=2#post_29",
  "publishedAt": "2026-05-31T10:45:53.000Z",
  "site": "https://internals.rust-lang.org",
  "textContent": "RalfJung:\n\n> 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>\n> I 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\nThe model was intended for a world with catch-fire semantics where any data race is UB, but this is actually a stronger assumption than the proofs require – the proofs only actually rely on a special case (where the read that is part of the race is non-atomic). If you change the model's semantics to \"a race of a non-atomic read against any sort of write is UB/catch-fire, but a race of an atomic read against a non-atomic write reads an undefined value\", then all the proofs continue to work with no changes.\n\nSo, if you change the data model to allow races of atomic reads against non-atomic writes (i.e. effectively LLVM's model), the resulting model can be proved correct by using the exact same proofs, and will have all the desirable properties that the previous model did (together with the additional desirable property of allowing you to write seqlocks and other related sorts of concurrency).\n\nI went through all the proofs in the paper and verified that they were still valid even in the new model. (My plan was originally to come up with a new model and adapt the proofs – proving something about a new memory model from scratch is hard, but adapting existing proofs to allow for a small change in the model is often easy. In this case, it turned out to be even easier than I expected.)\n\nThis also acts as a proof of correctness for LLVM's model (although this of course doesn't prove that LLVM correctly implements that model – just that the model itself is correct).\n\nRalfJung:\n\n> Yes they do. The paper explicitly mentions this:\n\nIt does rely on one case of races being UB (the case where the read is non-atomic). (I get the impresion that the authors were trying to avoid relying on race-UB at all, but had to compromise, and this is why they included the section in question.) It does not rely on the case of races being UB where only the write is non-atomic. (Presumably the authors didn't realise that the weaker condition would be useful for some people, and just stated the stronger \"races are UB\" condition without noting that a weaker condition would still work.)",
  "title": "Include racy reads in Rust memory model with `MaybeInvalid<T>`"
}