Compilation and Synthesis for Real-Time Embedded Controllers - Correct System Design: Recent Insights and Advances - page 250

The exposition up to now is of course oversimplied. Firstly, the model of
the instruction's eect is too abstract. For example, the Transputer instructions
reference memory locations basically, not variable identiers as we assumed in
the description of stl (

), and a machine program basically is not a separate
entity but the executed instructions are taken from the memory. Secondly, a
number of unformalized assumptions have been made in the surrounding text.
An idealized abstract model of the target processor simplies the compiler
verication. But if considerations are based on such a model alone there is a
severe danger of unsoundness because the postulated model might fail to provide
a safe abstraction of the processor's actual behavior. To ban this danger we
interface directly to the Transputer's documentation by starting from a semi-
formal model of its execution cycle provided by INMOS, the manufacturer of
the Transputer, in [23]. A direct employment of this model in a compiler proof,
however, would result in very long and tedious calculations which would seriously
aect credibility of the proofs. How can we combine simplicity and conciseness
of proofs with realistic modeling of the processor?
The idea is to derive a hierarchy of mutually consistent, increasingly abstract
views to the Transputer's behavior, starting from bit-code level up to assembly
levels with symbolic addressing. In each of the abstraction steps one particular
phenomenon can be tackled in isolation. Afterwards we can choose for each proof
task the model that allows the simplest proof or even mix reasoning at dierent
abstraction levels without risking inconsistencies or unsoundness.
In the remaining parts of this section we describe the Transputer base model,
the derived more abstract models, and the technique by which the abstraction is
performed. Then we show how this hierarchy can advantageously be employed in
the translation correctness proof for an imperative (un-timed) source language.
Afterwards we indicate the generalization to a timed language. Due to lack
of space we cannot present all formal details but invite the reader to enjoy
the presentation with an informal understanding. A complete treatment can be
found in the monograph [37].

x

2.2 Transputer Base Model

Appendix F of the Transputer Instruction Manual [23] contains a semi-formal
model of the Transputer's behavior. Essentially it describes the Transputer as
a state machine that communicates via four bi-directional synchronous chan-
nels called links , and works on a state consisting of three accumulators A , B
and C (used as a small stack by most instructions), an operand register Oreg ,
a workspace pointer Wptr , an error flag EFlag , an instruction pointer IP ,and
an addressable memory Mem . We reformulate this model using the notation of
the imperative meta-language mentioned above. The state components are rep-
resented by likewise named variables of appropriate type and the links by four
input channels In 0 ;:::; In 3 and four output channels Out 0 ;:::; Out 3 .
We introduce a process Run that is constrained by axioms in the form of
renement formulas. Run models the complete behavior of the running phase
which is entered by the Transputer after the initialization phase that follows a