Changed description
from
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.
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. In the absence of some complete coverage, this version
of the library provides an optional, runtime verifier to confirm
expectations of correctness, since it is easier to prove the validity of
generated data, than of how it was generated.
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.
to 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.