Verified compilation for shared-memory C

Lennart Beringer, Gordon Stewart, Robert Dockins, Andrew W. Appel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

14 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationProgramming 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
PublisherSpringer Verlag
Pages107-127
Number of pages21
ISBN (Print)9783642548321
DOIs
StatePublished - Jan 1 2014
Event23rd European Symposium on Programming, ESOP 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014 - Grenoble, France
Duration: Apr 5 2014Apr 13 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8410 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other23rd European Symposium on Programming, ESOP 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014
CountryFrance
CityGrenoble
Period4/5/144/13/14

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Verified compilation for shared-memory C'. Together they form a unique fingerprint.

  • Cite this

    Beringer, L., Stewart, G., Dockins, R., & Appel, A. W. (2014). Verified compilation for shared-memory C. In 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 (pp. 107-127). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8410 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-642-54833-8_7