Skip to Main content Skip to Navigation
Conference papers

Relaxed-memory concurrency and verified compilation

Jaroslav Sevcik 1 Viktor Vafeiadis 2 Francesco Zappa Nardelli 3 Suresh Jagannathan 4 Peter Sewell 1
1 CAM - University of Cambridge [UK]
2 MPI-SWS - Max Planck Institute for Software Systems
3 Parkas - Parallélisme de Kahn Synchrone
DI-ENS - Département d'informatique de l'École normale supérieure, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
4 Purdue University [West Lafayette]
Abstract : In this paper, we consider 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. We define a concurrent relaxed-memory semantics for ClightTSO, an extension of CompCert's Clight in which the processor's memory model is exposed for high-performance code. We discuss a strategy for verifying compilation from ClightTSO to x86, which we validate with correctness proofs (building on CompCert) for the most interesting compiler phases.
Document type :
Conference papers
Complete list of metadata
https://hal.inria.fr/hal-00907801
Contributor : Francesco Zappa Nardelli <>
Submitted on : Thursday, November 21, 2013 - 5:41:50 PM
Last modification on : Thursday, July 1, 2021 - 5:58:08 PM

Identifiers

  • HAL Id : hal-00907801, version 1

Collections

CNRS | INRIA | ENS-PARIS | PSL

Citation

Jaroslav Sevcik, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell. Relaxed-memory concurrency and verified compilation. POPL - 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, Jan 2011, Austin, TX, United States. ⟨hal-00907801⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

200

 

Contact                    Legal Notice                    Personal Data