Verified compilation for shared-memory C

Author(s): Beringer, L; Stewart, G; Dockins, R; Appel, Andrew W.

Download

To refer to this page use: http://arks.princeton.edu/ark:/88435/pr1n01p

Abstract:	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. © 2014 Springer-Verlag.
Publication Date:	1-Jan-2014
Citation:	Beringer, L, Stewart, G, Dockins, R, Appel, AW. "Verified compilation for shared-memory C" Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 8410 LNCS, 107 - 127, doi:10.1007/978-3-642-54833-8_7
DOI:	doi:10.1007/978-3-642-54833-8_7
ISSN:	0302-9743
EISSN:	1611-3349
Pages:	107 - 127
Type of Material:	Conference Article
Series/Report no.:	Lecture Notes in Computer Science;
Journal/Proceeding Title:	23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014
Version:	This is the author’s final manuscript. All rights reserved to author(s).