Speakers
Description
eBPF users pay for verified safety with performance. Across 27 microbenchmarks extracted from production programs, code that reaches native speed when compiled directly is up to 2x slower through the eBPF pipeline. The gap is structural and cannot be closed by LLVM optimization passes or source code rewrites: every deployment runs on specific hardware under a specific workload, yet the pipeline is a single-pass JIT deliberately kept simple to keep a minimal trusted computing base (TCB), without many optimizations. For example, a 64-bit rotate costs 15 machine instructions in the eBPF JIT instead of one ROL. Hardware features and registers, and workload facts such as stable input patterns, map contents, and biased branches remain under-explored. Improving the JIT in place needs upstream acceptance, enlarges the TCB that years of formal-methods work have hardened, and grows per-architecture kernel code.
The talk covers two pieces that try to approach this problem with minimal additions to the kernel TCB. BpfReJIT is a userspace library built on LLVM: an in-process shim intercepts an unmodified application's load and attach calls, rewrites the bytecode based on configs, workloads, and the kernel version, and resubmits every candidate through the original verifier and JIT. It can perform runtime speculative optimization similar to V8 or the JVM, but separates correctness (ensured in userspace) from safety (ensured in the kernel). Kops is the part that needs a kernel patch and discussion. A small one-time patch adds an interface through which kernel modules can register new hardware-specific operations without further core changes. Each operation carries a proof sequence of vanilla eBPF instructions that the verifier checks on every load, plus a native emit that the JIT compiles. We can further leverage Lean 4 proofs to establish that the two compute the same result, so the emit is the only per-operation addition to the TCB. Seven hardware-idiom operations yield speedups of up to 24% on x86-64 and 22% on ARM64, and add up to 12% datapath throughput on Cilium and Katran. We would like feedback on the interface design, on where module-supplied emits sit in the kernel's trust story, and on when to apply an operation at all, since naively applying every matched site can regress.