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:
Full metadata record
DC FieldValueLanguage
dc.contributor.authorBeringer, L-
dc.contributor.authorStewart, G-
dc.contributor.authorDockins, R-
dc.contributor.authorAppel, Andrew W.-
dc.identifier.citationBeringer, 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_7en_US
dc.description.abstractWe 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.en_US
dc.format.extent107 - 127en_US
dc.relation.ispartof23rd 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, 2014en_US
dc.relation.ispartofseriesLecture Notes in Computer Science;-
dc.rightsThis is the author’s final manuscript. All rights reserved to author(s).en_US
dc.titleVerified compilation for shared-memory Cen_US
dc.typeConference Articleen_US

Files in This Item:
File Description SizeFormat 
AppelESOP2014.pdf641.87 kBAdobe PDFView/Download

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