[Haskell-cafe] ANN: linearscan, linearscan-hoopl 1.0.0
johnw at newartisans.com
Fri Nov 20 17:44:00 UTC 2015
linearscan is a linear scan register allocator, written in Coq, and
extracted to Haskell, as a library for Haskell programs that need to allocate
registers. It may also be used directly from Coq.
This project is the result of a year-long effort, funded by BAE Systems, to
explore the application of dependent-types and mathematical verification to a
typical engineering task. During the course of construction, several hundred
theorems about the code were proven -- although exhaustive coverage was not,
in the end, achievable given our time constraints. To remedy this, and as a
test of the extraction to Haskell, an optional runtime verifier was built to
certify the resulting allocations.
Coq 8.5b2 was used, as well as the ssreflect library created for that
version. linearscan further relies on another library, coq-haskell, that
I created to facilitate inter-operation between Haskell and Coq.
For those using Hoopl to represent program graphs, incorporating linearscan
is quite easy: provide an instance of NodeAlloc using the linearscan-hoopl
library. Examples of doing so are provided in the test suite for that library.
The allocation algorithm implemented by this library was first written in Java
by Hanspeter Mössenböck and Michael Pfeiffer, and later improved upon by
Christian Wimmer, whose master's thesis provided the specification for our
More information about the Haskell-Cafe