Thu 16 Jun 2016 16:30 - 17:00 at Grand Ballroom Santa Ynez - Verifying Systems Chair(s): Santosh Nagarakatte

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 Jun

pldi-2016-papers
15:30 - 17:00: Research Papers - Verifying Systems at Grand Ballroom Santa Ynez
Chair(s): Santosh NagarakatteRutgers University
pldi-2016-papers15:30 - 16:00
Talk
Rian ShambaughUniversity of Massachusetts Amherst, Aaron WeissUniversity of Massachusetts Amherst, Arjun GuhaUniversity of Massachusetts, Amherst
Pre-print Media Attached
pldi-2016-papers16:00 - 16:30
Talk
Hao ChenYale University, Xiongnan (Newman) WuYale University, Zhong ShaoYale University, Joshua LockermanYale University, Ronghui GuYale University
Pre-print Media Attached
pldi-2016-papers16:30 - 17:00
Talk
Eric MullenUniversity of Washington, Daryl ZunigaUniversity of Washington, Zachary TatlockUniversity of Washington, Dan GrossmanUniversity of Washington, USA
Pre-print Media Attached