University of Minnesota
Software Engineering Center

You are here

Research Seminar: End-to-End Verified Compositional Compilation to Machine Code

Date of Event: 
Tuesday, December 10, 2019 - 10:00am to 11:00am
6-212 Keller Hall, 200 Union Street S.E., Minneapolis, MN 55455

Speaker: Dr. Yuting Wang

Abstract: A key ingredient contributing to the success of CompCert, the state-of-the-art verified compiler for C, is its block-based memory model, which is used uniformly for all of its languages and their verified compilation. However, CompCert's memory model lacks an explicit notion of stack. Its target assembly language represents the runtime stack as an unbounded list of memory blocks, making further compilation of CompCert assembly into more realistic machine code difficult since it is not possible to merge these blocks into a finite and continuous stack. Furthermore, various notions of verified compositional compilation rely on some kind of mechanism for protecting private stack data and enabling modification to the public stack-allocated data, which is lacking in the original CompCert. These problems have been investigated but not fully addressed before, in the sense that some advanced optimization passes that significantly change the ways stack blocks are (de-)allocated, such as tailcall recognition and inlining, are often omitted.

We propose a lightweight and complete solution to the above problems. It is based on the enrichment of CompCert's memory model with an abstract stack that keeps track of the history of stack frames to bound the stack consumption and that enforces a uniform stack access policy by assigning fine-grained permissions to stack memory. Using this enriched memory model for all the languages of CompCert, we are able to reprove the correctness of the _full_ compilation chain of CompCert, including all the optimization passes. In the end, we get Stack-Aware CompCert, a complete extension of CompCert that compiles to an assembly language with a realistic stack model and that supports a form of compositional compilation called _contextual compilation_ by exploiting the uniform stack-access policy. Based on Stack-Aware CompCert, we further develop CompCertElf, the first extension of CompCert that compiles to a standard binary file format, i.e, the ELF object format.

Speaker Bio: Yuting Wang is currently an associate research scientist at Yale University, working in Dr. Zhong Shao's group. He will be joining the John Hopcroft Center for Computer Science at the Shanghai Jiao Tong University, China as a tenure-tracked associate professor in March 2020. Prior to Yale, he was a Ph.D. student at the University of Minnesota, Twin Cities, supervised by Dr. Gopalan Nadathur. His research interests include the theory, implementation and application of programming languages and verification frameworks. In particular, he is interested in the methodologies and tools for verification of system software such as compilers and operating systems. He is currently part of the DeepSpec project, an "Expedition in Computing" funded by NSF and jointly carried out by Yale University, Princeton University, University of Pennsylvania and MIT. His main focus in this project is to provide verified compilation support that connects the verification efforts at different levels together, such as connecting verified compilers with formal semantics of different architectures including ARM, X86 and RISC-V and combination of the user-level verified programs with verified OS kernels. He is also a core developer of Abella, an interactive theorem prover particularly suitable for the formalization and verification of meta-properties of programming languages and logics.