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.
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
For package maintainers and hackage trustees
Candidates
- No Candidates
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] |
License | BSD-3-Clause |
Author | John Wiegley |
Maintainer | johnw@newartisans.com |
Revised | Revision 1 made by JohnWiegley at 2022-06-24T20:47:23Z |
Category | Development |
Home page | http://github.com/jwiegley/linearscan |
Source repo | head: git clone https://github.com/jwiegley/linearscan |
Uploaded | by JohnWiegley at 2015-11-20T17:35:06Z |
Distributions | |
Reverse Dependencies | 2 direct, 0 indirect [details] |
Downloads | 11052 total (23 in the last 30 days) |
Rating | (no votes yet) [estimated by Bayesian average] |
Your Rating | |
Status | Docs available [build log] Last success reported on 2016-11-29 [all 3 reports] |