Sep 2026· Proceedings of the 4th Workshop on eBPF and Kernel Extensions· pp. 41-49· 0 citations· 19 references
TL;DR
An extension to the compilation process with a post-verification optimization phase to address the eBPF verifier limitation and measure the performance overhead introduced by these restrictions.
Abstract
The eBPF runtime relies on a static program verifier to check safety properties of custom programs before they are executed in the kernel. In some cases, the verifier limits compiler optimizations because it cannot reason about the optimized code. Moreover, developers are forced to use costly abstractions to satisfy the verifier. We measure the performance overhead introduced by these restrictions and find that it can halve performance in a compute-heavy benchmark under workload with large number of iterations. Finally, we propose an extension to the compilation process with a post-verification optimization phase to address this limitation.
Modern optimizing compilers rely on heuristic search algorithms for NP-hard optimization problems, which can result in poor generated-code performance and long or unpredictable compile times. These are considered bugs by users, but verified compilers rarely reason beyond semantic preservation. We propose verifying perf...
eBPF allows user-defined programs to safely extend Linux kernel functionality at runtime, but its final machine code comes from a compilation pipeline that differs from native targets, and how efficient that pipeline is has no clear reference point. Our work constructs one: using the standard LLVM x86 backend as an app...
Hoang Duong, Hao Sun, Zhendong Su· Proceedings of the 4th Works...· 0 citations
This paper introduces the first verification-aware data-plane language: VeriLucid, which aims to unify programming and specification in one high-level language, with built-in proof automation.
John Sonchack, P. Zave, Jennifer Rexford· Conference on Applications,...· 0 citations
It is demonstrated that LLMs provided with specific optimization goals achieve better measured performance and validity rates when generating C code compared to creating computation pipelines and optimization schedules with established frameworks, suggesting that future development should explore alternative approaches...
Jiří Klepl, Matyáš Brabec, Martin Kruliš· 0 citations
This paper presents an incremental, classroom-scale approach to building a JIT compiler in manageable steps that successfully supports a Read-Eval-Print Loop and a first-call specialization mechanism.
Shaurya Raswan, Mark Barbone, Nicolás Lehmann et al.· Proceedings of the 27th ACM...· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
