Wed Mar 3 19:50:37 CET 2010
Correctness and Machine Description
One of the major problems in the development of Staapl was the
correctness of its code generator and peephole optimizations. While
the rules by themselves are easy enough to prove, their large number
and the absence of a coverage test makes it possible for mistakes to
I've written before about a way that makes it possible to assure the
correctness of the code generation by adding redundant information
(semantics) to the machine language (i.e. a simulator).
I wonder if this can be used together with quickcheck. Since the
problem is the generation of the test cases, automatic that part might
be an interesting approach.
When trying this I got stuck on the description language for writing
down the semantics. Then I got off on a tangent to describe a
Essentially what is necessary is to represent each instruction as a
transition function, and perform automatic lifting such that sequences
of instructions can be translated to composed transition functions.
Once a sequence of machine instructions has a _functional_
representation (function + dependencies) it is straightforward to make
test cases and relate this concrete low-level operational semantics to
any higher level operational semantics.
The real problem: Staapl is not a language. It is a notation for a
macro assembler, and in its current form it is not well specified.
I've seen this problem before: thinking of the evolution of Staapl
on multiple targets as the evolution of a standard interface. I'm not
so sure this is actually workable. The problems I face simply
attempting to move to a more complex architecture (PIC24) makes me
wonder if it's not better to stick at the low level, or at least have
_multiple_ interface inbetween that can be reused, given constraints.
I.e. following Haskell typeclasses and OCaml modules, it makes sense
to reuse number systems (type classes). It might be more useful to
push Staapl in such a direction: organically abstract more