CompCertTSO A Verified Compiler for Relaxed-Memory Concurrency
CompCertTSO A Verified Compiler for Relaxed-Memory Concurrency
复制标题
CompCertTSO 经过验证的宽松内存并发编译器
DOI：
10.1145/2487241.2487248
复制
发表时间：
2013
影响因子：
2.5
通讯作者：
Ševcík J
中科院分区：
文献类型：
--
作者：
Ševcík J
在这篇文章中，我们考虑的语义设计和验证编译的类C语言的并行共享内存计算x86多处理器。这样一种语言的设计是由几个因素令人惊讶的微妙：硬件的松弛内存行为，编译器优化对并发代码的影响，支持高性能并发算法的需要，以及对合理简单的编程模型的期望。反过来，这种复杂性使得验证编译必不可少的和具有挑战性的。我们描述ClightTSO，并发扩展CompCert的Clight，其中基于TSO的x86多处理器的内存模型是暴露的高性能代码，和CompCertTSO，正式验证编译器从ClightTSO到x86汇编语言，CompCert的基础上。CompCertTSO在Coq中得到验证：对于任何行为良好且成功编译的ClightTSO源程序，生成的汇编代码的任何允许的可观察行为（如果它没有耗尽内存）也可能在源语义中。我们还描述了一些经过验证的围栏消除优化，集成到CompCertTSO。
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.