4 ms·

I have a tangential question, more about BPF in general: I watched a presentation recently by one of the core BPF contributors, in which they paint it as a saf

I have a tangential question, more about BPF in general: I watched a presentation recently by one of the core BPF contributors, in which they paint it as a safer, extended version of C: https://www.youtube.com/watch?v=K08YCgALHDo https://www.youtube.com/watch?v=K08YCgALHDo Is there any reason why you wouldn't want to use this to write regular, user-land applications instead of C? Could you? (I don't know much about BPF in general)

javierhonduco 4y ago
(this talk is great!) I think this would be cool. Have you considered asking Alexei directly?
- gavinray 4y ago
  I did email the BPF kernel mailing list, they directed me to two user-land (user-space?) implementations of BPF but didn't say much about what "user-space BPF" meant. Didn't want to clutter up the mailing list with noise so I didn't reply: https://lore.kernel.org/bpf/Y3BQGgcCMaSptEFJ@google.com/T/#t https://lore.kernel.org/bpf/Y3BQGgcCMaSptEFJ@google.com/T/#t
hawski 4y ago
AFAIU BPF does not have loops as it is designed to be assured the execution has an end.
- javierhonduco 4y ago
  That's right! There's no "traditional" loops as programs have to be proved to terminate at some point. That being said, very recently support for bounded loops landed [0]. It's very exciting and useful, and I've seen it reduce verification times significantly, but we can't use this yet as it requires kernel 5.3 or greater, and we would like to support as many users as possible! [0]: https://lwn.net/Articles/877062/ https://lwn.net/Articles/877062/ [1]: https://github.com/iovisor/bcc/commit/38304256c49a02aecbf78f2fdc4b86d95eb8df9f https://github.com/iovisor/bcc/commit/38304256c49a02aecbf78f...
tptacek 4y ago
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.
- sudosysgen 4y ago
  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.
  - tptacek 4y ago
    The only thing Rust keeps you from implementing are trees. It's at least OK with loops! :)
    - sudosysgen 4y ago
      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.
    - saagarjha 4y ago
      Rust is fine with trees, no? No cycles and all that. It's arbitrary graphs that are hard.
- gavinray 4y ago
  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.

javierhonduco 4y ago

(this talk is great!) I think this would be cool. Have you considered asking Alexei directly?

gavinray 4y ago
I did email the BPF kernel mailing list, they directed me to two user-land (user-space?) implementations of BPF but didn't say much about what "user-space BPF" meant. Didn't want to clutter up the mailing list with noise so I didn't reply: https://lore.kernel.org/bpf/Y3BQGgcCMaSptEFJ@google.com/T/#t https://lore.kernel.org/bpf/Y3BQGgcCMaSptEFJ@google.com/T/#t

hawski 4y ago

AFAIU BPF does not have loops as it is designed to be assured the execution has an end.

javierhonduco 4y ago
That's right! There's no "traditional" loops as programs have to be proved to terminate at some point. That being said, very recently support for bounded loops landed [0]. It's very exciting and useful, and I've seen it reduce verification times significantly, but we can't use this yet as it requires kernel 5.3 or greater, and we would like to support as many users as possible! [0]: https://lwn.net/Articles/877062/ https://lwn.net/Articles/877062/ [1]: https://github.com/iovisor/bcc/commit/38304256c49a02aecbf78f2fdc4b86d95eb8df9f https://github.com/iovisor/bcc/commit/38304256c49a02aecbf78f...

tptacek 4y ago

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.

sudosysgen 4y ago
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.
- tptacek 4y ago
  The only thing Rust keeps you from implementing are trees. It's at least OK with loops! :)
  - sudosysgen 4y ago
    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.
  - saagarjha 4y ago
    Rust is fine with trees, no? No cycles and all that. It's arbitrary graphs that are hard.
gavinray 4y ago
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.