Thumbnail
Access Restriction
Subscribed

Author Evk, Jaroslav ♦ Vafeiadis, Viktor ♦ Zappa Nardelli, Francesco ♦ Jagannathan, Suresh ♦ Sewell, Peter
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©2013
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Relaxed memory models ♦ Semantics ♦ Verified compilation
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.
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2013-06-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 60
Issue Number 3
Page Count 50
Starting Page 1
Ending Page 50


Open content in new tab

   Open content in new tab
Source: ACM Digital Library