BIB-VERSION:: CS-TR-v2.0
ID:: CORNELLCS//TR93-1333
ENTRY:: 1994-06-28
ORGANIZATION:: Cornell University, Computer Science Department
LANGUAGE:: English
NOTES:: Replaces 91-1238
END:: CORNELLCS//TR93-1333
BODY::
Putting Time into Proof Outlines*
Fred B. Schneider**
Bard Bloom*
Keith Marzullo****
TR 93-1333
March 1993
Department of Computer Science
Cornell University
Ithaca, NY 14853-7501
*A preliminary version of this work appeared in Real-time: Theory and Practice,
Proceedings of REX workshop, June 1991, Springer-Verlag Lecture Notes in
Computer Science, volume 600.
**Supported in part by the Office of Naval Research under contract NOOOl 4-91 -J-
1219, the National Science Foundation under Grant No. CCR-8701 103, DARPA/NSF
Grant No. CCR-9014363, and a grant from IBM Endicott Programming Laboratory.
***Supported in part by NSF grant CCR-9003441.
****Supported in part by Defense Advanced Research Projects Agency (DoD) under
NASA Ames grant number NAG 2-593 and by grants from IBM and Siemens.
Putting Time into Proof Outlines*
Fred B. Schneidert			Bard Bloom ?
Cornell University			Cornell University
fbs?cs . cornell. edu			bardCcs . cornell . edu
March 10, 1993
Abstract
Keith Marzullo 
Cornell University
marzulloQcs . cornell. edu
A logic for reasoning about timing properties of concurrent programs is presented. The logic
is based on Hoare-style proof outlines and can handle maximal parallelism as well as certain
resourceconstrained execution environments. The correctness proof for a mutual exclusion
protocol that uses execution timings in a subtle way illustrates the logic in action. A soundness
proof using structural operational semantics is outlined in the appendix.
Key words: concurrent program verification, timing properties, safety properties, real-time
programming, real-time actions, proof outlines.
1 Introduction
A safety property [9j of a program asserts that some proscribed "bad thing" does not occur during
execution. To prove that a program satisfies a safety property, one typically employs an invariant, a
characterization of current (and possibly past) program states that is not invalidated by execution.
If an invariant 1 holds in the initial state of the program and 1 ? Q is valid for some Q, then
?Q cannot occur during execution. Thus, to establish that a program satisfies the safety property
asserting that ?Q does not occur, it suffices to find such an invariant I.
Timing properties are safety properties where the "bad thing" involves the time and program
state at the instants that various specified control points in a program become active.1 Timing
properties can concern externally visible events, like inputs and outputs, as well as events and data
that are internal to a program, like the value of a variable or the time that a particular command
starts or finishes. For example, in process control applications, the elapsed time between a stimulus
and response may have to be bounded. This is a timing property where the "bad thing" is defined
in terms of the time that elapses after one control point becomes active until some other control
point does. Timing properties concerning internal events are useful in reasoning about ordinary
A preliminary version of this work appeared in Real-time: Theor? and Practice, Proceedings of REX workshop,
June 1991, Springer-Verlag Lecture Notes in Computer Science, volume 600.
t5upported in part by the Office of Naval Research under contract N00014-91-J-1219, the National Science Foun-
dation under Grant No. CCR-8701103, DARPA/NSF Grant No. CCR-9014363, and a grant from IBM Endicott
Programming Laboratory.
`Supported in part by NSF grant CCR-9003441.
?Supported in part by Defense Advanced Research Projects Agency (DoD) under NASA Ames grant number NAG
2-593, and by grants from IBM and Siemens.
1Informally, the active control points at any instant are determined by the values of the program counters at that
instant; See [15j for a more formal definition.
concurrent programs that exploit knowledge of command execution times to coordinate processes.
One such protocol--Hfor mutual exclusion--His given in section 4.
Because timing properties are safety properties, the invariant-based method outlined above for
reasoning about safety properties can be used to reason about timing properties. This means that
a programming logic L to verify (ordinary) safety properties can form the basis for a logic L' to
verify timing properties. It suffices that in L' we are able to:
(a) specify ill I and Q information about the times at which events of interest occur and
(b) establish that program execution does not invalidate such an I.
Point (a) means that in defining L', the language of L might have to be extended so that it becomes
more expressive. Point (b) means that the inferencing apparatus of L might have to be refined
so that I can be proved an invariant for a program whose semantics includes information about
execution timings.
A logic for timing properties will, of course, depend on the execution model for programs. Like
[14], we consider two kinds of actions, ordinary actions, which can take any amount of time to
execute, and rea1-time actions, which have constant upper and lower bounds on their execution
time. Real-time actions allow the modelling of schedulers typically found when multiprogramming
is employed to implement processes.
This paper describes extensions to a logic of proof outlines [15] to enable verification of timing
properties for concurrent programs. The approach taken is the one just outlined: we start with
a logic for proving ordinary safety properties, augment the language according to (a) and refine
the inference rules according to (b). The presentation is organized as follows. In Section 2 we
describe Proof Outline Logic for non-real-time programs. Then, in Section 3, we describe additional
mechanisms needed to handle real time. In particular, we describe changes that must be made to
the Rule of Consequence and to the definition of non-interference. In Section 4, we illustrate the
use of our logic on a mutual exclusion protocol. Section 5 contains discussion of related topics.
An appendix summarizes a Plotkin-style [13] structural operational semantics and soundness
proof. The full details of the soundness proof will appear in [2]. Our proof builds a natural model,
similar to models built by other researchers in the theory of concurrent programming languages[6,
18, 1, 13]. This method of construction argues for the reasonability of the logic and language as
well as proving its soundness, in much the same way that, for example, having the integers as a
model of an arithmetic system, or the Scott models for a A-calculus, give more plausibility than a
term model does.
2 Ordinary Proof Outline Logic
In order to reason about a program, we must be able to characterize sets of program states and
reason about them. First-order predicate logic is an obvious choice for this task, and we employ
the usual correspondence between the formulas of the logic and the programming language of
interest--Heach variable and expression of the programming language is made a term of the logic
and each Boolean expression of the programming language is made a predicate of the logic. It wili
be convenient to assume that predicates and terms are always defined, although the value of a term
may be unspecified in some states. For example, we will `?sume that the term x/y has a value
whatever value y has, but that y x (x/y) need not equal .?. when y is 0 because the value of x/y is
2
unspecified in such states.2
Predicates and function symbols for the programming language's data types provide a way to
express facts about program variables and expressions. Type declarations in the program induce
axioms concerning the values that may be assumed by the variables they declare. For simplicity,
we take these as given.
The state of a program also includes information that tells what atomic actions might be
executed next. For representing this control information, we fix some predicate symbols, called
control predicates, and give axioms to ensure that, as execution proceeds, changes in the values of
the control predicates correspond to changes in program counters. (An alternative representation
would have been to define a "program counter" variable and a data type for the values it can
assume.)
2.1 Control Predicates
A program is a structured collection of labelled commands, although we omit labels in program
texts unless they are needed. Each command comprises one or more atomic actions. The defining
characteristic of an atomic action is that its execution is performed as a single indivisible state
transformation. The control points of a program are defined by its atomic actions. Each atomic
action has distinct entry and exit control points. For example, the atomic action that implements
skip has a single entry control point and a single exit control point; the test for an if has one entry
control point and multiple exit control points, one for each alternative. Execution of an atomic
action a can occur only when an entry control point for a is active. Among other things, execution
causes that active entry control point to become inactive and an exit control point of a to become
active.
For each command or atomic action S, we define the following control predicates:
at(S): an entry control point for 5 is active.
after(S): an exit control point from 5 is active.
in(S): at(S') holds for some atomic action comprising 5.
The various commands of a programming language give rise to a set of axioms relating these
control predicates. These axioms formalize how the control predicates for a command or atomic
action 5 relate to the control predicates for constructs comprising 5 and constructs containing 5,
based on the control flow defined by 5. For our programming language these axioms are given in
Figure 1. We use GEvalif(S) there to denote the guard evaluation action for an if with label 5 and
GEval?o(S) to denote the guard evaluation action for a do with label 5. Equality of Boolean values
is logical equivalence. And, we write i?eP2e... ?P" to denote that exactly one of P1 through Pn
holds.
Our programming language is based on guarded commands [3j. Sequencing is written without
the traditional semicolon separator.3 The guard evaluation of the if command atomically evaluates
all its tests at once and selects a branch for which the test is true; if none are true, then it will block
until some test is made true by another process. A do ????mmand atomically evaluates its tests,
selects a branch with a true test, and repeats; if none are true, then it exits. A cobegin command
2More formally, we admit any interpretation in which aib is interpreted as a divided by b when b $ 0, and has
arbitrary values otherwise.
3We shall later see that this avoids a problem. A semicolon separ :)r would have to occupy the same position as
an assertion in the standard textual representation of the proof outI;????.
3
starts all of its component processes simultaneously, executing them concurrently. When they all
finish, the cobegin finishes as well.
Construct
a atomic
Axioms
5 : SlS2
s -;
ifB1?S1.?			at(S)
[IBj?Sj?			afler(S)
II Bn?S?			afier(GEvaljf(S))
fi			in(s)
?(at(a) A afler(a))
in(a)			=			at(a)
at(S)			=			at(S17
after(S)			=			after(S2)
after(S1)			=			at(S2)
in(S)			=			in(S1)?in(S2)
at(S) = (at(S1) A . . A at(S?))
after(S) = (after(S1) A ... A after(S?))
at(GEval1?(S))
(after(S1)eafter(S2)?... ?after(S?))
(at(S1)?at(S2)?... eat(S?))
ifl(GEValjf(S)) e in(S1) e.
e ifl(Sn)
5:
(1oB1?S1			.			at(GEval?c(S))
II Bj?Sj??			after(GEvaI<j0(S))
llBn?Sn			in(S)
od			at(S)
(after(GEval?0(S)) v V1%1 after(S?))
(at(S)eafter(S1)eafter(S2)?... ?aJter(S?))
(at(S1)eat(S2)?... ?at(Sn)?after(S))
in(GEvaI?0(S)) e in(S1) .... ? in(Sn)
at(GEvaI?0(S))
(after(Si) ... . ? after(S?) ? after(GEval?0(S)))
5:
cobegin
Siff???flSn
coend
Figure 1: Control Predicate Axioms
2.2 Syntax and Meaning of Proof Outlines
A proof outline PO(S) for a program or atomic action 5 is a mapping from the control predicates
of 5 to assertions. Each assertion is a Predicate Logic formula in which
o+ the free variables are program variables (typeset in italics) or rigid variables, (typeset in
uppercase roman), and
o+ the predicate symbols are control predicates or the predicates of the programming language's
expression language.
Assertions in which all terms are constructed from program ??iables, rigid variables, and predicates
involving those variables are called primitive assertions.
If T is a subprogram of 5 and some PO(S) is fixed, then we write pre(T) (resp. post(T)) for the
assertion(s) that PO(S) associates with at(T) (resp. a?c r( T)); these are called the precondition
and postcondition of T. For the proof outline in Figure 2, this correspondence is summarized in
Figure 3. In it, x is a program variable and X is a rigid variable. All assertions except pre(S) and
post(S) are primitive.
Proof outlines are generally represented as texts cont.?ining the program 5 and an assertion in
braces before and after every subprogram of 5. For our pio?ramming language, this will associate
4
= X A at(S))
5: if x >0 ??x =XAx >0)
: skip
= XAx >0)
II x<0??x=XAx<0)
S2 : x := --Hx
f--Hx = X A --Hx < 0)
fi
= X A after(S))
Figure 2: Computing lxi
at least one assertion with every control predicate of a program. Multiple control predicates may
be mapped to the same assertion, as illustrated by the proof outline
fP)x:=1 (Q)y:=2fR).
(1)
Here, the entry control point for program x := 1 y := 2, and the entry control point for x := 1 map
to the same assertion, P. This is reasonable, because at("x := 1 y := 2") and at("x := 1") are
equivalent; if one control point is active, so will be the other.
Finally, for a proof outline PO(S), we write pre(PO(S)) to denote pre(S), post(PO(S)) to
denote post(S), and use a triple ?P) PO(S) ?Q) to specify the proof outline in which pre(S) is P,
post(S) is Q, and all other pre- and postconditions are the same as in PO(S).
Validity of Proof Outlines
Assertion Assertion Text
pre(S) x = X A at(S)
post(S) x = X A after(S)
pre(51) x=XAx>0
post(S1) x=XAx>0
pre(52) x = X A x <0
post(S2) --Hx = X A --Hx < 0
Figure 3: Assertions in a Proof Outline
The assertions in a proof outline are intended to document what can be expected to hold of
the program state as execution proceeds. The proof outline of Figure 2, for example, implies that
if execution is started at the beginning of Si with x = 23 (a state that satisfies pre(S1)), then if
Si completes, post(Si) will be satisfied by the resulting program state, as will post(S). And if
execution is started at the beginning of 5 with x = X, then whatever assertion is next reached--Hbe
it pre(51) because X > 0 or pre(52) because X < 0--Hthat assertion will hold when reached, and
the next assertion will hold when it is reached, and so on.
With this in mind, we define validity of assertions and proof outlines. A valid assertion P
is one that holds in all program states, viz., states satisfying the datatype and control predicate
5
ftruej
a: cobegin
(x=lJ
b: skip
...
ff
coend
...
... 1
c: skip
Figure 4: Multiple Active Control Points (Partial proof outline)
axioms. A valid proof outline PO(S) will be one that describes a relationship among the program
variables and control predicates of 5 that is invariant and, therefore, not falsified by execution of
5. The invariant defined by a proof outline PO(S) is "if a control predicate ep is true, then so is
every assertion that PO(S) associates with cp" and is formalized as the proof outline inVariant for
PO(S):
1P0(s): A ((at(T) pre(T)) A (after(T) post(T)))
where T ranges over the subprograms of 5. For example, the proof outline invariant defined by
PO(S) of Figure 2 is:
at(S) ? (x = X A at(s))			A			afler(S) ? (x = X A afler(S))
A			at(S1)?(x=XAx >0)			A			afler(S1)?(x=XAx >0)
A			at(S2)?(x= XAx <0)			A			afler(S2)?(--Hx = XA--Hx <0)
Notice that proof outline validity is with respect to executions starting in any state, even a
state in the middle of the program. For example, the proof outline
5: a:
= 0 A y = 1)
x := r + 2
?x=2J
y := y + 2
fx = 2 A y =
is not valid. This is because a state where at(b), x = 2, and y = 20 hold satisfies 1Po(s)? but
starting execution in this state leads to one that does not satisfy 1P0(s).
In order to make the inference rules of our logic as easy to use as possible, we have designed
them so that hypotheses concerning proof outlines do not delve too deeply into the structure of
those proof outlines. Allowing multiple control predicates to be true simultaneously --H as we do
complicates the realization of this goal. Consider the concurrent program of Figure 4. There, at(a)
is true iff both at(b) and at(c) are true. Thus, in Figure 4. f at(a) and 1P0(S) are both true, then
x = 1 holds. However, pre(a) gives no warning of this requiiement; it is the trivial assertion "true"
6
To avoid such anomalies, we insist that a proof outline PO(S) give its requirements in its
precondition. If at(S) and pre(PO(S)) hold, then 1P0(S) must hold as well. We call such proof
outlines self-consistent, and require self-consistency of a valid proof outline along with invariance
of 1P0(S)
These invariance and self-consistency requirements for proof outline validity can be formalized
in terms of 1f+?-validity of Temporal Logic formulas, where 1t+? contains all infinite state sequences
constructed by executing programs C[Sj that contain a copy of 5. The elements a of lL+? are those
infinite sequences of states such that:
o+ ao is a state reached by executing some program C[S] zero or more steps from its initial state,
and
o+ each state a?+1 is a possible result of performing an atomic action of 5 from state Q', or, if
no action of 5 is enabled, repeating a?.
Note that ?i+? ? P denotes that a Predicate Logic formula P is valid, because every program
state is the first state of some sequence in 7f?+. We now define PO(S) to be valid if and only if
Invariance: ?+s k 1P0(S) ? 01P0(S)
Self-Consistency: 7i+? k (at(S) A pre(S)) ? 1PO(S)
From this definition we see that values of rigid variables are the same throughout any execution,
because free rigid variables in a temporal logic formula are implicitly universally quantified. This
means that rigid variables in proof outlines can be used relate the values of program variables from
one state to the next. For example, the proof outline of Figure 2 is valid and employs a rigid
variable X to record the initial value of x. Starting execution in a state where at(s2) and x = --H23
holds will satisfy 1P0(S) ? 01P0(S) even if x is 41 rather than --H23 because then 1P0(S) is not
satisfied (causing 1P0(S) ? 01P0(S) to be trivially satisfied).
2.3 Axiornatization for a Proof Outline Logic
Proof Outline Logic is an extension of Predicate Logic. The language of Predicate Logic is extended
with proof outlines for all atomic actions, commands, and ?rograms. The axioms and inference
rules of Predicate Logic are extended with axioms and inference rules that allow only valid proof
outlines to be proved theorems. In particular, there are some command-independent inference
rules as well as an axiom or inference rule for each type of command and atomic action. The
command-independent rules appear in Figure 5. With one minor exception, they will apply in our
real-time setting as well. We now turn to the axiomatization for a guarded-command concurrent
programming language.
The skip command is a single atomic action whose execution has no effect on any program
variable. Thus, it leaves primitive assertions--Hwhich only mention program variables and terms
that by their nature cannot chang?unchanged.
skip Axiom: For a primitive assertion P: ?P? skip ?PJ
The familiar Hoare [7] assignment rule applies:
7
(7)
P,fPJPO(S)?Qy,Q ? QI
(P'J PO(S) (Q')
Rule of Consequence:
Rule of Equivalence:
PO(S), 1P0(S) = 1P0'(S), pre(PO'(S)) A at(s) ? pre(PO(S))
P01(S)
(2)
(3)
Rigid Variable Rule: PO(S)XExp denotes a proof outline in which rigid variable X ill every
assertion is replaced by Exp, an expression involving constants and rigid variables
(only).
fP?PO(S)fQ)
?PEXxp? PO(S)EXxp ?QEXxp?
(4)
Conjunction Rule: P0A(S)OPOB(S) denotes the proof outline that associates assertion
AcpABcp with each control predicate cp, where Xcp is the assertion that POx(S)
associates with control predicate cp.
P0A(S),POB(S)
POA(S) ? POB(S)			(5)
Disjunction Rule: POA(S) ? POB(S) denotes the proof outline that associates Acp V Bcp
with each control predicate cp.
POA(S),POB(S)
P0A(S) 0 POB(S)
Figure 5: Command-Independent Rules of Ordinary Proof Outline Logic
(6)
Assignment Axiom:			For a primitive assertion P: fPe?) x := e ?PJ			(8)
Sequential composition of commands is like Hoare's rule without deletion of the intermediate
assertion:
Command Composition Rule:
fP)Si?Q),(Q)52fRJ
?PYS1 fQJS2fRJ
(9)
In order to reason about an if command, we must reason about its guard evaluation action as
well as the commands it guards. The following axiom allows us to derive proof outlines for guard
evaluation actions.
8
GEValif(S) Axiom: For an if command
S:ifBi?Sill.. llBn?Snfi
and a primitive assertion P,
(Pi GEvali(S) (P A (Ai at(Si) ? Bi))			(10)
A proof outline for an ifis then constructed by combining a proof outline for its guard evaluation
action with a proof outline for each alternative.
if rule:
(a) (P) GEValif(S) (R)
(b) (R A at(Si)) ? P1,
(c) (P1i PO(51) (Qi?
..., (R A at(Sn)) ?
fPni PO(Sn) (Qi
5:
if B1 ?(JN JPO(s1 )(Qi
II.
[I Bn?(i4?iPO(Sn)(Qi
fi
(11)
(Qi
The guard evaluation action for do selects a command Si for which corresponding guard Bi
holds. If no guard is true, then the control point foliowing the do becomes active.
GEvaI<j0(S) Axiom: For a do command
S:doB1?S1? . llBn?Snod
and a primitive assertion P,
(Pi GEvald0(S) (P A (Ai at(S?) ? Bi) A (after(s) ? (?Bi A ... A ?Bn)))			(12)
The inference rule for do is based on a loop invariant, an assertion I that holds before and after
every iteration of a loop and, therefore, is guaranteed to hold when do terminates--Hno matter how
many iterations occur.
(a)
(Il GEvald0(S) (Ri
(R A at(S1)) ? Pi, ..., (R A at(S?)) ?
(P1i PO(S1) (Il, ..., (Pni PO(Sn) (Il
(RAafter(S))?(IA?BiA??A?Bn)
tIJ
5:
do Bi?(PiiPO(S1)(Ii
[I...
II Bn?(PnJPO(Sn)f Ji
od
(IA?BiA???A?Bni
9
do rule:
(13)
The inference rule for a cobegin combines proof outlines for its component processes. An
interference-freedom test [12] ensures that execution of an atomic action in one process does not
invalidate the proof outline invariant for another. This interference-freedom test is formulated in
terms of triples,
NI(a, A): ?pre(a) A AJ a
that are valid if and only if a does not invalidate assertion A. If no assertion in PO(Si) is invalidated
by an atomic action a then, by definition, 1PO(Si) also cannot be invalidated by a. Therefore, we can
prove that a collection of proof outlines PO(S1), ..., PO(Sn) are interference free by establishing:
Interference Freedom
Foralii,j,1<i<n 1<j<n,i#j:
For all atomic actions a in Si
For all assertions A in PO(S5):
NI(a,A) is valid.
(14)
The following inference rule characterizes when a valid proof outline for a cobegin will result
from combining valid proof outlines for its component processes:
cobegin rule:
(a)			PO(S1), ..., PO(Sn)
(b)			P ? (A?pre(PO(Si)))
(c)			(Ai post(PO(Si))) ? Q			(15)
(d)			PO(S1),...,PO(Sn) are interference free
[P? cobegin PO(S1)fl...fiPO(Sn)coend fQJ
Since execution of an atomic action a in one process never interferes with a control predicate
ep in another, certain interference-freedom triples follow axiomatically.
Process Independence Axiom: For a control predicate ep in one process and an atomic
action a in another,
fcp = XJ a ?cp =			(16)
Notice that NI(a, ep) follows directly from this axiom when a and cp are from different processes.
2.4 From Proof Outlines to Safety Properties
Theorems of Proof Outline Logic can be used in verifying safety properties because of the way that
proof outline validity is defined. If a proof outline PO(S) is valid then 1Po(s) must be an invariant.
Suppose that 1Po(s) is an invariant. Then according to the method of Section 1 for proving safety
properties, we can prove that executions of 5 starting with pre(PO(5)) true will satisfy the safety
property proscribing ?Q by proving (at(s) A pre(PO(S))) ? 1Po(s) and 1P0(S) ? ?Q. The proof
of (at(S) A prePo(S)) ? 1P0(S) follows trivially from thj? ?ay Jp0(5) is defined. And, to prove
1P0(S) ? ?Q, we simply prove
(CpA Acp) ? Q			(17)
for every assertion Acp in PO(S), where Acp is the asse:' ion that PO(S) associates with control
predicate cp. For example, we prove as follows that for ije absolute value program in Figure 2
10
after(s) ? = IXI) holds during executions started in a state satisfying x = X A at(s): For the
case where cp does not imply after(s), (17) is trivially valid. The remaining cases are when cp is
after(s1), after(s2) and after(s). Here, we must show
All are valld.
after(s1) A post(s1)			?			(after(s) ? (x = Ixi))
after(5?) A post(s2)			?			(after(s) ? (x = lxi))
after(s) A post(s) ? (after(s) ? (x = lxi))
3 Real-time Logic
3.1 A View of Real Time
In taking into account real-time, our universe of discourse comprises processes executing parts of
some program along with an external world. We thus are forced to consider three kinds of actions:
Ordinary actions: Atomic actions without timing constraints are called ordinary actions. They
may execute whenever they are enabled, or wait arbitrarily long.
Real-time actions: A real-time action is an atomic action whose execution time is constrained.
Idles: Execution time may pass without the program doing anything. Such a passage of time can
be attributed to the external world, and we model this by an idle.
Ordinary actions are famillar, and the Proof Outllne Logic of Section 2 works fine for them.
Real-time actions cause no logical difficulties, as they have the same effects on variables and program
state as ordinary actions, but their execution is more constrained. Adding axioms to Proof Outllne
Logic suffices for reasoning about the execution time of real-time actions. Idles, strangely enough,
are more troublesome because their presence causes some matters of logical concern (viz., the time)
to change without program execution. For example, Rule of Consequence (2) is unsound when idles
are present.
In defining our logic, we consider an extremely powerful real-time language, allowing constructs
that may be impractical or impossible to implement. Programmers using actual languages will
not necessarily have access to all the features we allow. However, we belleve that most actual
programs in our intended domain can be translated into our language. Thus, expressive power is
an advantage: the more powerful our language, the greater the number of real programs that can
be expressed in it.
Our programming language is the one of Section 2 with additional real-time actions. In particu-
lar, for each unconditional atomic action4 a, we define corresponding real-time action (a??s,? where
6 and E are real-valued, non-negative constants. Execution of (a)??,cj causes the same indivisible
state transformation as a does, but constrains it to occur at some instant between e and E +6 time
units after the entry control point for (a)??,?? becomes active.
We have elected to characterize the execution time for a real-time action in terms of two parame-
ters (6 and E), following [14j, in order to gain fiexibillty in modelling various execution environments.
4An atomic action is unconditionai if it is executable whenever its entry control point becomes active. In the
programming notation of Section 2, skip, assignment, and the guard evaluation action for do are unconditional. The
guard evaluation for if is not unconditional.
11
Parameter E describes the fixed execution time of the action on a bare machine; 6 models execu-
tion delays attributable to multiprogramming and other resource contention. A system where each
process is assigned its own processor is modeled by choosing 0 for 6; a system where processors are
shared is modeled by choosing a value for 6 based on the length of time that a runnable process
might have to wait for a processor to become available.
As an illustration, suppose we know that assignment commands take one time-unit, and that
there is a single processor. If three assignment commands are started concurrently, they will be
executed in some order. The first one to run will be started immediately and take one time-unit;
the last one will be started two units after it was issued, and it also takes one time-unit. Thus we
could model this with real-time actions having an execution time of 1 and a possible delay of 2.
cobegin (xl := 1?[2,1lff(2 2?[2,11//(x3 ??[2,1J coend
We do not allow a in a real-time action (a)[8,f] to be a conditional atomic action, such as an
if guard evaluation action, because it is not clear what such a construct would mean. The delay
in a conditional atomic action is already dependent on something else changes to the program
state. Lower bounds on conditional atomic actions (e.g., an if command that requires at least one
time-unit to evaluate its condition) can be implemented with a real-time skip command followed by
an ordinary if. Timeouts on conditional atomic actions can be implemented by parallel processes
and shared variables.
When writing a real-time program, it is sometimes necessary to program a loop whose iterations
have fixed or bounded execution time. All of the atomic actions in such a loop must be real-time
actions. We therefore introduce the following syntax to specify that (CEvaI<i0(5)??6c1 be used as
the guard evaluation action in a do command:
d0[&fJBl?Sl?			[IBn?Snod
3.2 Reasoning About Real-time Actions
(18)
To reason about timing properties, terms are added to the assertion language and additional in-
formation is included in the program state. This is because the method of Section 2 for reasoning
about safety properties can only be used to prove safety properties for which the negation of the
proscribed ?Q is implied by each of a proof outline's assertions. Timing properties, by definition,
concern the instants at which control predicates become active, so we define a term tcp for each
control predicate cp:
Icp =
t t is the time that cp last became true
--Hoo cp has never been true
(19)
We also define a new real-valued term T to be equal to the current time.
Only certain assignments of values to these terms are sensible in a program state. In particular,
if two control points become active as part of the same event, then they must be assigned the same
time. For example, since S is the first subcommand of S T, we require that lat(s) = Iat(S T).
Similarly, the subcommands Si and S2 in S: cobegin Si ffS2 coend start at the same time, so
we require tat(Si) = ?at(S2) = tat(S).
Notice what effect adding these terms to the state has on the definition of proof outline validity.
Recall that a proof outline PO(S) is valid if execution starting in any state that satisfies 1P0(S)
leaves 1P0(S) invariant. Now, a state includes a time, and so we must consider starting states with
arbitrary times as well as arbitrary values for program variables and control.
12
Let C[S] be a program containing a copy of S. All initial state of C[Sj not only must satisfy
at(C[S]), but must be one in which the value of T is some non-negative number, and the values
of $at(T) and Iafler(T) (for every command T) are initialized properly. That is, for any control
predicate cp, if at(C[S]) ? ep is valid, then tcp has the same value as T; otherwise it is --H00. The
elements a of JiTs are those infinite sequences of states such that:
o+ a0 is a state reached by executing some program C[S] zero or more steps from an initial state,
updating T, Iat(T), and $afier(T) appropriately on each step.
o+ Each
from
state ai+1 is the result of performing an ordinary action, a real-time action, or an idle
a?. Execution of an ordinary or real-time action updates T, tat(T), and ?afler(T)
appropriately. Execution of an idle only updates T, and in a way that does not violate the
bounds ? and E associated with any enabled real-time action. If no action of S is enabled,
then the only transition permitted is an idle that does not increase T
Validity of proof outlines in our real-time logic is defined as before (Section 2.2), using ijT5 in
place of 1L?+:
Real-Time Invariance:
?T5 ? 1Po(s) ? 01P0(S)			(20)
Real-Time Self-Consistency: TLT5 k (at(S) A pre(S)) ? 1P0(S)
Axioms and Rules for Real Time
Execution of a real-time action (a???,? affects the program variables and control predicates in
the same ways as the ordinary action a from which it was derived. Therefore, we have the following
inference rule:
Real-time Action Transformation: For a an unconditional atomic action, P and Q
primitive assertions, and 0 < ? and 0 < c:
fPJa?Q1
?PJ (a??s,ci fQ)
(21)
Some additional axioms and inference rule aliow us to reason about formulas of our more ex-
pressive assertion language. First, the various non-atomic conimands of our programming language
give rise to axioms based on the way they equate their components' control points. These axioms
are similar to the control-predicate axioms. For our programming language, these axioms are given
in Figure 6.
Next, there are the additional axioms given in Figure 7 for the assertion language. In these, cp
can denote any control predicate, including those not associated wi! h entry or exit control points for
real-time actions; 5 is the label for a real-time action (o?[6,?. Axioms (22) and (23) follow directly
from the definition of tcp. Axioms (24) and (25) capture the essence of a real-time action--Hthat
its entry control point cannot stay active too long. This, iii t?urn, ?llows us to infer that a control
point is not active by using the following corollary of (24):
(I at(S) + ? + E < T) ? ?ut(S)
13
(26)
For 5 the sequential composition 5i 52
lat(S)
lafler(S)
Iafier(Si)
For all if command:
tat(S)
tafler(S)
$afler(GEvaijf(S))
--H tat(S1)
--H tafter(S2)
--H tat(S2)
5: ifB1?S1????llBn?nfl
--H Iat(GEvaljf(S))
--H max(tafler(S1), ... ,tafler(S?))
--H max (tat(S1), ... ,tat(Sn))
For a do command:
tat(GEvaI?0(S))
tafler(GEva?0(S))
?in(S)
at(S)
in(Sj)
after(S)
5: d0B1?S1ll????Bn?Snod
--H max (tat(S), tafter(Si),..., tafler(S?))
--H max (tafler(S), tat(S1),.. .,tat(S?))
tafter(S) = tafler(GEval?o(S))
tat(S) = tat(GEval<i0(S))
tat(S?) = tafter(GEvaii0(S))
--H? tafter(S?) = tat(GEval<i0(S))
For a cobegin command:
5: cobegin ..... //Sn coend
tat(S)			=			tat(S1) = tat(S?) = . = tat(S?)
tafler(S)			max(tafter(Si).			tafler(S?))
Figure 6: Control Time Axioms
The way these new terms change value when atomic actions execute is captured by new axioms.
For any ordinary or real-time atomic action a and control predicate ep, we have:
cp Invariance			fep = C A tcp =			a f(cp ? C) ? (tcp = V)?			(27)
The antecedent in the postcondition is necessary for the case where cp could become true when a
finishes, e.g., cp = after(a).
Next, for any ordinary action, we have:
Action Time Axioms:
< tat(S))			5: a			< tafter(S))			(28)
fK < TJ			5: a			< tafter(S))			(29)
Action Time Axiom (28) asserts that the exit control point for 5 becomes active after the entry
control point for 5 last became active. Action-time Axiom (29) makes the subtly different assertion
tep			(22)
(tcp= --Hoo)			(23)
at(S)			(24)
tat(S) ? --Hoo			(25)
Figure 7: General Real-Time Axioms
?cp
tat(S)<T< t(1t(S)+6+e
tafter(S) <
14
that the exit control point for S becomes active after every time that the entry control point for S
was active.
For a real-time action (a??6?j, the following axiom characterizes how execution changes the
$c?terms.
Real-time Action Axiom fK < tat(S)J 5: (a?t6?i fK + E < tafier(S)1
(30)
This axiom is analogous to Action-time Axiom (28), except that now the postcondition has been
strengthened to give a tighter lower-bound on when the exit control point for 5 first becomes active.
Two things that the Real-time Action Axiom (30) does not say are worthy of note. First, this
axiom does not bound the interval during which the entry control point for 5 is active; Axiom (24)
serves that role. Second, one might expect the following triple to be valid--Hits precondition being
similar to that of (29).
fK < T? 5: (a?[s,?] ?K + E < T?			(invalid)			(31)
Unfortunately, (31) is not sound. Execution of 5 started in a state such that Iat(a) <K < T would
satisfy the precondition but might terminate before K + E. For example, consider an execution of
(a??021 that is started at time 0. Thus, at time T = 1 the state satisfies K <T if we choose K =1,
and so precondition K < T is satisfied by that state. When execution of (a??0,2? terminates--H2
units after it is started--Hat time T = 2, the postcondition K + E < T is 1 + 2 < 2, which is false.
Finally, the following rule allows rigid variables to be instantiated with expressions involving
Ic?terms. (Rigid Variable Rule (4) only allows rigid variables to be instantiated by constants,
rigid variables, or expressions constructed from these.)
?c?Instantiation
fmp=VJ a ?$cp=VJ, fP) a fQJ
a QXTcp
(32)
This rule is typically used along with cp Invariance (27). For the case where real-time action
a and control predicate cp are in different processes, the first hypothesis of Ic?Instantiation is
automatically satisfied due to Process Independence Axioms (16). Thus, we obtain a derived rule
of inference:
Derived Ic?Instantiation
a and cp are in different processes,
?PJa?Q)			______
?Pjx? a Q?tcp
(33)
3.3 Rule of Consequence Revisited
Most of the axioms and proof rules of Proof Outllne Logic are sound in our real-time setting.
However, the Rule of Consequence (2) is unsound and needs revision. We also need to revise
the notion of interference freedom. While the Owicki-Gries cobegin rule [12] is sound, when the
assertion language concerns real time, the rule is is no longer complete and, in particular, not
powerful enough for even simple examples of concurrent real-time programs.
Rule of Consequence (2) is invalid in any setting where some aspect of the state is not under
program control. Recall, the rule is:
15
Maxidle(a)
MaxIdle((a)?6?)
Maxldle(51 52)
Maxidle(if. .fi)			--H oo
MaxIdle(do... od)
MaxIdle(do[5,]?? od)
MaxIdle(cobegin51ff...fl5?coend)			=
oo			? ordinary
6+E
Maxidle( 51)
oo
mill ?Max1dle(5j)ii = 1,.
Figure 8: Definition of Maxidle(S), the maximum idle of 5
P'?P, (P)PO(5)fQ), Q?Q'
(P') PO(S) (Q')
The difficulty is illustrated by the following example. Consider the following proof outline, which
is valid in our model:
> 4) 5: skip ?true)			(34)
Furthermore, note that
(35)
is valid. However, if we apply the Rule of Consequence to (34) and (35), we obtain the following
proof outline:
fT = 4) 5: skip ftrue)			(36)
It is invalid because an idle by the environment invalidates its precondition, T = 4. In particular,
let ? be a state in which at(s) A T = 4 is true. Therefore, the precondition of (36) is satisfied by
?, and so is 1P0(s). An idle can lead to a state ?` in which at(S) A T = 4.01, invalidating 1P0(S).
Thus the proof outline does not satisfy Real-Time Invariance (20), and hence is not valid.
We eliminate problems of this sort by modifying Rule of Consequence (2) so that idles cannot
invalidate a strengthened precondition P'. In light of (36), an obvious approach is to rule out any
strengthening of preconditions achieved by placing an upper bound on T. However, that restriction
would prevent us from deriving the valid triple
flat(S) = 4 A 4 < T < 6) 5: skip[0,21 ftrue). (37)
We therefore characterize the interval over which a streiigthened precondition P' must not be
invalidated by an idle. For any program 5, define Maxldle (maximum idle time for 5) to be the
longest real time interval that can elapse after at(5) beconie? true but before some program action
of 5 must be executed. If 5 may idle arbitrarily long, then Ai'axldle(S) = 00. Figure 8 gives a way
to calculate Maxidle(S) by induction on the structure of 5.
For example,
Maxldle(skip) =
as skip can wait arbitrarily long before taking a step, and
Maxldle(cobegin SkiPff(skip?[0,2; coend) = 2
16
as that program will necessarily take a step at or before time 2. In order for Rule of Consequence
(2) to be sound, not only must P'?P hold but P' must remain true until time $at(5)+Maxldle(S).
We say that an assertion P is patient for s if
(P A at(S)) ? (vd.(T < d < lat(S) + Maxidle(S)) ? paT) (38)
Thus, if P' is patient for 5, then P' can be a precondition for 5 and no idle by 5 can invalidate
P'. For example, 4 < T < 6 is patient for (skip)[0,2], but 4 < T < 5 is not. A corollary of the way
7isT is constructed is that the precondition of any vaild proof outline PO(S) is patient for 5.
Note that under some circumstances P' is easily demonstrated to be patient for 5:
o+ If P' does not mention T
o+ If P' only gives lower bounds on T
However, even assertions involving upper bounds on T can be patient. For example,
?at(5) = 4 A 4 < T < 6
is patient for 5 : skip[0,2].
A sound Rule of Consequence for our real-time logic can be formulated in terms of patient
assertions:
Rule of Consequence:
? P, P' is patient for 5, fP) PO(S) fQ), Q ? QI
(P') PO(S) (Q')			(39)
So, because T = 4 is not patient for skip, it is not possible to deduce (36) from (34) and (35)
using this new Rule of Consequence. On the other hand, because
(?at(5) = 4 A 4 < T < 6) ? T> 4			(40)
is valid and tat(S) = 4 A 4 < T < 6 is patient for Skip[0,2], we can use the Rule of Consequence
(39) to infer
ftat(S) = 4 A 4 < T < 6) skiP[0,2] ftrue) (41)
Note that we do not need to place similar restrictions on Q'. The interpretation of fP) PO(S) fQ)
is that, when 5 finishes, Q remains true indefinitely. If Q ? Q' in predicate logic, and Q remains
true forever, then Q' will also remain true forever.
The following derived rule, the Simple Rule of Consequence, handles most of the bookkeeping
uses of the Rule of Consequence (39):
PI=P,fP)PO(S)fQ),Q ? QI
Simple Rule of Consequence			fP') PO(S) (Qli
17
(42)
3.4 Interference Ireedom Revisited
When execution times of atomic actions are bounded, certain forms of interference cannot occur.
This is illustrated by the following proof outline.
fx=OJ
cobegin
fx=OJ
1/
a: := x + 1)[o,2] fx = 1J
?: (y := x + 1)[o,1] ?Y = 11
f=OJ
coend
= 1 A y = lJ
It is valid, but cannot be derived using the cobegin Rule because PO(a) and PO(P) are not
interference free. In particular, NI(a, pre(P)) is not valid.
NI(a, pre(P))
fpre(a) A pre(P)J (x := x + 1)(o,2] ?pre(P)J
= OJ (x := x + 1)!o,21 ?x = OJ
Using operational reasoning, however, it is not difficult to see that executing a cannot invalidate
pre(P), so PO(a) and PO(P) should be considered interference free. This is because according to
Figure 6, both at(a) and at(P) become active at the same instant, say time 0. By definition, a
completes at time 2, and so x remains 0 until this time. Real-time action ? completes at time 1
and, therefore, must find x to be 0. Thus, it is simply not possible for a to change the value of x
while at(P) is active.
The ordinary cobegin Rule (15) is based on a form of interference freedom that does not take
into account execution-time bounds of real-time actions. In particular, NI(a, Acp) does not account
for the fact that although A? might be associated with an active control point cp when a is started
then we may be able to prove that cp cannot be active when a completes. The remedy is to refine
NI(a, Acp) taking into account the time bounds for how long an entry control point for a real-time
action can remain active. The foliowing triple accomplishes this.5
NIrt(a, A?): fat(a) A pre(a) A cp A a fcp ?
Returning to the example above, we now have:
NIrt(a, pre(P))
fat(a) A pre(a) A at(P) A pre(P)J (x := x + 1?[o,21 ?at(P) ? pre(P)J
?at(a) A at(P) A x = OJ (x := x + 1)[o,2] (at(P) ? x = OJ
And, this obligation can be discharged as follows. We present the proof in detail, to show how
the axioms and rules fit together. Steps that involve standard logic (including arithmetic) are listed
as simply "predicate logic."
5This triple is not specific to real time; see [11] for example. It ari.?<?s naturally when one attempts to construct a
proof rule for cobegin. In many cases, it can be simplified to the Owicki-Cries condition, but here it cannot.
18
1. Real-time Action Axiom (30)
< Iat(a)) a			X + 1?[o,2]
fK + 2 < ?afler(a)1
2. Derived Icmlnstantiation (33) with 1, substituting Iat(P) for K
?Iat(P) < Iat(a)J a : X + 1)[o,2] ftat(P) + 2 < Iafler(a))
3. Axiom (22) with tafler(a) for Icp, and predicate logic
(tat(P) + 2 < tafter(a)) ? (Iat(P) + 2 <
4. Simple Rule of Consequence, (42) with 2 and 3
ftat(P) < ?at(a)J a : ? + 1?[Q2] flat(P) + 2 <
5. Axiom (24) and predicate logic
at(P) ? tat(P) < T < Iat(P) + 1
6. Predicate logic and arithmetic:
(at(P) ? tat(P) < T < ?at(P) + 1) ? ((Iat(P) + 2 <			? ?at(P))
7. Modus Ponens from 5 and 6
(tat(P) +2< T) ? ?at(P)
8. Simple Rule of Consequence with 4 and 7
flat(P) < Iat(a)Y a: := x + `?[o,2] f?at(P))
9. A Control Time Axiom from Figure 6
?at(a) = Iat(P)
10. Predicate logic from g
tat(P) < tat(a)
11. Predicate logic from 10, since anything implies true
pre(N4t(a, pre(P))) ? tat(P) < tat(a)
12. Predicate logic
?`at(P) ? post(NIrt(a, pre(P)))
13. Rule of Consequence with 8, 11, and 12; patience is vacuous
ATIrt(a, pre(P))
19
Notice that information about the time after a is accumulated ill steps 4 and 5, and used ill
step 6 to reach the same conclusion that operational reasoning gave: that, once a finishes, p has
also finished.
4 Example: A Mutual Exclusion Protocol
cobegin
6: ifx = 0 c: := 1)[s(c),c(c)]fi
d: (SkiP)[6(d),c(d)]
e : if x = 1 f: Critical Section fi
fi
6' : ifx = 0 c': (x := 2?[6(c'),f(c')1 ?
: (Skip??6??i?,???i??
: if x = 2 f': Critical Section fi
coend
Figure 9: Core of Fischer's Mutex Protocol
Knowledge of execution times can be exploited to synchronize processes. A mutual exclusion
protocol attributed in [10] to Mike Fischer [4] illustrates this point. The core of this protocol
appears in Figure 9. There, c, d, c? and d' are real-time actions. Provided the parameters defining
these real-time actions satisfy
and
?(c') + E(c') < E(d)			(43)
?(c) + E(c) < E(d')			(44)
this protocol implements mutual exclusion of the marked critical sections, as we now show.
Mutual exclusion of at(f) and at(f') is a safety property. It can be proved by constructing a
valid proof outline in which pre(f) ? ?at(f') and pre(f') ? ?at(f). A standard approach for this
is to construct a valid proof outline in which ?(pre(f) A pre(f')) is valid. It is thus impossible for
at(f) A at(f') to hold, because that would imply pre(f) A pre(f').
A proof outline for the first process is given in Figure 10; the proof outline for the other process is
symmetric, with "1,, everywhere replaced by "2" and the primed labels interchanged with unprimed
ones. Notice that pre(f)?x = 1 and pre(f)?x = 2. Thus, the proof outlines satisfy the conditions
just outlined for ensuring that states satisfying at(f) A at(f') cannot occur.
It is not difficult to derive the proof outline of Figure 10 using the axiomatization of real-
time actions given above. The proofs of (pre(c)J c fpost(c)J and (pre(d)? d fpost(d)) are the
most enlightening, as they expose the role of assumptions (43) and (44) in the correctness of the
protocol. Here is the proof of fpre(c)J c (post(c)?:
Let
M = ?(c') + E(c') --H E(d)
1.			Axiom (29)
< TJ c:			:= 1)[s(c),f(c)] fK < tafier(c))
20
(true?
b:			ifx = 0			(tat(c') <
c:
(x $ 0 A (at(c') ? Iat(c') + M < Iat(d)))
fi
(x $ 0 A (at(c') ? tat(c') + M < Iat(d)))
d:
(x $ 0 A
e:			ifx = 1			= 1 A ?at(c')?
f: Criticai Section 1
?trueJ
fi
ftrue)
Figure 10: Proof Outline for Fischer's Algoritlirn
2. Derived IcThlnstantiation. (33). on step 1? to substitute tat(c') for K
(tat(c') < TJ c: := 1)[&(c),c(c)] ftat(c') < tafier(c)1
3. Control Time Axiom (Figure 6) for if and sequencing
Iafler(c) = tat(d)
4. Predicate logic on step 3. and M < 0 by (43)
(Iat(c') < tafler(c)) ? (Iat(c') + M < Iat(d))
5. Predicate logic on step 4
Iat(c') < tafler(c) ? (at(c') ? (Iat(c') + M < Iat(d)))
6. Simple Rule of Consequence (39) on steps 2 and 5
ftat(c') < TJ c:			:= 1)[6(c),c(c)] (at(c') ? (Iat(c') + M < Iat(d)))
7. Assignment Axiom (8)
= 1J c: := 1)[6(c),f(c)] fx =
8. Predicate logic
true ? (1 = 1)
21
9. Predicate logic
x=1?x$0
10. Rule of Consequence, (39) on steps 7, 8, and 9, since true is patient for c.
?trueJ c:			1)[6(c),c(c)] fx $ 0)
11. Conjunction Rule (5) on steps 10 and 6, plus a trivial use of the Rule of Equivalence (3).
(Iat(c') < T) c: 1)t??c?,qc?j fx $ 0 A (at(c') ? Iat(c') + M < Iat(d)))
And, here is the proofof (pre(d)) d (post(d)).
1. Real-time Action Axiom (30)
< Iat(d)) d: (SkiP)[6(d),c(d)] ?K + E(d) < Iafter(d))
2. skip Axiom (7)
(L < K) d: (SkiP)t&(d),E(d)] (L < K)
3. Conjunction rule (5) on steps 1 and 2
?L < K A K < Iat(d)) d: (Sk?P)[s(d),c(d)i fL < K A K + E(d) < Iafter(d))
4. Predicate logic
(L < K A (K + E(d) < tafler(d))) ? (L + E(d) < Iafler(d))
5.
Rule of Consequence (39) on 3 and 4, noting that the precondition does not mention time and is
thus patient.
fL < K < Iat(d)) d: (Sk?P)[6(d),c(d)] fL + E(d) < Iafter(d))
6. cp Invariance axiom, (27)
(at(d) = C A Iat(d) = V) d: (SkiP?[s(d),?(d)l ?(at(d) ?			? (Iat(d) = V))
7. Rigid Variable Rule (4) on 6, replacing C by true
?at(d) = trueA Iat(d) = V) d: (SkiP?(s(d),f(d)] f(at(d) ? true) ? ($at(d) = V))
8. Rule of Equivalence (3) on 7
flat(d) = V) d: (Sk?P?[s(d),c(d)l flat(d) = V)
9. Icp-lnstantiation (32) using 8 and 5 to substitute Iat(d) for K.
< tat(d) < ?at(d)) d: (SkiP?[6(d),?(d)l ?L + E(d) < Iafler(d))
10. Rule of Equivalence (3) on 9
< Iat(d)) d: (Sk?P?[s(d),f(d)] ?L + c(d) < Iafler(d))
22
11. Derived tc?lnstantiation (33), and Rigid Variable Rule (4), to substitute tat(c') + M for L in 10
flat(c') + M < Iat(d)) d: (Sk?P)[s(d),c(d)] (tat(c') + M + E(d) < ?afler(d))
12. Process Independence Axiom (16), Rigid Variable Rule (4), and Rule of Equivalence (3)
(?at(c')) d: (Sk?P)(6(d),c(d)l (?at(c'))
13. Disjunction rule (6) on steps 11 and 12
(?at(c') v (Iat(c') + M < tat(d))) d: (Sk?P?[6(d),f(d)] (?at(c') v (tat(c') + M + E(d) < Iafler(d))1
14. Rule of Equivalence (3) on 13
(at(c') ? (Iat(c') + M < Iat(d))J d: (skiP)t6(d),?(d)J f?at(c') v (Iat(c') + M + E(d) < Iafter(d))J
15. Axiom (22)
tafler(d) < T
16.
?at(c') V Iat(c') + E(c') + 6(c') < Iafler(d)
? Predicate Logic from step 15
??at(c') v (Iat(c') + E(c') + 6(c') < T)
?lEquation (26)
?at(c') v ?at(c')
? Predicate Logic
?at(c')
17. Simple Rule of Consequence (42) on steps 14 and 16
(at(c') ? (tat(c') + M < Iat(d))J d: (Sk?P?[s(d),f(d)] (?at(c'))
18. skip Axiom (7)
fx $ OJ d: (Sk?P)[6(d),f(d)] ?x $ OJ
19. Conjunction Rule (5) on steps 18 and 17
?x $ 0 A (at(c') ? (tat(c') + M < tat(d)))? d: (Sk?P)[S(d),f(d)] (x $ 0 A
Notice how timing information is used in step 16 to infer that a particular control point cannot
be active.
5 Related Work
It is instructive to compare our logic with that of [17j, another Iloare-style logic [7] for reasoning
about execution of real-time programs. In [17], the passage of time is modeled by augmenting each
atomic action with an assignment to an interval-valued variable RT, so that RT contains lower and
23
upper bounds for the program's elapsed execution time. The equivalent of our Command Composi-
tion Rule (9) and the Assignment Axiom (8) would then be used to derive rules for reasoning about
these augmented atomic actions.6 In contrast, our logic is obtained by augmenting the assertion
language (of an underlying logic of proof outlines) with additional terms (tcp and T) and devising
new axioms for reasoning about these terms. We cannot derive rules for real-time actions simply
by using the original logic, because we do not employ assignment commands to model the passage
of time.
Although our logic is more complex, by augmenting the axioms rather than the atomic actions
we are led to a more powerful logic. First, having the icpterms allows the logic to be more expres-
sive. These terms permit the definition of properties involving historical information--Hinformation
that is not part of the current state of the program. Timing properties that constrain the elapsed
time between events can only be formulated in terms of such historical information. The logic of
[17j has no way to express historical information and, consequently, can be employed to reason
about only certain timing properties.
Second, our axiomatization allows reasoning about programs whose timing behavior is data-
dependent. The logic of [17] does not permit such reasoning. For example, because of the way
command composition is handled in [17], the logic produces overly-conservative intervals for time
bounds. This is illustrated by the following sequential program, which takes at least 10 time units
to execute.
ifB			skip[o,9j II ?B			skip[o,ljfi
if?B			skip[0,9] [B			skip[0,1Jfi
This fact can be proved in our logic; the logic of [17] can prove only that execution requires at
least 18 time units.
A lloare-style programming logic for reasoning about real-time is also discussed in [8]. That
work is incomparable to ours. First, the programming language axiomatized in [8] is different,
having synchronous message-passing and no shared variables. This is symptomatic of a fundamental
difference in the two approaches. The emphasis in [8J is on the design of compositional proof
systems. Shared variables could not be handled compositionally and so they are excluded from
programs. In contrast, we do not require that our proof system be compositional, and we do
handle shared variables.7 Moreover, it would not be difficult to extend our logic for reasoning (non-
compositionally) about programs that employ synchronous message-passing or any of the other
communication/synchronization mechanisms for which Hoare-style axioms have been proposed.
The set of properties handled in [8J is also incomparable to what can be proved using our
logic. Our timing properties make visible the times at which control points become active (through
tc?terms). A compositional proof system cannot include information about control points in its
formulas, because they betray the internal structure of a component. The logic of [8], therefore, may
only be concerned with times at which externally visible events occur: the time of communications
events and the time that program execution starts and terminates. This turns out to allow proofs
of certain liveness properties as well as certain safety properties. Our logic cannot be used to prove
any liveness properties other than those implied by the progress of time.
6The idea of augmenting actions with assignment commands in order to reason about the passage of time is also
discussed in [5], where it is used to extend Dijkstra's wp [3] for reasoning about elapsed execution time. A more
recent effort to augment a wp calculus for real time is reported in [16].
7The cobegin Rule of Proof Outline Logic (15) is not compositional because its interference-freedom test depends
on the internal structure of the processes being composed.
24
6 Concerns
A concern when designing a logic is expressive completeness. Our timing properties include many,
but not all, safety properties of interest for reasoning about the behavior of real-time programs.
This is because the historical information in a timing property is limited to times that control points
become active. One might also be concerned with the elapsed time since the program variables last
satisfied a given predicate or with satisfying constraints about how the program variables change
over time. These are safety properties, but neither is a timing property (according to our definition).
In general, safety properties can be partitioned into invariance properties and history properties
[15]. The invariant used in proving an invariance property need only refer to the current state; the
invariant used in proving a history property may need to refer to the sequence of states up to the
current state. Timing properties are a type of history property.
A version of Proof Outline Logic does exist for reasoning about history properties [15]. It
extends ordinary Proof Outline Logic by augmenting the assertion language with a "past state"
operator and a function-definition facility. In this logic, our tc?terms can be constructed explicitly;
they need not be primitive. And, the more general class of safety properties involving times--Hbe it
times that predicates hold or times that control predicates hold--Hcan be handled.
A Outline of the Soundness Proof
A.1 Scheme of the Proof
Our soundness proof has a straightforward structure. First we build a model, using structural
operational semantics (SOS) [13, 18, 6]. We then show how to interpret expressions and formulae
of the logic in this model. Using the model, we define the set of execution sequences 7iTs used to
define validity in Section 3.2. We prove a series of "sanity lemmas," showing that the intuitive
definitions presented earlier match the formal definitions. Finally, we check each of the axioms and
proof rules against the model.
The most subtle part of the construction is in building the model. Checking the axioms and
proof rules is long but straightforward. In our model, we give a structural operational semantics
for our programming language. States ? include all of the information necessary to interpret Proof
Outline Logic assertions. And, the operational semantics define the relation ? , stating that a
program in state ? can perform a single atomic action, or can idle, and enter state ?`.
Using ?, we construct a linear-time temporal-logic model of a program S; that is, a set of
infinite sequences F of states. We define a notion of "? is a suitable initial state for S". We get an
arbitrary consistent state ? by running an arbitrary suitable initial state ? for S arbitrarily long,
? ?? ?. ?Ts is then the set of executions of S started in arbitrary consistent states ?.
Having defined liTs, we have have enough information to use the definition of Section 3.2 that
[= PO(S) when 1tT5 k 1P0(s) ? 01P0(S). This puts us in a position to check the soundness of the
logic, which is tedious but not difficult.
A.2 Defining the transition relation
Defining relation `,` is nontrivial. The values of control predicates, especially at the beginning
and end of concurrent segments, change in fairly complicated ways. Consider the program of
Figure 11. When the cobegin labelled a finishes, afler(c) or after(d) will hold as well as afler(g)
and afler(h); and at(j), at(1), and at(m). A single atomic action --H say, g finishing --H may cause
other actions at faraway points in the program to start. Or it may not.
25
a: cobegin
b: if
/1
fi
B1			c:			skip
B2			d:			skip
skip
cobegin
fi
coend
coend
cobegin
j: skip
cobegin
I:
ff
coend
coend
skip
skip
skip
skip
Figure 11: Control flow example
Any description of the state transition function will, at some level, involve an inductive analysis
of the structure of the original program. We thus chose to define the operational semantics of
processes directly, using SOS. In this style, the behavior of a composite program is defined in terms
of the behavior of its subterms. Since the state ? must contain enough information to interpret all
assertions in Proof Outline Logic, it must include:
o+ at(1) and after(t) for each label 1
o+ values of program variables
o+ values of rigid variables
o+ Iat(1) and tafler(1) for each label 1
All save the first can be encoded directly as components of a tuple. For example, if ? is a state,
then ?.?at(.) is a function from program labels to times, and ?.a(.) is a function from program
variables to values. Following the usual SOS methodology, program counters in a state 7 are
represented by the partial program 7.S that remains to be executed. We assume that programs are
completely labelled; that is, each command (simple and composite) has a unique label, as in the
example above. We also introduce a new command, done, indicating that a thread of computation
has finished.
26
We 110W define the relation ? ?` by induction on ?.S. By ill large, if ? , ?`, then ? and ?`
are almost the same; e.g., most variables won't change values. We therefore present the SOS rules
by explaining the differences between ? and ???8 For example, if ?.S is the program 1: skip, then
the operational rule which applies to ? is:
If
= 1: skip
= I:done
?`.T> ?.T
?` is otherwise the same as
Then ?`,
The behavior of a composite process is determined inductively by the behavior of its subpro-
cesses. For example, cobegin ....... fiSn coend can act if one of the Sj's can act without exceeding
the time bounds of the other Sd's. This happens if there is a state ? in which the program is simply
the Si that performs the the transition. Thus, the rule for cobegin is roughly:
If
= cobegin ..... ......... ffSn coend,
= cobegin ..... - #S'fl - ffSn coend,
where ??o, ?o' such that:
= Sj
?o is otherwise the same as
No other component of ?.S is required to act before ?.T
?` is otherwise the same as
Then ?
Of course, the English antecedents are made formal.
Idle actions are described by:
If
?`.T> ?.T
?.S is not required to act before ?`.T
?` is otherwise the same as
Then ?
One important consequence of using a structural operational semantics is that ? ?` iff there
is a proof of ?			?` from the operational rules. These proofs			can be regarded as formal objects,
and, in particular, we can do induction on the proof that ?			?`. Many of the basic lemmas used
for soundness proceed by such inductions.
This discussion omits subtleties that are essential to the proof. For the model construction, the
actual proof rules assign responsibility for the transition, so that when we define JiTs we can ensure
that 5 takes all the transitions in ijT5 Roughly, a subterm 5' of the program ?.S is responsible for
the transition ? , ?` if 5' appears as ?.5 in the proof of ? `, ?` or if the transition is idle. The
determination of which processes are finished requires some care. For example, done is a finished
atomic process, but there are also others, such as cobegin doneffdone coend. While the intuition
is reasonably straightforward, the details are delicate.
8In the full proof, we use a more standard SOS notation, which makes the structural induction clearer but requires
extra notation.
27
A.3 Interpreting Expressions and Formulae
The meanings of most expressions and formulae can be read directly from the state ?. For example,
the value of the expression x + y in state ? is the sum of ?.?(x) and ?.a(y). However, the values of
control predicates at(1) and after(1) depend on the control state ?.S of the program. In this section,
we sketch the interpretations of these predicates for the case when 1 is the label of an atomic action.
Let ? be a state in an element of 7tTs. Interpreting afler(1) where 1 is the label of an atomic
action is straightforward; 7.5 includes a subterm of the form 1: done if and only if the atomic
action labelled tin 7.5 is finished.
We define the set of active atomic actions of a program 5 inductively; e.g., if 5 is atomic,
act(S) = f5J, and e.g.
act(cobeginSiff... ff5?coend)
if S? is not finished, act(5i52)
if Si is finished, act(SiS2)
--H U?act(5j)
--H act(Si)
--H act(s2)
Then 7 k at(1) if 1 is the label of an atomic action in act(?.5). In the actual proof, we allow at(1)
when 1 is the label of any program, not just the label of an atomic action. This complicates the
definition of act somewhat and requires use of an extra set of markers in the operational semantics.
However, it allows us to verify the Proof Outline Logic control predicate axioms without having
built them directly into the definition of 7 k at(1).
A.4 Sanity Checking
We demonstrate that the operational semantics and notion of interpreting processes are reasonable
by proving a series of sanity lemmas. These are lemmas that are not necessarily used in the
soundness proof proper but show that the formal definitions derived from the operational semantics
agree with the less formal ones used in the body of this paper. The following sanity lemma, for
example, shows that the intuitive definition of Iat(1) as the last time that at(1) became true agrees
with the formal definition of Iat(1) as it appears in the operational semantics:
Let 70 be a snitable initial state, and 7o `" 71 ` Then, for any index i and
label 1, 7i.tat(t) is:
o+ --Hooif(VO<j<i : 7j?at(1))
o+ 7j.T if J is the largest 0 < j < i such that (7j--Hi ? at(1) and ?? k at(1)).
o+ 70.T, if neither of the preceding conditions obtains; that is, if 7o ? at(1) but
7j ? at(1) A 7j+i ? at(1)).
That is, the time that the bookkeeping mechanism gives for Iat(1) is in fact the value of the clock
on the most recent instant that at(1) became true.
A.5 Soundness
Once the SOS rules have been constructed and their sanity checked, it is a routine matter to show
soundness of all the Real-Time Proof Outline Logic axioms and proof rules. We define the model
liTs in the following way. We consider executions starting with 5 in an arbitrary state of control
and memory. We allow other processes in this initial state as well. We thus consider executions
that start with some program that includes 5; we run this program for a time (which gives an
arbitrary state, perhaps with 5 partially executed). However, in the sequences in ji5T, only 5 is
aliowed to take steps, so 5 must be responsible for each transition.
28
o+ ? is all initial state for S iff ?.S includes S as a subprogram, and ?.Iat(l) and ?.Iafler(l) are
initialized properly. That is, ?.Icp = ?.T if ?.S k cp, and to --Hoo otherwise, for cp a control
predicate.
o+ liTs is the set of all sequences (?o,?i, . .) such that ? ?? ?o for some initial state ?, and
?+i for every i, and S is responsible for each transition.
Note that TLT5 is suffix?closed; that is, if (?o, ?,...,?, ?+1,..)ETLT5, then also (?,?+i,..) C TLT5.
To prove the Control Predicate Axioms of Figure 1 sound, we characterize possible control
states of a program and possible executions of a program. For example, omitting labels, done S is
a possible subterm of a control state (as skip S can evolve into it); but S done is not possible (the
first in a sequence of commands is executed before the second).
Similarly, we say that program fragment S' is a descendant of s if (roughly) there are states
? ?? ?` such that ?.S = S and ?`.S = S'; it is a proper descendant if s # S'. We characterize the
descendants of all terms. For example, let S be a command sequence 1: ((m : S1)(n : s2)), and S'
be a descendant of S. Then there is at most one subterm of S' labelled I, and it must be:
o+ (:((m:S1,)(n :S2)) where ?i' is adescendant ofS1,or
o+ I : (n : S21) where S21 is a proper descendant of S2.
Soundness of the Control Predicate Axioms follow easily from these characterizations. For
example, for one direction of the axiom for sequencing, after(m) = at(n), we calculate that if
k after(m), then there must be a subterm m : doneof ?.S. From the preceding characterization,
this means that n : S2 must also be a subterm of ?.s; and, by the definition of at(.), this implies
that at(n) holds as well.
The other axioms and proof rules are proved similarly. For example, to show (22), we show by
induction on the proof of ? , ?` that
(?.T <
(45)
Suppose that ? `,` ... is a sequence of transitions from an initial state. By induction on i
and the definition of initial state, we show that ?.1at(l) and ?.?afler(l) are either --Hco, or
for some j < i. This and (45) suffices to show (22).
Axioms and rules involving proof outlines require verifying statements of the form 1tT5 k I? 01.
From temporal logic, we know that, if I ? or is valid, so is I ? 01. I is a predicate logic formula
rather than a temporal one, hence it is true or false in a single state. It thus suffices to show that,
for each ? ?? ? where ? is an initial state for S, if?0 ? I, then ? ? I.
We use this method to verify each proof outline axiom and proof rule. All these verifications
proceed by induction on the proof of the transition ? `` ?i. For example, to check skip Axiom (7),
let S = I : skip. 1P0(S) = (at(l) ? P) A (afler(l) ? P), where P is primitive. Suppose ?o ? 1Po(s).
It is easy to show that ? k P is independent of 7.5 and 7.T if P is primitive. The proof comprises
the following cases:
1. The transition is idle, and 70 k at(l). As 70 k 1PO(S)? we conclude 70 ? In this case,
the only component of 71 that is different from 70 is 71 .T. Since the value of a primitive
formula does not depend on 7.T, and since 70 k P, we conclude 71 ? P This suffices to
show 71 ? 1P0(S).
2. The transition is idle, and 70 k after(l). The proof proceeds as above.
29
3.
4.
The transition is not idle, in which case it proceeds by SOS rule for skip above. That is,
= 1: skip, ?i-S = 1: done, and ? and ?i are otherwise identical except possibly for
?.T. Note that ? [= P, because ? [= at(l) and ? [= 1P0(S)- Primitive formulas do not
depend on the changed components. Hence ? [=P and, thus, ?i [=1P0(s) as desired.
70 [= ?(at(l) A after(l)). In this case, 5 cannot be responsible for any non-idle transitions,
and all transitions are thus idle. In particular, 71 [= ?(at(l)A after(l)), and hence 71 [=1P0(s)
vacuously.
Each of the other axioms and rules of Real-Time Proof Outline Logic is handled in a similar
manner, and thus we establish soundness. The subtle part of the proof is not checking these rules,
so those details are omitted here. The subtle part is the definition of the real-time execution model
that is explained above.
Acknowledgements
We are grateful to Limor Fix for extensive comments, and Georges Lauri for preliminary work
on the soundness proof.
References
[1] K. Apt and G. Plotkin. Countable nondeterminism and random assignment. j. ACM,
33(4):724--H767, 1986.
[2] B. Bloom and F. B. Schneider. Soundness of a real-time proof outline logic. In preparation.
[3] E. W. Dijkstra. Guarded commands, nondeterminacy, and formal derivation of programs.
CA CM, 18(8):453--H457, Aug 1975.
[4] M. Fischer. Re: where are you? Arpanet [electronic mall system], June 1985. Message to:
Leslie Lamport. Message No.: 8506252257.AA07636?YALE-BULLDOG.YALE.ARPA.
[5] V. Haase. Specification and compositional verification of real-time systems. IEEE Transactions
on software engineering, 12(1O):494--H501, Oct 1981.
[6] M. Hennessy. The Semantics of Programming Languages: An elementary introduction using
structured operational semantics. Wiley, 1990.
[7] C. A. R. Hoare. An axiomatic basis for computer programming. Comm. ACM, 12(1O):576--H580,
1969.
[8] J. Hooman. Specification and Compositional Verification of Real- Time Systems. PhD thesis,
Eindhoven University of Technology, May 1991.
[9] L. Lamport. Proving the correctness of multiprocess programs. IEEE Truns. on Software
Engineering, 3(2):125--H143, 1977.
[10] L Lamport. A fast mutual exclusion algorithm. ACM TOCS, 5(1):1--H11, Feb 1987.
30
[11] L. Lamport and F. B. Schneider. The "Hoare logic" of CSP and all that. ACM Trans. on
Programming Languages and Systems, 6(2):281--H296, 1984.
[12J 5. Owicki and D. Gries. An axiomatic proof technique for parallel programs I. Acta Informatica,
6(4):319--H340, 1981.
[13] G. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19,
Aarhus University, Computer Science Department, Denmark, 1981.
[14J A. Pnueli and E. Harel. Applications of temporal logic to the specification of real-time systems
(extended abstract). In M. Joseph, editor, Formal Techniques in Real-time and Fault-tolerant
Systems, pages 84--H98. Springer-Verlag, New York, 1988. LNCS Volume 331.
[15j F. B. Schneider. On concurrent programming. (in progress), Jan 1993.
[16] D. Scholefield and H. 5. M. Zedan. Weakest precondition semantics for time and concurrency.
Information Processing Letters, 42:301--H308, 1992.
[17] A. Shaw. Reasoning about time in higher-level language software. IEEE Trans. on Software
Engineering, 7:875--H889,1989.
[18j 5. Weber, B. Bloom, and G. Brown. Compiling Joy to silicon: A verified silicon compilation
scheme. In T. Knight and J. Savage, editors, Proceedings of the Advanced Research in VLSI
and Parallel Systems Conference, pages 79--H98. 1992.
31
