[$] The challenge of compiling for verified architectures

On its surface, the BPF virtual machine resembles many other computer
architectures; it has registers and instructions to perform the usual
operations. But there is a key difference: BPF programs must pass the
kernel's verifier before they can be run. The verifier imposes a long list
of additional restrictions so that it can prove to itself that any given
program is safe to run; getting past those checks can be a source of
frustration for BPF developers. At the 2023 GNU Tools Cauldron,
José Marchesi looked at the problem of compiling for verified architectures
and how the compiler can generate code that will pass verification.