Trustworthy Systems

Code optimizations using formally verified properties

Authors

Yao Shi, Bernard Blackham and Gernot Heiser

NICTA

UNSW

Abstract

Formal program verification offers strong assurance of cor- rectness, backed by the strength of mathematical proof. Con- structing 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 ver- ification 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 in- formation 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%.

BibTeX Entry

  @inproceedings{Shi_BH_13,
    address          = {Indianapolis, USA},
    author           = {Shi, Yao and Blackham, Bernard and Heiser, Gernot},
    booktitle        = {Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA)},
    keywords         = {compiler_opt},
    month            = oct,
    pages            = {427--442},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/7246.pdf},
    slides           = {https://trustworthy.systems/publications/nicta_slides/7246.pdf},
    title            = {Code Optimizations Using Formally Verified Properties},
    year             = {2013}
  }

Download