Code Optimizations Using Formally Verified Properties

Select |




Print


Shi, Yao; Blackham, Bernard; Heiser, Gernot

Shi, Yao; Blackham, Bernard; Heiser, Gernot


2013-10-26


Conference Material


Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications


Indianapolis, USA


427-442


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


compiler_opt


http://splashcon.org/2013/cfp/618


nicta:7246


Shi, Yao; Blackham, Bernard; Heiser, Gernot. Code Optimizations Using Formally Verified Properties. In: Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications; Indianapolis, USA. 2013-10-26. 427-442.



Loading citation data...

Citation counts
(Requires subscription to view)