Telling the Compiler a True Story: Inline Assembly in Rust's Abstract Machine

The Opaque Block

When the Rust compiler encounters an asm! block, it runs into something fundamentally alien to the rest of the language. Every other construct in Rust, every function call, every dereference, every match arm, is legible to the abstract machine. The compiler can inspect it, reason about it, apply aliasing rules, track provenance. An inline assembly block offers none of that. It is a template string wrapped in metadata, and the compiler must take the programmer at their word about what happens inside. That role requires vocabulary adequate to the task.

The traditional answer, borrowed from C, centers on constraints. GCC’s extended inline assembly uses constraint strings like "=r", "m", and "~{eax}" to declare which registers and memory locations the assembly touches. Rust’s asm! macro is structurally cleaner, but the underlying model is similar: declare operands, declare options, and the compiler trusts your declarations.

Ralf Jung’s recent post on inline assembly reframes this as a different kind of problem. The programmer is writing a chapter in the abstract machine’s execution story, specifically the chapter that covers what happened during the assembly block. That chapter needs to be internally consistent and accurate to what the hardware does.

The Abstract Machine

Rust programs are defined in terms of an abstract machine, a formal execution model that exists before LLVM optimization or platform-specific lowering. Ralf Jung has been formalizing this machine through several connected projects: MiniRust, a formalization of Rust’s core operational semantics; Stacked Borrows and its successor Tree Borrows, aliasing models for references; and Miri, an interpreter that executes programs on this abstract machine to detect undefined behavior.

The abstract machine tracks things the hardware doesn’t: whether a pointer has valid provenance for the memory it points to, whether a value is a valid instance of its type, whether two references are aliasing in a way the program declared they wouldn’t. Safe Rust is essentially a system for ensuring every step the abstract machine takes is well-defined.

Inline assembly is a hole in that system. The abstract machine reaches an asm! block and cannot proceed on its own. It needs the programmer to supply the missing chapter.

What Goes in the Story

The story is told through two mechanisms: operand declarations and option flags. Consider a simple example, reading a value from memory using a load instruction, something you might need when Rust’s standard operations don’t express the alignment or memory ordering you require:

use std::arch::asm;

unsafe fn load_u64(ptr: *const u64) -> u64 {
    let val: u64;
    asm!(
        "mov {val}, [{ptr}]",
        ptr = in(reg) ptr,
        val = out(reg) val,
        options(pure, readonly, nostack),
    );
    val
}

The operand declarations say: ptr enters the assembly as a register input and is not modified; val exits as a register output and has no meaningful initial value. These declarations tell the abstract machine which Rust values cross the assembly boundary and in which direction.

The options carry a different kind of information. readonly declares that the assembly reads memory but does not write it. nostack declares that the assembly does not push or pop the stack. pure declares that the output depends only on the declared inputs and the current memory state, with no observable side effects.

Each option is a claim about the assembly’s behavior, expressed in abstract machine terms. The compiler uses these claims to make optimization decisions. With readonly and pure, the compiler knows it can reorder stores around this block, and it may eliminate the block if the output is provably unused. With nostack, the compiler knows it does not need to ensure stack alignment before entry.

The full set of available options covers the major dimensions the abstract machine cares about. nomem is stronger than readonly: it asserts the assembly neither reads nor writes memory, allowing the compiler to freely reorder all memory operations across the block. preserves_flags tells the compiler the assembly leaves the condition flags register unchanged, enabling certain peephole optimizations around flag-dependent branches. These are not hints; they are claims with formal semantics.

The C Comparison

GCC’s extended inline assembly encodes similar information through constraint strings, but the encoding is cryptic and the semantics are less precisely documented. The rough equivalent in C:

uint64_t val;
__asm__(
    "mov %1, %0"
    : "=r"(val)
    : "m"(*ptr)
    :);

The "=r" constraint says the output goes into a general-purpose register; "m" says the input is a memory operand. There is no direct equivalent to readonly, pure, or nostack as named options. The absence of "memory" in the clobber list serves a similar function to Rust’s nomem, but the semantics are defined by GCC’s internal IR model rather than a formal abstract machine specification.

The practical difference is that GCC’s model accumulates meaning through compiler documentation and examples, while Rust’s inline assembly model is being defined alongside a formal operational semantics. When you write options(nomem) in Rust, that claim maps to a defined property of the abstract machine: the assembly does not access any memory visible to the Rust program. When you omit "memory" from a GCC clobber list, the meaning is similar but the formal grounding is weaker, and the edge cases are less systematically catalogued. The difference matters most when you are doing something unusual, which is precisely when inline assembly tends to appear.

False Stories

The storytelling frame makes one class of error easier to recognize. Consider a version of the load function with an incorrect options claim:

// WRONG: nomem claims no memory is accessed, but the assembly reads from ptr
unsafe fn load_u64_wrong(ptr: *const u64) -> u64 {
    let val: u64;
    asm!(
        "mov {val}, [{ptr}]",
        ptr = in(reg) ptr,
        val = out(reg) val,
        options(pure, nomem, nostack),  // false: assembly reads from memory
    );
    val
}

The story claims nomem, meaning no memory is accessed. The assembly template dereferences ptr, reading from memory. These two facts contradict each other. The compiler, trusting the story, is permitted to reorder other memory operations around this block, cache the result across multiple calls to the same pointer even if the memory changed between them, or perform other transformations that assume no memory is touched.

The behavior is formally undefined. The optimizer is permitted to produce any output whatsoever, and observed behavior on one compiler version may change silently on the next. This is not a stability guarantee failure or a quality-of-implementation issue; it is the intended scope of “undefined behavior” in Rust’s model.

Replacing nomem with readonly tells an accurate story. The block reads memory but doesn’t write it; the output depends on the pointer’s contents at the time of the call. The compiler can no longer freely reorder writes around the block, but it can still reason about the absence of writes. The story is less permissive for the compiler, but it is true.

The same logic applies when options are too weak as well. Claiming only the default (no options) when the assembly is actually pure and nomem is not a safety violation, but it is an underspecified story that prevents legitimate optimizations. The abstract machine will accept a conservative story, but an accurate one gives both the compiler and future readers more to work with.

What Miri Can Check

One consequence of grounding inline assembly semantics in a formal abstract machine is that Miri can partially verify these claims. Miri does not execute assembly templates, since it is an abstract machine interpreter rather than a hardware emulator. But it can check that operand types are valid, that declared outputs are properly initialized after the block, and that the options are not internally inconsistent.

This is a partial check. As the abstract machine specification matures through ongoing work in the unsafe code guidelines working group, the gap between a programmer’s story and a machine-checkable proof narrows. The inline assembly semantics being formalized today are the foundation for stronger tooling in future compiler versions. The investment in a formal model pays out over time, as the space of automatically detectable errors expands.

The Point of the Framing

The storytelling metaphor is not decorative. It captures something true about what the programmer is actually doing when they write an asm! block.

The programmer holds information the compiler cannot derive: what the assembly does in terms the abstract machine can reason about. The operand declarations and option flags are the vocabulary for encoding that information. When the encoding is wrong, the bug lives in the gap between what the programmer told the compiler and what the assembly actually does. The hardware may have behaved correctly at every step; the contract with the optimizer was false.

That failure mode is distinct from a logical error in the assembly template, and it requires a different approach to find and fix. Reading an asm! block as a story to be evaluated for truthfulness is more natural than checking a list of constraints for completeness. It frames the programmer’s job as writing an accurate account of what happens, rather than selecting the right symbols from a lookup table.

The Rust ecosystem has invested heavily in making unsafe code auditable, through aliasing models, provenance tracking, and formal semantics. Inline assembly has historically been the least legible part of that surface. A coherent storytelling framework, grounded in the abstract machine, is the first step toward making it as auditable as the rest.