Fri Apr 3 13:02:23 CEST 2009
Before going anywhere, it needs to be defined what a "machine" is. It
is important that the description of the machine (data structures and
interpreter) is written in such a way that it can be easily
specialized/compiled (to C code).
One important question: why use bottom-up operational semantics? Why
not define an intermediate semantics (i.e. Forth)? The answer is:
this is about (specializing) compiler correctness. The high level
semantics themselves are trivial and could be used to verify the
bottom-up semantics, but this requires complete simulation of the true
A machine is:
* a collection of registers / memory array
* MIMO functions
Note that the registers are _not_ SA like in [LLVM], since we're
trying to model exact machine semantics for simulation, and are not
trying to map a generic language to a register machine.
Should I take a hint from this? Should the machine model be
completely functional so code can be transformed into data flow
networks? Or can I write a model using assignments only to avoid
overspecifying operations (declaring outputs), then use dataflow
analysis to transform it to a different representation? I probably
need to take a better look at Chaper 8 in [ACDI]. A lot of intuition
is still missing..
The bottom line however: machine description needs both:
- assembly (compilation)
- simulation (evaluation / compile time computation / type
The description of the semantics should be compilable as fast and
standalone code (read: C).
I can do this only (practically) for simple machines, or subsets of