Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Fri 18 Jan 2019 16:59 - 17:21 at Sala I - Verified Compilation and Concurrency Chair(s): Michael Greenberg

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 enforces the finiteness of the stack and fine-grained stack permissions.

Based on Stack-Aware CompCert, we develop CompCertMC, the first extension of CompCert that compiles into a low-level language with flat memory spaces. Based on CompCertMC, we develop Stack-Aware CompCertX, a complete extension of CompCert that supports a notion of compositional compilation that we call contextual compilation by exploiting the uniform stack access policy provided by the abstract stack.

An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code (popl19.pdf)135KiB

Fri 18 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

16:37 - 17:43: Verified Compilation and ConcurrencyResearch Papers at Sala I
Chair(s): Michael GreenbergPomona College
16:37 - 16:59
A Calculus for Esterel: If can, can. If no can, no can.
Research Papers
Spencer P. FlorenceNorthwestern University, USA, Shu-Hung YouNorthwestern University, USA, Jesse A. TovNorthwestern University, Department of Electrical Engineering and Computer Science, Robby FindlerNorthwestern University, USA
Link to publication DOI Media Attached File Attached
16:59 - 17:21
An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code
Research Papers
Yuting WangYale University, Pierre WilkeYale University, Zhong ShaoYale University
Link to publication DOI Media Attached File Attached
17:21 - 17:43
A Verified, Efficient Embedding of a Verifiable Assembly Language
Research Papers
Aymeric FromherzCarnegie Mellon University, Nick GiannarakisPrinceton University, Chris HawblitzelMicrosoft Research, Bryan Parno, Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft Research
Link to publication DOI Media Attached File Attached