Section: New Results

Relaxed-Memory Concurrency and Verified Compilation

Participants : Jaroslav Ševčík [U. of Cambridge] , Peter Sewell [U. of Cambridge] , Jagannathan Suresh [U. of Cambridge] , Viktor Vafeiadis [U. of Cambridge] , Francesco Zappa Nardelli.

We studied the semantic design and verified compilation of a C-like programming language for concurrent shared-memory computation above x86 multiprocessors. The design of such a language is made surprisingly subtle by several factors: the relaxed-memory behaviour of the hardware, the effects of compiler optimisation 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 (or verifying) compilation both essential and challenging.

This project started in 2010, when we defined a concurrent relaxed-memory semantics for ClightTSO, an extension of CompCert's Clight in which the processor memory model is exposed for high-performance code, and, building on CompCert, we implemented a certifying compiler from ClightTSO to x86, and proved in Coq several compilation phases. A paper describing our approach has been accepted in POPL [29] 2011.

During 2011 we completed this project by developping correctness proofs for all the compilation phases, and made a public distribution of the compiler, available from http://www.cl.cam.ac.uk/~pes20/CompCertTSO .

In 2011 Zappa Nardelli and Vafeiadis investigated the soundness of fence elimination optimisations for x86TSO. They implemented and proved correct two optimisations that remove redundant fence instructions as compiler passes over RTL in CompCertTSO. Despite an apparent simplicity, these optimisations generate almost optimal code for several standard concurrent algorithms (CompCertTSO does not implement escape analysis, which would enhance the effectiveness of the optimisations), and since they only perform data-flow analysis over the code of each thread (without analysing the full-system thread interactions) they do not suffer form the finite-state and finite control limitation of other approaches. The proof of correctness of one optimisation was challenging has required some for prophecy variable simulation. This work has been published in SAS 2011 [28] and the code is part of CompCertTSO.

A journal version, describing the correctness proof of all the phases of CompCertTSO (including the fence eliminations) as been submitted to the Journal of the ACM [35] .