Academic
Publications
Relaxed-memory concurrency and verified compilation

Relaxed-memory concurrency and verified compilation,10.1145/1925844.1926393,Sigplan Notices,Jaroslav Ŝevčik,Viktor Vafeiadis,Francesco Zappa Nardelli,

Relaxed-memory concurrency and verified compilation   (Citations: 1)
BibTex | RIS | RefWorks Download
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.
Journal: Sigplan Notices - SIGPLAN , pp. 43-54, 2011
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...This is often the case when modelling key computational infrastructure: network protocols, programming languages, multiprocessors, and so on. For example, we have worked on TCP [4,13], Optical Networking [3], Java Module Systems [18], the semantics of an OCaml fragment [11], concurrency for C and C++ [2,5,16], and the semantics of x86,...
    • ...with various colleagues we have built hand-crafted symbolic evaluators within HOL4 [3,4,13,15], interpreters from code extracted from Coq [16], and memory model exploration tools from code generated from Isabelle/HOL [2]...

    Scott Owenset al. Lem: A Lightweight Tool for Heavyweight Semantics

Sort by: