Certified implementation of a parametrized framework for concurrent garbage collectors
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
Coq
Haskell
.gitignore
README

README

Correctness-Preserving GC Transformations
=========================================

This directory contains implementation and (in the future)
formalization of the framework for correctness-preserving derivations
of concurrent garbage collectors by Vechev et al. [VYB06].

The structure of the project:

- ./Haskell -- a folder with the Haskell prototype of parametrised
  expose functions. Different dimensions are implemented as type
  classes with mutually-disjoint functions, specifying the
  corresponding partitions.

   
---- GCDerivation.hs -- this file contains implementation of the main
     GC machinery concerning parametrized instances of the explore
     function. The same file also contains definitions of all the
     dimension type classes.

---- ExampleXY.hs -- example files, corresponding to the case studies
     labelled as X.Y in the [VYB06] paper. The comments after the
     expressions describe the results obtained by evaluating them.

- ./Coq -- a Coq formalization of the collector's exposing functions
  and their correctness wrt. graph reachability

---- Heaps -- a library of partial heaps, developed by Aleks Nanevski
     (see http://software.imdea.org/fcsl for details).

---- Hgaphs.v -- a theory of object graphs, including facts about
     allocation/mutation.

---- Logs.v -- implementation of collector/mutator logs

---- Wavefronts.v -- A library for wavefronts

---- Apex.v -- implementation of the "apex" expose procedure

---- WavefrontDimension.v -- Parametrizing the expose over the
     wavefront dimension.


Building the project
====================

-- Haskell --

Run

make clean; make

from the folder "Haskell" to compile the project.

Individual example files can be loaded into the ghci REPL as follows

:load ExampleXY.hs

-- Coq --

Run 

make clean; make 

from the folder "Coq". This will build the necessary libraries and the
GC formalizaion.


References
==========

[VYB06] M. Vechev, E. Yahav, D. Bacon. Correctness-Preserving
Derivation of Concurrent Garbage Collection Algorithms. PLDI'06.