CertiGC

A Verified Software Unit that provides a formally verified generational garbage collector.

Implemented in C, modeled in Coq, and proven correct using the Verified Software Toolchain and CertiGraph.

Compatible with CompCert.

Verification status

Specifications are proven correct for the following targets:

• x86_64-linux
• x86_32-linux

Proofs are checked by our CI infrastructure.

Contributors

• Aquinas Hobor
• Shengyi Wang
• Anshuman Mohan
• Tim Carstens

Install the dependencies

Clone and install CertiGraph using the included opam files.

Packages

• coq-vsu-gc-src - C source code
• coq-vsu-gc-vst - VST model, spec, and proof (x86_64-linux)
• coq-vsu-gc-vst-32 - VST model, spec, and proof (x86_32-linux)
• coq-vsu-gc - All of the above

Installing

Installation is performed by opam with help by coq-vsu.

$ opam pin -n -y .
$ opam install --working-dir ./coq-vsu-gc.opam

Using the C library

The C library is installed to the path given by vsu -I. For example:

$ tree `vsu -I`
/home/tcarstens/.opam/coq-8.14/lib/coq-vsu/lib/include
└── coq-vsu-gc
    ├── config.h
    ├── gc.h
    ├── mem.h
    └── src
        └── gc.c

2 directories, 4 files
$

Building without opam

The general pattern looks like this:

$ make [verydeepclean|deepclean|clean]
$ make BITSIZE={opam|64|32} [all|_CoqProject|clightgen|theories]

BITSIZE determines which compcert target to use. If unspecified, the default value is opam:

• opam and 64 both use x86_64-linux
• 32 uses x86_32-linux

Example: x86_64-linux

$ make verydeepclean ; make

Example: x86_32-linux

$ make verydeepclean ; make BITSIZE=32