I like to joke that BPF-verified C is the future of memory-safe systems code, not Rust. It's a joke because you can't express most programs in verified BPF. The reason BPF is safe, despite the seeming theoretical impossibility of program verification, is that the verifier rejects most "valid" programs. To give a simple example: every loaded BPF program must provably halt, so any loop in a BPF program must be bounded in a way that the verifier can prove. And bounded loops, where you can see just from the AST that the loop can only tick N times, are a recent eBPF verifier innovation.
The way you build serious systems with BPF is that you couple a tiny straight-line BPF kernel that generates events with a userland program that consumes the events and does interesting stuff.
Ah, that sounds like a pretty serious limitation. Do you think they might relax this restriction in the future?
In the talk, he mentions adding higher-level constructs to C like lists and RB-trees that are also concurrently-safe(!!) which seem just massive to me.
It'd be stellar to be able to program in a safe C subset with some higher-level affordance like this.
Having worked with eBPF for a while now, it’s actually interesting how it makes you think about useful limits, that we typically defer thinking about. For example instead of writing code that validates a string and then doesn’t care about the length anymore we just always limit it to only process a certain length in the first place. I’ve found few problems that I couldn’t find useful limits for.
That’s not to say that the verifier isn’t limiting and at time difficult to deal with, but I find it less of a limitation in practice than it seems at first. Much like rust’s borrow checker I do think it takes a change in mindset.
//edit
Turns out being thoughtful about this when writing the code is also helpful for performance reasons as things like loops can be unrolled which can have significant performance gains.
I think they'll make incremental progress at accepting more programs, but that BPF-C programs aren't going to look like normal C programs any time in the near future.
There's a bunch of data structures available to BPF programs, because they can call "helpers", which are just ordinary C functions. There are concurrent semi-durable key-value stores of varying types (eBPF "maps"). These aren't written in BPF-C; they're just kernel code that BPF gets to call.
Adding new helpers is not nontrivial; you can't just load them into your kernel and call them; they're part of the kernel API.
This is true of Rust as well. The Rust type system is just a formal verifier for memory safety which rejects most memory safe programs. Of course Rust will accept more memory safe programs than eBPF.
That's not really the point I'm trying to make. There are programs that are literally memory safe that don't compile, that may be using any data structure you can think of.
The way you build serious systems with BPF is that you couple a tiny straight-line BPF kernel that generates events with a userland program that consumes the events and does interesting stuff.