BPF Memory Model Two Years On
summary
A concrete BPF memory model is proposed that honors dependencies and maps BPF instructions to specific ordering guarantees: exchange/compare-exchange = full ordering, add/or/xor (no fetch) = unordered, fetch variants = full ordering. JITs and compilers must either emit matching branches and loads, insert lightweight ordering via a dummy atomic (bpmb), or explicitly preserve address/control/data dependencies; experiments use GCC/clang builtins on Godbolt and show expected behavior but some backends lack support. Future work considers acquire/release loads/stores and formal verification tooling.
AI-written summary · about
chapters (8)
- 0:00Introduction and motivation
- 3:28BPF instruction set memory model
- 9:03Atomic instructions ordering
- 12:18Conditional jumps and control dependencies
- 21:50Load instructions and address dependencies
- 23:56JIT strategies for memory ordering
- 28:10Loads and stores implementation
- 30:56Future work and expansions
related talks
45mSupporting BPF in the GNU Toolchain
36mThe journey of BPF from restricted C language towards extended and safe C.
47mBPF: The Status of BTF, producers, consumers.
34mWhat's new in the BPF world?
43mHotBPF++: A More Powerful Memory Protection for the Linux Kernel
32meBPF: BPF kernel infrastructure
28mDeveloping Modern eBPF Applications
46mbpftrace internals