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

Note that I say it's not freeze not due to the implementation—that's fine—but because angelic nondeterminism is the incorrect spec for what we want freeze to be. freeze wants demonic nondeterminism, but there's no established way to specify that an initialized byte remains as-is and an uninitialized byte is replaced with a demonically selected nondeterministic value.

(Choose a random value, and its always the one that you want it to be is angelic. Choose a random value, and its always the one that causes the most issues is demonic. Demonic nondeterminism is fairly easy to optimize around. Angelic nondeterminism can cause optimization issues very easily.)

It may be the case that dropping down to x86 asm! implicitly freezes any value that passes through a register, as the physical machine cannot represent an abstract byte that is uninitialized. Or it may be that putting uninitialized into a physical machine register is UB. I don't think the latter is really useful in any way other than maintaining "freeze is UB" as a property, and that's a contributing factor to why I think we will end up exposing freeze in some form.

You cannot force the AM to do something it cannot do just by dropping down to asm!. But specifying freeze properly in the AM is not the hard part, at all. It's justifying the implications of introducing a new primitive nondeterministic operation to the AM.

Unfortunately, while convenient, this is a misleading partial truth. You still need to be able to define the transition function that the asm! implements, and if that definition relies on implementation details of how the AM is lowered to the target machine, you're opening yourself up to conflicts with optimization passes that (rightly) assume that those details cannot be observed from within conformant (UB free) code.

1 Like