TY - GEN
T1 - Verified compilation for shared-memory C
AU - Beringer, Lennart
AU - Stewart, Gordon
AU - Dockins, Robert
AU - Appel, Andrew W.
PY - 2014
Y1 - 2014
N2 - We present a new architecture for specifying and proving optimizing compilers in the presence of shared-memory interactions such as buffer-based system calls, shared-memory concurrency, and separate compilation. The architecture, which is implemented in the context of CompCert, includes a novel interaction-oriented model for C-like languages, and a new proof technique, called logical simulation relations, for compositionally proving compiler correctness with respect to this interaction model. We apply our techniques to CompCert's primary memory-reorganizing compilation phase, Cminorgen. Our results are formalized in Coq, building on the recently released CompCert 2.0.
AB - We present a new architecture for specifying and proving optimizing compilers in the presence of shared-memory interactions such as buffer-based system calls, shared-memory concurrency, and separate compilation. The architecture, which is implemented in the context of CompCert, includes a novel interaction-oriented model for C-like languages, and a new proof technique, called logical simulation relations, for compositionally proving compiler correctness with respect to this interaction model. We apply our techniques to CompCert's primary memory-reorganizing compilation phase, Cminorgen. Our results are formalized in Coq, building on the recently released CompCert 2.0.
UR - http://www.scopus.com/inward/record.url?scp=84900563611&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84900563611&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-54833-8_7
DO - 10.1007/978-3-642-54833-8_7
M3 - Conference contribution
AN - SCOPUS:84900563611
SN - 9783642548321
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 107
EP - 127
BT - Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings
PB - Springer Verlag
T2 - 23rd European Symposium on Programming, ESOP 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014
Y2 - 5 April 2014 through 13 April 2014
ER -