Verified Peephole Optimizations for CompCert
Transformations over assembly code are common in many compilers. These transformations are also some of the most bug-dense compiler components. Such bugs could be eliminated by formally verifying the compiler, but state of the art formally verified compilers like CompCert do not support assembly-level program transformations. This paper presents Peek, a framework for expressing, verifying, and running meaning-preserving assembly-level program transformations in CompCert. Peek contributes four new components: a lower level semantics for CompCert x86 syntax, a liveness analysis, a library for expressing and verifying peephole optimizations, and a verified peephole optimization pass built into CompCert. Each of these is accompanied by a correctness proof in Coq against realistic assumptions about the calling convention and the system memory allocator.
Verifying peephole optimizations in Peek requires proving only a set of local properties, which we have proved are sufficient to ensure global transformation correctness. We have proven these local properties for 28 peephole transformations from the literature. We discuss the development of our new assembly semantics, liveness analysis, representation of program transformations, and execution engine; describe the verification challenges of each component; and detail techniques we applied to mitigate the proof burden.
Thu 16 JunDisplayed time zone: Tijuana, Baja California change
15:30 - 17:00
Verifying SystemsResearch Papers at Grand Ballroom Santa Ynez
Chair(s): Santosh Nagarakatte Rutgers University
|Rehearsal: A Configuration Verification Tool for Puppet|
Rian Shambaugh University of Massachusetts Amherst, Aaron Weiss University of Massachusetts Amherst, Arjun Guha University of Massachusetts, AmherstPre-print Media Attached
|Toward Compositional Verification of Interruptible OS Kernels and Device Drivers|
Hao Chen Yale University, Xiongnan (Newman) Wu Yale University, Zhong Shao Yale University, Joshua Lockerman Yale University, Ronghui Gu Yale UniversityPre-print Media Attached
|Verified Peephole Optimizations for CompCert|
Eric Mullen University of Washington, Daryl Zuniga University of Washington, Zachary Tatlock University of Washington, Seattle, Dan Grossman University of Washington, USAPre-print Media Attached