GCTransformations/README at master · UCL-PPLV/GCTransformations · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
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.