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.

This version of the algorithm was written and verified in Coq, containing over 130 proved lemmas, at over 5K 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. Thus, it should be within the performance range of an equivalent implementation written directly in Haskell.

Note that not every conceivable property of this library has been proven. For some of the lower layers this is true, because the algebraic constraints on these components could be exhaustively described in the context of their use. However, higher-level components represent a great variety of use cases, and not every one of these cases has been proven correct. This represents an ongoing effort, with the hope that proofs will entirely replace the necessity for ad hoc unit testing, and that at some point we can know that any allocation produced by this library must either fail, or be mathematically sound.

This library's sole entry point is the LinearScan.allocate function, which takes a list of information about basic blocks to an equivalent list, with annotations indicating allocation choices.

Modules

[Index]

Downloads

• linearscan-0.3.1.0.tar.gz [browse] (Cabal source package)
• Package description (as included in the package)

Maintainer's Corner

Package maintainers

• JohnWiegley

For package maintainers and hackage trustees

• edit package information

Candidates

• No Candidates