Carbonneaux, Q; Zilberstein, N; Klee, C; O'Hearn, PW; Zappa Nardelli, F; (2022) Applying formal verification to microkernel IPC at meta. In: CPP 2022 - Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2022. (pp. pp. 116-129). Association for Computing Machinery (ACM)

Preview

Text 3497775.3503681.pdf - Published Version Download (258kB) | Preview

Abstract

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 Meta.

Download activity - last month

Export as XMLCSVJSON

Download activity - last 12 months

Export as CSVJSONXML

Downloads by country - last 12 months

Export as XMLCSVJSON

Archive Staff Only

View Item