CompCertTSO: A verified compiler for relaxed-memory concurrency
Jaroslav Ševčík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell[doi] [Google Scholar] [DBLP] [Citeseer] [url]
J. ACM
60(3)
Association for Computing Machinery
New York, NY, USA
jun 2013
Note(s): verified compilers, weak memory, ISA specification, TSO, CompCert compiler
Association for Computing Machinery
New York, NY, USA
jun 2013
Note(s): verified compilers, weak memory, ISA specification, TSO, CompCert compiler