Information Technology Reference
In-Depth Information
2.6
Time Shifts
In this section we discuss the additional ingredients of the compiler correctness
proof for the timed language.
First of all, the imperative meta-language is provided with a timed interpreta-
tion and extended by delays
.
This is done in such a way that all constructs except delays execute in zero time.
The bound operator constrains the time consumed by the enclosed process
d
and time bounds
j P jd
,where
d2
[f1g
0
P
(not counting the time that
P
stalls waiting for communication partners to be-
come ready);
time units without state change. For
simplicity, we use the duration of one execution cycle of the target processor as
the unit of time in this section.
We add delays to the axioms describing the eect of instructions. For exam-
ple, the timed version of Axiom (3) looks as follows:
d
executes in at most
d
E 0 ( ldc )
1; A
;
;
;
;
Oreg := Oreg
;
;
;
IP +1
;
0
:
B
C
IP
A
B
This expresses that ldc uses at most one execution cycle for execution. The
timing information is taken from the tables in [23, Appendix D].
A particularly interesting aspect of the code generator proof is that it justies
the idealization of instantaneous execution for all internal constructs of the timed
source language, i.e. all constructs except input/output statements. Of course,
the code implementing, say, an assignment needs time to execute. The idea is to
shift such excess time of code implementing internal activity to a sequentially
successive process that is compiled to a machine program needing less time
for execution than allowed by the source [15]. This can be accomplished by
adding two parameters
L
and
R
to the correctness predicate for statements,
where
L
states the excess time of the sequential predecessor that is absorbed
and
states the excess time that is handed over to the sequential successor for
absorption. A third new parameter
R
is introduced that asserts a time bound for
the source statement. This leads to the following denition: a machine program
E
m
implements source statement stat , absorbing excess time
L
from its sequential
R
predecessor, exporting excess time
to its sequential successor, under time
E
a
b
bound
, i for all instruction sequences
and
5 (
5 (
L
;
I
a;m b
)
j MS
( stat )
jE
;
R
;
I
am;b
)
:
CS 0 (
For brevity, we denote this implementation property by
m;
stat
;;L;R;E
).
Let us now have a look at some example translation theorems.
The theorem that allows to translate time bounds in the source program
looks as follows:
CS 0 (
Theorem 4 (Translation of time bounds). Suppose
m;
stat
;;L;R;E
) .
CS 0 (
If
E t
then
m;
upperbound (
P;t
)
;;L;R;E
) .
Thus, a compiler encountering an upper bound operator in the source statement
needs only check whether the required time bound is more liberal than the one
asserted upon the code generated for the enclosed statement. If it is, then no
 
Search WWH ::




Custom Search