> Yeah, I'm not sure that's accurate, and even if it were, I'm not sure that's relevant.
The size of the verifier and runtime is absolutely relevant to keeping the TCB down to a manageable level.
> The description of the addressing modes in eBPF [1] means each instruction is polymorphic just like in WASM, yielding a multiplicative explosion in instructions in both cases.
There's two very different ISAs being described in that doc, the classic BPF from the 90s that resembled a CISC architectre with tons of addressing modes, and the more RISC-esque eBPF that only has the one.
> Furthermore, the "extras" in WASM amounts to supporting floating point, different integral types other than 32-bit int, function calling instructions and basic loops. Hardly revolutionary or difficult to implement. Once you add those with the requisite polymorphic instructions, eBPF and WASM aren't so dissimilar. You could argue those aren't necessary, and yet they unarguably make WASM a more attractive target, and the instructions can be specifically optimized in ways that simulating them cannot be.
I described above how they're different, and how that helps simplify the in kernel work for eBPF.
> Translation: eBPF isn't fast. The majority of performance in virtual machines is from decent register allocation.
The register allocation is done by the untrusted code and is only verified by the runtime. You can still achieve very good register usage.
>> [eBPF is a] load/store architecture, so for the vast majority of cases for both CISC and RISC architectures, there's a one to one correlation between eBPF instructions and native processor instructions, also greatly simplifying code generation.
> This is shared by WASM.
Your [] block is telling. It cut off the first half of that clause which is necessary for my comment to make sense. WASM is a stack based machine which means you have a strict choice between fast JITed and a dead simple code generator. The two address register instruction part that you cut off is an extremely important part of that.
> Does not follow. CPP is guaranteed to terminate as well, and yet you can easily write macros [2] that will blow up CPP at compile-time because the generated expression is so large. Not Turing complete does entail "tractable".
I'm not sayig that it's tractable because it's turing incomplete; I'm saying that it's Turing incomplete because it's tractable. It's tractable because the code flow graph is a DAG with non infinite code size. The macro example doesn't apply because there's no in kernel expansion like that.
> Useful, but this has also been done for Turing complete languages as well
It's only been done for Turing complete languages by keeping to a Turing incomplete subset. That's how sel4 works for instance.
> so there's no a priori reason to think you can't get 90% of the same effect with WASM, and without the expressiveness headaches of dealing with non-Turing completeness.
It's the other 10% that worries me. : ) Yeah, you can get 90% of the way there in WASM, but that doesn't cut it for the use case.
> As for verification, yes limiting expressiveness is useful for making certain properties trivial, but it also makes your tool less useful.
Limiting expressiveness is the only way to get to verification. That's a natural consequence of the Halting problem. If you want to do crazy town stuff like getting to the point of running multi-tenant untrusted user code in kernel space, including in interrupt handlers, then you need to reduce expressiveness. Hell, even if you're compiling a regular kernel module you need to reduce expressiveness because of the environment.