eBPF is no longer a single-platform technology. It runs in the Linux kernel, on Windows, in user space, on microcontrollers, and in blockchain virtual machines, on independently built runtimes. The IETF ISA standard, RFC 9669, pins down the core instructions but leaves out features that real programs depend on, such as helper functions and maps. We are building an executable formal semantics for eBPF in F* that explicitly distinguishes cross-platform and platform-specific behaviors. Our semantics passes the BPF conformance test suite on par with uBPF, bpftime, Linux, and Windows, and we are extending it beyond the core ISA to other shared features the RFC omits. Using Meta-F* metaprogramming, we can also generate prose specifications in structured English that provably match the model. We envision this semantics as a practical foundation for a uniform, trustworthy eBPF across platforms.
Yan-Ze Li, Reto Achermann, Ivan Beschastnikh et al.· Proceedings of the 4th Works...· 0 citations
Verifying low-level system code requires reasoning about how software interacts with the hardware environment on which it runs. Typically, this means specifying an abstract model of the hardware and verifying the code against it. However, the validity of the verification result depends on the accuracy of the formalized hardware model. Unfortunately, validating the accuracy of the formalized hardware model is hard. It not only requires relating the model's specification to the observable behavior of real hardware, but also involves many invisible internal microarchitectural steps that influence the observable execution of a modern processor. We present a methodology that lets us validate an abstract formal model against real hardware by generating test cases, executing them on real hardware to capture traces of observable behavior, and finally employing a synthesis approach to identify the internal microarchitectural steps that explain the observable behavior. We discuss this methodology for an x86 MMU model of TLB and page-table behavior, using model-specific state reductions to keep test generation and synthesis tractable and to illustrate how similar reduction arguments can apply in other hardware-model contexts.
Rishika Varma Kalidindi, Reto Achermann· Proceedings of the 14th Work...· 0 citations
This paper proposes a deployment scheme for agentic workloads tailored for serverless, accompanied by pre-warming policies that minimize the idle resource footprint and startup latencies and outlines promising research directions for serverless agents.
Ian Dougherty, Natalie Lambert, Joshua Wang et al.· ACM SIGOPS Operating Systems...· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
