How does inline assembly and the physical machine fit into the abstract machine model, or exist outside of it?

language design
5

It's about operations, not guarantees. In the end, to rationalize an inline asm block, a user has to do the following:

  • Pick a specification for what the block does, as a function transforming the AM state before the block into the AM state after the block (or more precisely, the output is a set of AM states to capture non-determinism, and can also include UB, and things get even more complicated if you need to account for concurrency). The extra flags set on the asm blocks can constrain this state transformation, e.g. readonly means that most of the AM state must be left unchanged.
  • Ensure that the asm code in the block indeed acts on the AM state in the way described by the spec. The asm block can have arbitrary other side-effects not visible to the AM (unless it is marked pure or readonly), those don't matter. (This answers @newpavlov's question.) However, every part of the asm state that the compiler relies on to implement the AM semantics must be left intact. Note that this step might have to rely on how exactly the Rust compiler maps AM states to asm states; this mapping is in general considered unstable, so in principle you can only rely on what is documented about it. This mapping can also be implementation-specific. (The formal name for this mapping is "simulation relation" as it describes how the asm execution simulations the AM execution.)
  • Demonstrate that the exact same state transformation could be written in regular Rust code.

From then on, reasoning about the program can proceed on the AM level by treating the asm block as a black box that performs the AM transition picked in the first step.

For freeze, the last step fails: there is no Rust code that can achieve the AM state transition that the inline asm block is intended to provide. freeze is a somewhat special case in that I am not aware of optimizations that it actually breaks, but I would be extremely hesitant to permit any kind of deviation from the recipe laid out above. That recipe ensures that program analysis can assume the entire program is written in Rust, which is what MIR-level compiler optimizations inevitably will have to assume once they want to do more interesting transformations (e.g. based on the aliasing model).

2 Likes