linearscan: Linear scan register allocator, formally verified in Coq

The linearscan library is an implementation -- in Coq, extracted to Haskell -- of a register allocation algorithm developed by Christian Wimmer. It is described in detail in his Masters thesis, which can be found at http://www.christianwimmer.at/Publications/Wimmer04a/Wimmer04a.pdf. A Java implementation of this same algorithm, by that author, is used in Oracle's Graal project. It has also been implemented in C++ by Mozilla.

This version of the algorithm was written and verified in Coq, containing over 231 proved lemmas, at over 10K LOC. It was funded as a research project by BAE Systems (http://www.baesystems.com), to be used in an in-house compiler written in Haskell.

In order for the Coq code to be usable from Haskell, it is first extracted from Coq as a Haskell library, during which many of Coq's fundamental types are mapped directly onto counterparts in the Haskell Prelude.

This library's sole entry point is the function LinearScan.allocate, which takes a list of basic blocks, and a functional characterization of those blocks, and produces a new list, with register allocations applied to their component operations.

Modules

[Index]

Downloads

• linearscan-1.0.0.tar.gz [browse] (Cabal source package)
• Package description (revised from the package)

Note: This package has metadata revisions in the cabal description newer than included in the tarball. To unpack the package including the revisions, use 'cabal get'.

Maintainer's Corner

Package maintainers

• JohnWiegley

For package maintainers and hackage trustees

• edit package information

Candidates

• No Candidates