linearscan: Linear scan register allocator, formally verified in Coq
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
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
takes a list of basic blocks, and a functional characterization of those
blocks, and produces a new list, with register allocations applied to their
- 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'.
|Versions [RSS]||0.1.0.0, 0.2.0.0, 0.3.0.0, 0.3.0.1, 0.3.1.0, 0.4.0.0, 0.5.0.0, 0.5.1.0, 0.6.0.0, 0.7.0, 0.8.0, 0.9.0, 0.10.0, 0.10.1, 0.10.2, 0.11, 0.11.1, 1.0.0|
|Dependencies||base (>=4.7 && <5.0), containers, ghc-prim, mtl, transformers [details]|
|Revised||Revision 1 made by JohnWiegley at 2022-06-24T20:47:23Z|
|Source repo||head: git clone https://github.com/jwiegley/linearscan|
|Uploaded||by JohnWiegley at 2015-11-20T17:35:06Z|
|Reverse Dependencies||2 direct, 0 indirect [details]|
|Downloads||10464 total (41 in the last 30 days)|
|Rating||(no votes yet) [estimated by Bayesian average]|
|Status||Docs available [build log]
Last success reported on 2016-11-29 [all 3 reports]