Information Technology Reference
In-Depth Information
reset. (The initialization phase need not be formally captured for the purpose
of compiler verication.) In order to describe
Run
in a modular fashion we
introduce auxiliary processes
Step
and
Fetch
and for each Transputer instruction
instr
a process
E
0
(
instr
).
Step
models the behavior of a complete execution cycle,
Fetch
the instruction fetch phase and
E
0
(
instr
) the instruction specic part of
the execution cycle.
The basic property of
Run
is that it cyclically executes steps. This is captured
by the axiom
Run
=
Step
;
Run
:
(1)
Step
is characterized by the family of axioms (one for each Transputer instruction
instr
)
2
Step
f
CurFct
(
instr
)
g
;
Fetch
;
E
0
(
instr
)
;
(2)
def
=(
Byte
;
bitand
InstrCode
where
CurFct
(
instr
)
(
instr
). Intu-
itively,
CurFct
(
instr
) is a predicate that holds true if and only if the memory lo-
cation pointed to by the instruction pointer
IP
contains just the instruction code
of the instruction
instr
. The above property of
Step
means that
Step
behaves
like the sequential composition of the
Fetch
phase and the process
(
Mem
IP
)
$
F0
)=
E
0
(
instr
)if
activated in a state where
CurFct
(
instr
) holds.
Fetch
is completely described by
the axiom
Fetch
=
Oreg
;
IP
:=
Oreg
bitor
(
Byte
(
Mem
;
IP
)
bitand
$
0F
)
;
IP
+1
:
The eect of the single instructions is described by Z-like schemata in appendix
F.3 of [23]. (The fetch phase too is described by a schema called `InstrDecode'.)
The schema for the load constant instruction
ldc
, for example, which loads the
contents of the operand register
Oreg
to the evaluation stack, looks as follows
[23, Page 132]:
ldc
#4
load constant
Areg
0
=Oreg
0
Breg
0
= Areg
Creg
0
= Breg
Oreg
0
=0
Iptr
0
=
NextInst
Primed names represent the values of the corresponding register after execution
and unprimed names the values before.
0
stands for the operand register's
contents after the fetch phase. In our framework the eect of
ldc
is captured by
a renement axiom about
Oreg
E
0
(
ldc
). As we are using an imperative programming
notation we need not use primed and superscripted variables for distinguishing
2
For a predicate
,the
assertion fg
is a process that terminates immediately without
state change if
holds, and behaves chaotically, i.e. is completely unconstrained
otherwise. (Formally,
fg
is the predicate transformer dened by
fg
(
)=
^
.)
As a consequence, (2) constrains { for a given instruction
instr
{ the behavior of
Step
only for initial states in which
CurFct
(
instr
)holds.
Search WWH ::
Custom Search