[$] The challenge of compiling for verified architectures

On its surface, the BPF virtual machine resembles many other computerarchitectures; it has registers and instructions to perform the usualoperations. But there is a key difference: BPF programs must pass thekernel's verifier before they can be run. The verifier imposes a long listof additional restrictions so that it can prove to itself that any givenprogram is safe to run; getting past those checks can be a source offrustration for BPF developers. At the 2023 GNU Tools Cauldron,Jose Marchesi looked at the problem of compiling for verified architecturesand how the compiler can generate code that will pass verification.