The CompCertTSO compiler

Commented Coq development

Version 1.13.8255

Introduction

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.

Papers

People

Suresh Peter Jaroslav Viktor Francesco

Code

General-purpose libraries, data structures and algorithms

Definitions and theorems used in many parts of the development

Source, intermediate and target languages: syntax and semantics

Compiler passes

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

Type systems

Trivial type systems are used to statically capture well-formedness conditions on the source and intermediate languages. Proofs that compiler passes are type-preserving:

All together


[Validate this page.]