Applying Formal Verification to Microkernel IPC at Meta
We use Iris, an implementation of concurrent separation logic in the Coq proof assistant, to verify two queue data structures used for inter-process communication in an operating system under development. Our motivations are twofold. First, we wish to leverage formal verification to boost confidence in a delicate piece of industrial code that was subject to numerous revisions. Second, we aim to gain information on the cost-benefit tradeoff of applying a state-of-the-art formal verification tool in our industrial setting.
On both fronts, our endeavor has been a success. The verification effort proved that the queue algorithms are correct and uncovered four algorithmic simplifications as well as bugs in client code. The simplifications involve the removal of two memory barriers, one atomic load, and one boolean check, all in a performance-sensitive part of the OS. Removing the redundant boolean check revealed unintended uses of uninitialized memory in multiple device drivers, which were fixed.
The proof work was completed in person months, not years, by engineers with no prior familiarity with Iris. These findings are spurring further use of verification at CompanyX.
Mon 17 JanDisplayed time zone: Eastern Time (US & Canada) change
10:20 - 12:00
|Specification and Verification of a Transient StackDistinguished Paper AwardRemote|
CPPDOI Pre-print Media Attached File Attached
|Mechanized Verification of a Fine-Grained Concurrent Queue from Meta’s Folly LibraryRemote|
Simon Friis Vindum Aarhus University, Lars Birkedal Aarhus University, Dan Frumin University of GroningenPre-print Media Attached
|Applying Formal Verification to Microkernel IPC at MetaInPerson|
Quentin Carbonneaux Meta, Noam Zilberstein Cornell University, Christoph Klee Facebook, Peter W. O'Hearn Meta; University College London, Francesco Zappa Nardelli MetaPre-print
|Certified Abstract Machines for Skeletal SemanticsRemote|
CPPPre-print Media Attached