Verified compilation for shared-memory C
Author(s): Beringer, L; Stewart, G; Dockins, R; Appel, Andrew W.
DownloadTo refer to this page use:
http://arks.princeton.edu/ark:/88435/pr1n01pFull metadata record
| DC Field | Value | Language |
|---|---|---|
| dc.contributor.author | Beringer, L | - |
| dc.contributor.author | Stewart, G | - |
| dc.contributor.author | Dockins, R | - |
| dc.contributor.author | Appel, Andrew W. | - |
| dc.date.accessioned | 2016-10-17T14:13:57Z | - |
| dc.date.available | 2016-10-17T14:13:57Z | - |
| dc.date.issued | 2014-01-01 | en_US |
| dc.identifier.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 | en_US |
| dc.identifier.issn | 0302-9743 | - |
| dc.identifier.uri | http://arks.princeton.edu/ark:/88435/pr1n01p | - |
| dc.description.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. | en_US |
| dc.format.extent | 107 - 127 | en_US |
| dc.relation.ispartof | 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 | en_US |
| dc.relation.ispartofseries | Lecture Notes in Computer Science; | - |
| dc.rights | This is the author’s final manuscript. All rights reserved to author(s). | en_US |
| dc.title | Verified compilation for shared-memory C | en_US |
| dc.type | Conference Article | en_US |
| dc.identifier.doi | doi:10.1007/978-3-642-54833-8_7 | - |
| dc.identifier.eissn | 1611-3349 | - |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| AppelESOP2014.pdf | 641.87 kB | Adobe PDF | View/Download |
Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.