A certified framework for compiling and executing garbage-collected languages

A certified framework for compiling and executing garbage-collected languages,10.1145/1863543.1863584,Andrew McCreight,Tim Chevalier,Andrew P. Tolmach

A certified framework for compiling and executing garbage-collected languages   (Citations: 3)
BibTex | RIS | RefWorks Download
We describe the design, implementation, and use of a machine- certified framework for correct compilation and execution of pro- grams in garbage-collected languages. Our framework extends Leroy's Coq-certified Compcert compiler and Cminor intermediate language. We add: (i) a new intermediate language, GCminor, that includes primitives for allocating memory in a garbage-collected heap and for specifying GC roots; (ii) a precise, low-level specifica- tion for a Cminor library for garbage collection; and (iii) a proven semantics-preserving translation from GCminor to Cminor plus the GC library. GCminor neatly encapsulates the interface between mutator and collector code, while remaining simple and flexible enough to be used with a wide variety of source languages and collector styles. Front ends targeting GCminor can be implemented using any compiler technology and any desired degree of verifi- cation, including full semantics preservation, type preservation, or informal trust. As an example application of our framework, we describe a compiler for Haskell that translates the Glasgow Haskell Com- piler's Core intermediate language to GCminor. To support a simple but useful memory safety argument for this compiler, the front end uses a novel combination of type preservation and runtime checks, which is of independent interest.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...Dargaye [13] has adapted the Compcert framework to a compiler for a pure mini-ML language, and McCreight et al. [19] have extended it to support interfacing with a garbage collector...
    • ...They prove in Coq that various collectors implement this interface, and that various mutator programs respect it. In more recent work, Mc-Creight et al. [19] extend Leroy’s Compcert compiler [18] with support for garbage collection, by building the mutator-collector interface into the design of a new intermediate language, GCminor...

    Chung-Kil Huret al. A kripke logical relation between ML and assembly

    • ...Recently, Leroy’s Coq-verified C compiler [14], which targets PowerPC, ARM and 32-bit x86 assembly, has been extended with new front-ends that makes it compile MiniML [4] and a garbage-collected source language [16]...
    • ...Our runtime uses a verified copying garbage collector similar to the sample collector in McCreight et al. [16], but less than 10% of our proof scripts are directly concerned with verification of our garbage collector and interfacing with it; our approach to this is unchanged from our previous paper [18]...

    Magnus O. Myreenet al. A Verified Runtime for a Verified Theorem Prover

Sort by: