CompCertTSO swMATH ID: 8230 Software Authors: Ševčík, Jaroslav; Vafeiadis, Viktor; Zappa Nardelli, Francesco; Jagannathan, Suresh; Sewell, Peter Description: CompCertTSO: a verified compiler for relaxed-memory concurrency. 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. Homepage: http://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/ Keywords: relaxed memory models; semantics; verified compilation Related Software: Coq; CompCert; CompCertS; Paco; GCminor; CakeML; Isabelle/HOL; Flocq; Toolchain; Delphin; seL4; VeriML; Rtac; Mtac; Ynot; CDSChecker; Pilsner; MLton; Poly/ML; HOL Cited in: 12 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year CompCertTSO: a verified compiler for relaxed-memory concurrency. Zbl 1281.68072Ševčík, Jaroslav; Vafeiadis, Viktor; Zappa Nardelli, Francesco; Jagannathan, Suresh; Sewell, Peter 2013 all top 5 Cited by 31 Authors 3 Vafeiadis, Viktor 2 Besson, Frédéric 2 Blazy, Sandrine 2 Jagannathan, Suresh 2 Krebbers, Robbert 2 Pous, Damien 2 Wilke, Pierre 2 Zappa Nardelli, Francesco 1 Balabonski, Thibaut 1 Cachera, David 1 Chakraborty, Soham 1 Demange, Delphine 1 Dreyer, Derek R. 1 Fox, Anthony C. J. 1 Krishnaswami, Neelakantan R. 1 Kumar, Ramana 1 Lochbihler, Andreas 1 Morisset, Robin 1 Myreen, Magnus O. 1 Nanevski, Aleksandar 1 Norrish, Michael 1 Owens, Scott 1 Petri, Gustavo 1 Pichardie, David 1 Rot, Jurriaan 1 Ševčík, Jaroslav 1 Sewell, Peter 1 Tan, Yong Kiam 1 Vitek, Jan 1 Zakowski, Yannick 1 Ziliani, Beta Cited in 3 Serials 4 Journal of Automated Reasoning 2 Journal of Functional Programming 1 Journal of the ACM Cited in 5 Fields 12 Computer science (68-XX) 4 Mathematical logic and foundations (03-XX) 2 Order, lattices, ordered algebraic structures (06-XX) 1 General algebraic systems (08-XX) 1 Category theory; homological algebra (18-XX) Citations by Year