Skip to main content

Verified compilation for shared-memory C

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

To refer to this page use:
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).

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.