typo/wording

[web.git] / personal / _posts / 2026-03-13-inline-asm.md

diff --git a/personal/_posts/2026-03-13-inline-asm.md b/personal/_posts/2026-03-13-inline-asm.md
index ea5ef483bb60f2c49298bf66af8ff7ca18d81211..87a5fbf68fd5e726cfc1798ce3249152807e3941 100644 (file)
--- a/personal/_posts/2026-03-13-inline-asm.md
+++ b/personal/_posts/2026-03-13-inline-asm.md
@@ -82,7 +82,7 @@ Specifically, for every inline assembly block, there has to be a corresponding p
 When reasoning about the behavior of the overall program, the inline assembly block then gets replaced by that "story" code.
 You don't have to actually write this code; what's important is that the code exists and tells a coherent story with what the surrounding Rust code does.
 
 When reasoning about the behavior of the overall program, the inline assembly block then gets replaced by that "story" code.
 You don't have to actually write this code; what's important is that the code exists and tells a coherent story with what the surrounding Rust code does.
 

-[^alice]: Thank you to Alice Ryhl for suggesting the term "telling a story" for this model.
+[^alice]: Credits go to Alice Ryhl for suggesting the term "telling a story" for this model.

 
 For our example above, this immediately explains what went wrong:
 the story code for the inline assembly block would have to be something like `(x as *const i32 as *mut i32).write(0)`, and if we insert that code in place of the inline assembly block, we can immediately see (and Miri could confirm) that the program has UB.
 
 For our example above, this immediately explains what went wrong:
 the story code for the inline assembly block would have to be something like `(x as *const i32 as *mut i32).write(0)`, and if we insert that code in place of the inline assembly block, we can immediately see (and Miri could confirm) that the program has UB.


@@ -135,7 +135,7 @@ Slightly more concretely, "allocating" a page in a way that is compatible with t
 - Next, the address of the page is cast to a pointer (using [`with_exposed_provenance`](https://doc.rust-lang.org/std/ptr/fn.with_exposed_provenance.html)).
 - Finally, Rust code may use that pointer to access the new page.
 
 - Next, the address of the page is cast to a pointer (using [`with_exposed_provenance`](https://doc.rust-lang.org/std/ptr/fn.with_exposed_provenance.html)).
 - Finally, Rust code may use that pointer to access the new page.
 

-[^volatile]: Why am I insisting on volatile accesses here? Because if you had the page tables inside a regular Rust allocation, writes to that page table could have "interesting" effects, and that doesn't really correspond to anything that can happen when you write to a nomral Rust allocation. In other words, I haven't (yet) come up with a proper story that would allow for those writes to be non-volatile.
+[^volatile]: Why am I insisting on volatile accesses here? Because if you had the page tables inside a regular Rust allocation, writes to that page table could have "interesting" effects, and that doesn't really correspond to anything that can happen when you write to a normal Rust allocation. In other words, I haven't (yet) come up with a proper story that would allow for those writes to be non-volatile.

 
 The story of this asm block is that it performs memory allocation at the given address, which we know to be unallocated.[^alloc-control]
 This creates a fresh provenance that represents the new allocation.
 
 The story of this asm block is that it performs memory allocation at the given address, which we know to be unallocated.[^alloc-control]
 This creates a fresh provenance that represents the new allocation.


@@ -281,10 +281,12 @@ In some cases, however, there are no obvious miscompilations.
 And indeed, if we knew exactly which universal properties of Rust programs the compiler relies on, we could allow inline asm code that satisfies all those universal properties, even if it has no story which can be expressed in Rust source code.
 Unfortunately, this approach would require us to commit to the full set of universal properties the compiler may ever use.
 If we discover a new universal property tomorrow, we cannot use it since there might be an inline asm block for which the universal property does not hold.
 And indeed, if we knew exactly which universal properties of Rust programs the compiler relies on, we could allow inline asm code that satisfies all those universal properties, even if it has no story which can be expressed in Rust source code.
 Unfortunately, this approach would require us to commit to the full set of universal properties the compiler may ever use.
 If we discover a new universal property tomorrow, we cannot use it since there might be an inline asm block for which the universal property does not hold.

+

 This is why I am proposing to take the conservative approach:
 This is why I am proposing to take the conservative approach:

-only allow inline asm blocks that are obviously compatible with all universal properties of actual Rust code, because their story can be expressed as actual Rust code!
+only allow inline asm blocks that are obviously compatible with all universal properties of actual Rust code, because their story can be expressed as actual Rust code.
+If there is an operation we want to allow that currently has no valid story, we should just [add](https://github.com/rust-lang/rfcs/pull/3700) a [new language operation](https://github.com/rust-lang/rfcs/pull/3605), which corresponds to officially blessing that operation as one the compiler will keep respecting.

 
 

-[^noopt]: This assumes that we do not want to sacrifice the optimizations in question. Since inline assembly could hide inside any function call, this typically becomes a language-wide tradeoff: either we forbid such inline asm blocks, or we cannot do the optimization even in pure Rust code.
+[^noopt]: This assumes that we do not want to sacrifice the optimizations in question. Since inline assembly could hide inside any function call, this typically becomes a language-wide trade off: either we forbid such inline asm blocks, or we cannot do the optimization even in pure Rust code.

 
 Right now, we have no official documentation or guidelines for how inline asm blocks and FFI interact with Rust-level UB,
 but as the `innocent` example at the top of the post shows, we cannot leave inline asm blocks unconstrained like that.
 
 Right now, we have no official documentation or guidelines for how inline asm blocks and FFI interact with Rust-level UB,
 but as the `innocent` example at the top of the post shows, we cannot leave inline asm blocks unconstrained like that.