CompCertTSO is a compiler that generates x86 assembly code from ClightTSO, a large subset of the C programming language enhanced with concurrency primitives for thread management and synchronisation, and with a TSO relaxed memory model based on the x86-TSO model. The development is based on the CompCert compiler from sequential Clight to PowerPC and ARM (developed by Leroy et al., INRIA). The CompCertTSO compiler is written mostly within the specification language of the Coq proof assistant, and the correctness of that part has been proved within Coq: for any legal ClightTSO program, any behaviour of the generated code in the x86-TSO semantics is allowed by the ClightTSO semantics of the source program, in the absence of out-of-memory errors.
The first paper below describes the whole project, including a correctness proof covering all the compiler phases (from the ClightTSO AST to symbolic assembly).
A preliminary high-level description of the CompCertTSO compiler appeared in POPL 2011 (the second paper below). That described the overall structure of the compiler and proof, then completed only for key phases.
Later work on verifying fence eliminations, in SAS 2011, added additional verified phases to remove some redundant MFENCE instructions, as described in the third paper below.
This Web site gives a commented listing of the underlying Coq specifications and proofs. Proof scripts and the parts of the compiler written directly in Caml are omitted. This development is a work in progress; some parts have substantially changed since the overview paper above was written. Here is a brief change log.
This document and the CompCertTSO sources are copyright 2005, 2006, 2007, 2008, 2009, 2010, 2011 Institut National de Recherche en Informatique et en Automatique (INRIA), and Suresh Jagannathan, Jaroslav Sevcik, Peter Sewell, and Viktor Vafeiadis. The document and sources are distributed under the terms of the following license.
This work is associated with a broader project on Relaxed-Memory Concurrency.
|
Pass | Source & target | Compiler code | Correctness proof |
---|---|---|---|
Simplification of control structures; explication of type-dependent computations |
Clight to Csharpminor | Cshmgen | Cshmgenproof1 Cshmgenproof2 Cshmgenproof3 |
Stack allocation of local variables whose address is taken |
Csharpminor to Cstacked | (none) |
Cstackedproofsimdef Cstackedproofunbuffer Cstackedproofalloc Cstackedprooffree Cstackedprooftau Cstackedproof |
Simplification of switch statements | Csharpminor to Cminor | Cminorgen | Cminorgenproof |
Recognition of operators and addressing modes |
Cminor to CminorSel | Selection SelectOp |
CminorP Selectionproof SelectOpproof |
Construction of the CFG, 3-address code generation |
Cminor to RTL | RTLgen |
RTLgenspec RTLgenproof |
Constant propagation | RTL to RTL | Constprop ConstpropOp |
Constpropproof ConstproppOproof |
Common subexpression elimination | RTL to RTL | CSE | CSEproof |
Fence elimination (scheme 1) | RTL to RTL | Fenceelim | Fenceelimproof |
Selected fence introduction to improve subsequent fence elimination |
RTL to RTL | Fenceintro2 | Fenceintro2proof |
Fence elimination (scheme 2) | RTL to RTL | Fenceelim2 | Fenceelim2proof |
Register allocation by coloring of an interference graph |
RTL to LTL | InterfGraph Coloring Allocation |
Coloringproof Allocproof |
Branch tunneling | LTL to LTL | Tunneling | Tunnelingproof |
Linearization of the CFG | LTL to LTLin | Linearize | Linearizeproof |
Spilling, reloading, calling conventions | LTLin to Linear | Conventions Reload |
Parallelmove Reloadproof |
Laying out the activation records | Linear to Mach |
Bounds Stacking |
Stackingproof |
Storing the activation records in memory | Mach to Mach | (none) |
Asmgenretaddr MMperthreadsimdef MMproofaux MMperthreadsimproof MMtsoaux MMtsosimproof MMproof |
Emission of assembly code | Mach to Asm | Asmgen |
Asmgenproof1 Asmgenproof |