Information Technology Reference
In-Depth Information
2.3
A Hierarchy of Views
The base model of the Transputer is on a rather low level of abstraction. It has
not even an explicit notion of an executed machine program but instructions are
taken from the memory. In principle it is possible to use this model directly in a
correctness predicate relating machine code with source programs but this leads
to a complicated denition and to complicated proofs. Therefore, we stepwise
derive more abstract views to the Transputer's behavior. These views are suc-
cessively concerned with the following topics, which in this way can be treated
in isolation:
{ symbolic representation of the control point, which results in a treatment of
the executed machine program as a separate entity;
{ word-size operands for direct functions;
{ convenient access to the workspace;
{ symbolic variables instead of workspace addresses; the mapping of these
variables to the workspace is described by a dictionary
;
{ hiding of registers.
Each abstraction level comprises a collection of processes. The abstractions
are performed by dening the collection of processes for the more abstract view in
terms of the collection for the more concrete one. Afterwards suciently strong
theorems are established that allow one to reason with the abstract family of
processes alone, without referring to the concrete family. This is essential for
meeting the objective of abstraction, viz. to increase tractability.
Table 1 shows the drastic reduction of the complexity of the terms describing
the instruction ldl (load local) at the various abstraction levels. As mentioned,
the assertion
present at the lower abstraction levels
make the inequalities applicable only if the referenced address is valid. From
Level 3 onwards this is ensured by a global assumption about the storage allo-
cated for the workspace. The models in the hierarchy are consistent by construc-
tion, i.e. by denition and calculation.
In the following we discuss the rst two abstractions in more detail and sketch
the other abstractions.
f Index
( Wptr ; Oreg )
2 Addr g
Symbolic Representation of Programs. It is quite natural to think of a
machine program as a separate entity consisting of a sequence of instructions.
The point of execution, that is represented on the machine by the instruction
pointer's contents, can be modeled by a distinguished position in that instruction
sequence. More elegantly we can use a pair of instruction sequences (
a;b
), where
a
stands for the part of the machine program before the distinguished position
and
b
for the part thereafter, i.e. the complete machine program is
a b
and the
next instruction to be executed is the rst instruction of
b
. Progress of execution
can be elegantly expressed by partitioning the sequence
dierently.
Formalizing this idea we dene, based on Run , a family of processes
a b
I 1 (
a;b
)
(parameterized by the pair of instruction sequences
a;b
).
I 1 (
a;b
) describes the
 
Search WWH ::




Custom Search