{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreiekja6gnypq4lcwouugqsgfzvyn23npudep26oyvlgkp6txopsoza",
    "uri": "at://did:plc:ivbknywyskln22er3nkssdhl/app.bsky.feed.post/3mn66t2cy7ms2"
  },
  "path": "/t/include-racy-reads-in-rust-memory-model-with-maybeinvalid-t/24289?page=2#post_40",
  "publishedAt": "2026-05-31T17:25:54.000Z",
  "site": "https://internals.rust-lang.org",
  "tags": [
    "here"
  ],
  "textContent": "RalfJung:\n\n> I have come up with counterexamples to multiple proposals that involve the program predicting the future (e.g. here and here).\n\nI find the first example here really interesting because I think it demonstrates a difference between two different sorts of future-prediction / angelic choice (and also think that it's effectively the same situation as the sequence-lock situation being discussed in this thread).\n\nFrom my point of view, the reordering of the `let b` and `let x` lines in the the first example is allowed _even with angelic choice being used_ , and the reason is that the sequence of events is as follows:\n\n  * `x` is created from a pointer using exposed provenance. For the time being, the provenance is opaque, in the sense that the compiler's behaviour does not depend on it.\n  * `b` is chosen non-deterministically.\n  * Depending on the value of `b`, `x` is offset. Its provenance is still opaque (but the same as what it was previously).\n  * `x` is dereferenced. At this point, we determine what its provenance must have been, on the basis of which address is being accessed. It is considered to have had that provenance all along (e.g. trying to access a different allocation through a copy of `x` would be undefined behavior).\n\n\n\nOr 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: initially nothing is known about them, as they are used it places more constraints on what they are, if the constraints can't be fulfilled simultaneously you get a failure (in Prolog) or undefined behavior (in Rust semantics). For people who haven't seen Prolog before, it lets you write this sort of program:\n\n\n    A = B,\n    write(B),\n    A = 2,\n    write(B).\n\n\nand get an output saying that `B`'s value is unknown from the first `write`, and an output saying that `B` is 2 from the second `write`. (The program is evaluated in order from start to end, and yet learning more about `A` nonetheless lets us know more about what `B` is/was, without any futher information being given about `B` directly.)\n\nThe basic idea is that just as a Prolog implementation can't make assumptions about the value of `B` until it sees some evidence about what the value is, a Rust compiler can't make assumptions about what provenance is obtained from `from_exposed_provenance` until it sees the pointer being dereferenced in a way that puts constraints on the provenance, or about whether or not an inline-assembly block actually read memory until it can prove that the read would have been a race.\n\nI think that this is conceptually the sort of reasoning that people want to apply to both the seqlock case (where we determine whether or not we have read from the memory, depending on whether we subsequently treat the resulting value as initialised or not) and the exposed-provenance case (where we determine which provenance the pointer had, based on which addresses it is subsequently used to access). That said, I am not convinced that this sort of reasoning is, in the abstract, always correct – based on my previous attempts to prove seqlocks correct, I suspect that it's _almost_ right, but that merely using this Prolog-style reasoning isn't automatically enough to prove the code sound, there may be other constraints too which haven't been formalised yet.\n\nOr in other words, this sort of argument from opaqueness is probably the most natural approach to solve this sort of problem (as opposed to doing things like changing the memory model, which is easier to prove correct), and many people seem to intuitively feel that it is obviously correct, but more effort will be needed to determine whether it actually does work, and to formally prove why. (There's an attractive informal argument why it works – while the angelically-determined information is opaque and so the compiler has no evidence to constrain it, it can't make optimisations that depend on its properties – but this argument is hard to formalize properly.)",
  "title": "Include racy reads in Rust memory model with `MaybeInvalid<T>`"
}