CompCertTSO
- 1 June 2013
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 60 (3), 1-50
- https://doi.org/10.1145/2487241.2487248
Abstract
In this article, we consider the semantic design and verified compilation of a C-like programming language for concurrent shared-memory computation on x86 multiprocessors. The design of such a language is made surprisingly subtle by several factors: the relaxed-memory behavior of the hardware, the effects of compiler optimization on concurrent code, the need to support high-performance concurrent algorithms, and the desire for a reasonably simple programming model. In turn, this complexity makes verified compilation both essential and challenging. We describe ClightTSO, a concurrent extension of CompCert’s Clight in which the TSO-based memory model of x86 multiprocessors is exposed for high-performance code, and CompCertTSO, a formally verified compiler from ClightTSO to x86 assembly language, building on CompCert. CompCertTSO is verified in Coq: for any well-behaved and successfully compiled ClightTSO source program, any permitted observable behavior of the generated assembly code (if it does not run out of memory) is also possible in the source semantics. We also describe some verified fence-elimination optimizations, integrated into CompCertTSO.Keywords
Funding Information
- Inria
- Agence Nationale de la Recherche (ANR-06-SETI-010-02, ANR-11-JS02-011)
- Engineering and Physical Sciences Research Council (EP/F036345, EP/H005633, EP/K008528)
This publication has 43 references indexed in Scilit:
- A case for an SC-preserving compilerACM SIGPLAN Notices, 2011
- Relaxed-memory concurrency and verified compilationACM SIGPLAN Notices, 2011
- x86-TSOCommunications of the ACM, 2010
- Ott: Effective tool support for the working semanticistJournal of Functional Programming, 2010
- Formal verification of a realistic compilerCommunications of the ACM, 2009
- Hiding relaxed memory consistency with a compilerIEEE Transactions on Computers, 2001
- Forward and Backward SimulationsInformation and Computation, 1995
- The existence of refinement mappingsTheoretical Computer Science, 1991
- Efficient and correct execution of parallel programs that share memoryACM Transactions on Programming Languages and Systems, 1988
- Global optimization by suppression of partial redundanciesCommunications of the ACM, 1979