Speaker
Description
The eBPF instruction set has quietly grown a concurrency surface: load_acquire/store_release instructions, arena atomics now JIT-compiled across x86, arm64, riscv and powerpc, resilient queued spinlocks, and lock-free ring buffers. eBPF programs routinely run concurrently across CPUs and increasingly coordinate through shared memory. Yet unlike the Linux kernel — which has a formal, herd7-executable memory model (LKMM) and the klitmus7 tool to exercise it — eBPF has no formal memory model and no way to check that the ordering a program requests actually survives the verifier and each architecture's JIT.
This talk presents blitmus (https://github.com/puranjaymohan/blitmus), a tool that converts standard LKMM litmus tests into eBPF programs and runs them on real hardware. Each process of a litmus test becomes a BPF program pinned to a specific CPU; a userspace harness races them across millions of iterations, histograms the outcomes, and compares them against the test's exists clause and expected result — the same methodology klitmus7 and herd7 use, but exercising the BPF runtime end to end. Because the same litmus test can be run unchanged on every architecture, blitmus can surface JIT ordering bugs (e.g. a missing barrier for cmpxchg) that are otherwise silent and catastrophic for concurrent BPF code.
I will demo the tool converting and running the LKMM litmus suite through BPF, walk through the results on aarch64 and x86-64 (including weak behaviors observed for store-buffering and a Result: Never test that blitmus flags as violated), and use that case to discuss tool fidelity: how faithfully a batched, test-run-based harness models true multi-CPU races, and where the current barrier/interleaving strategy needs to improve.
I would like to use the session to discuss next steps with the community:
(1) growing the harness to cover BPF-specific primitives — arena spinlocks, rqspinlock, ring buffer reserve/commit ordering, per-CPU maps;
(2) a proper litmus parser and cross-architecture CI (qemu on riscv/ppc/s390/loongarch) wired into selftests/bpf as a memory-model conformance suite;