Code optimizations using formally verified properties

Abstract

Formal program verification offers strong assurance of correctness, backed by the strength of mathematical proof. Constructing these proofs requires humans to identify program invariants, and show that they are always maintained. These invariants are then used to prove that the code adheres to its specification.

In this paper, we explore the overlap between formal verification and code optimization. We propose two approaches to reuse the invariants derived in formal proofs and integrate them into compilation. The first applies invariants extracted from the proof, while the second leverages the property of program safety (i.e., the absence of bugs). We reuse this information to improve the performance of generated object code.

We evaluated these methods on seL4, a real-world formally-verified microkernel, and obtained improvements in average runtime performance (up to 28%) and in worst-case execution time (up to 25%). In macro-benchmarks, we found the performance of para-virtualized Linux running on the microkernel improved by 6-16%.

References

1. E. Alkassar, M. Hillebrand, D. Leinenbach, N. Schirmer, and A. Starostin. The Verisoft approach to systems verification. In N. Shankar and J. Woodcock, editors, VSTTE 2008, volume 5295 of LNCS, pages 209--224. Springer, 2008.
2. J. Andronick, B. Chetali, and C. Paulin-Mohring. Formal Verification of Security Properties of Smart Card Embedded Source Code. In J. Fitzgerald, I. J. Hayes, and A. Tarlecki, editors, FM, volume 3582 of LNCS, pages 302--317, Newcastle, UK, Jul 2005. Springer.
3. Y. Bertot, B. Gregoire, and X. Leroy. A structured approach to proving compiler optimizations based on dataflow analysis. In Types for Proofs and Programs, Workshop TYPES 2004, volume 3839 of LNCS, pages 66--81, 2006.
4. B. Blackham and G. Heiser. Correct, fast, maintainable - choose any three! In 3rd APSys, pages 13:1--13:7, Seoul, Korea, Jul 2012.
5. B. Blackham, Y. Shi, S. Chattopadhyay, A. Roychoudhury, and G. Heiser. Timing analysis of a protected operating system kernel. In 32nd RTSS, pages 339--348, Vienna, Austria, Nov 2011.
6. S. Blazy and X. Leroy. Formal verification of a memory model for C-like imperative languages. In International Conference on Formal Engineering Methods, vol. 3785 of LNCS, pages 280--299, 2005.
7. S. Blazy, Z. Dargaye, and X. Leroy. Formal verification of a C compiler front-end. In 14th FM, volume 4085 of LNCS, pages 460--475. Springer, 2006.
8. M. Daum, N. W. Schirmer, and M. Schmidt. From operating-system correctness to pervasively verified applications. In IFM, volume 6396 of LNCS, pages 105--120, Nancy, France, 2010. Springer.
9. R. J. Feiertag and P. G. Neumann. The foundations of a provably secure operating system (PSOS). In AFIPS Conf. Proc., 1979 National Comp. Conf., pages 329--334, New York, NY, USA, Jun 1979.
10. L. Gu, A. Vaynberg, B. Ford, Z. Shao, and D. Costanzo. CertiKOS: A certified kernel for secure cloud computing. In 2nd APSys, 2011.
11. C. L. Heitmeyer, M. Archer, E. I. Leonard, and J. McLean. Formal specification and verification of data separation in a separation kernel for an embedded system. In CCS, pages 346--355, Alexandria, VA, USA, 2006.
12. M. Hohmuth and H. Tews. The VFiasco approach for a verified operating system. In 2nd PLOS, Glasgow, UK, Jul 2005.
13. G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. seL4: Formal verification of an OS kernel. In 22nd SOSP, pages 207--220, Big Sky, MT, USA, Oct 2009. ACM.
14. X. Leroy. Formal certification of a compiler back-end, or: Programming a compiler with a proof assistant. In J. G. Morrisett and S. L. P. Jones, editors, 33rd POPL, pages 42--54, Charleston, SC, USA, 2006. ACM.
15. J. Liedtke. On μ-kernel construction. In 15th SOSP, pages 237--250, Copper Mountain, CO, USA, Dec 1995.
16. A. Ramirez, J. l. Larriba-pey, C. Navarro, J. Torrellas, and M. Valero. Software trace cache. In 13th Intl. Conference on Supercomputing, 1999.
17. S. Rideau and X. Leroy. Validating register allocation and spilling. In Compiler Construction, volume 6011 of LNCS, pages 224--243, 2010.
18. T. Sewell, M. Myreen, and G. Klein. Translation validation for a verified OS kernel. In PLDI, pages 471--481, Seattle, Washington, USA, Jun 2013. ACM.
19. H. Tews, T. Weber, and M. Völp. A formal model of memory peculiarities for the verification of low-level operating-system code. In R. Huuck, G. Klein, and B. Schlich, editors, 3rd SSV, volume 217 of ENTCS, pages 79--96, Sydney, Australia, Feb 2008. Elsevier.
20. The GCC Team. GCC 4.8 release series: Changes, new features, and fixes. http://gcc.gnu.org/gcc-4.8/changes.html, 2013.
21. J.-B. Tristan and X. Leroy. Formal verification of translation validators: A case study on instruction scheduling optimizations. In 35th POPL, pages 17--27, 2008.
22. J.-B. Tristan and X. Leroy. Verified validation of lazy code motion. In 2009 PLDI, pages 316--326, 2009.
23. J.-B. Tristan and X. Leroy. A simple, verified validator for software pipelining. In 37th POPL, pages 83--92, 2010.
24. M. T. Vandevoorde. Specifications can make programs run faster. In Theory and Practice of Software Development, LNCS, volume 668, pages 215--229, 1993.
25. B. J. Walker, R. A. Kemmerer, and G. J. Popek. Specification and verification of the UCLA Unix security kernel. CACM, 23 (2): 118--131, 1980.
26. X. Wang, H. Chen, A. Cheung, Z. Jia, N. Zeldovich, and M. F. Kaashoek. Undefined behavior: what happened to my code? In 3rd APSys, pages 9:1--9:7, New York, NY, USA, 2012. ACM.
27. J. Whaley and M. S. Lam. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In 2004 PLDI, 2004.
28. R. Wilhelm, J. Engblom, A. Ermedahl, N. Holsti, S. Thesing, D. Whalley, G. Bernat, C. Ferdinand, R. Heckmann, T. Mitra, F. Mueller, I. Puaut, P. Puschner, J. Staschulat, and P. Stenström. The worst-case execution-time problem - overview of methods and survey of tools. ACM Trans. Emb. Comput. Syst., 7 (3): 1--53, 2008. ISSN 1539-9087.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Performance

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Formal software verification

  • Software notations and tools

    • Compilers

  • Software organization and properties

    • Extra-functional properties

      • Software performance

    • Software functional properties

      • Formal methods