{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreibqccxuayxejj3fsu7rxvnhxb2lcjp2wap233ornf5cc3mxamw55a",
    "uri": "at://did:plc:ivbknywyskln22er3nkssdhl/app.bsky.feed.post/3mn5y4df6shs2"
  },
  "path": "/t/include-racy-reads-in-rust-memory-model-with-maybeinvalid-t/24289?page=2#post_39",
  "publishedAt": "2026-05-31T15:39:04.000Z",
  "site": "https://internals.rust-lang.org",
  "tags": [
    "here"
  ],
  "textContent": "newpavlov:\n\n> For it we would need to formally prove equivalence between the told \"story\" and the respective `asm!` block. Without it we are still in the realm of hand-waving.\n\nObviously. Your claim was that the approach is \"not formally verifiable\". I deny that claim, the entire thing could be formally verified, all the ingredients are there. That's in contrast to your approach which so far has not been expressed precisely enough to even enable the possibility of formally studying it.\n\nIf you had claimed that the approach is \"not formally verified\", I would have agreed. But that's true for basically every part of the toolchain so it's an unreasonably high bar for most of it.\n\nMaybe I misunderstood what you mean by \"verifiable\". I mean \"could be verified\", not \"has been verified\". I think that is in line with the usual meaning of the \"-able\" suffix in English.\n\nnewpavlov:\n\n> You should've started with it without assuming my dismissal\n\nI have come up with counterexamples to multiple proposals that involve the program predicting the future (e.g. here and here). I cannot come up with a counterexample to the concrete proposal for \"seqlock with inline asm\" since that code is correct, just your story isn't. And I cannot come up with a counterexample to your more general approach since you haven't written down the exact rules of what is and isn't allowed in inline asm. Therefore my claim is that if you were to write down those rules, and if they were to permit predicting the future, I'd most likely be able to come up with a counterexample.\n\nnewpavlov:\n\n> UDP: Ah, you mean that both reads and writes should be bytwise atomic.",
  "title": "Include racy reads in Rust memory model with `MaybeInvalid<T>`"
}