AXIOMATIC PROOF TECHNIQUES
+
FOR PARALLEL PROGRAMS
Susan Speer OwicYi
TR 75--H251
July 1975
Departrneflt of Computer
Cornell University
Ithaca, NY 14853
Science
+This research was partially supported by National Science
Foundation 9rant GJ-42512.
BIOGRAPHICAL SKITCH
Susan Speer Owicki was bom on June 25. 1947, in Pittsburgh.
Pennsylvania. In June, 1968, she received the Bachelor of Science degreo
in `latheratics from `.?ichigan State University, and in Januarv, 1970,
the ".?ster of Science degree in Computer Science fro? Cornell University.
Her professional experience includes several years of work as a
progra=er. She is a member of the Association for Computing `lachinery',
Pi 11' ?psilon mathematics honorary. and Phi Beta Xappa.
ii
ACKNOWLEDC'.?EWrS
am deeply indebted to Professor David Gries. my thesis advisor.
He was a constant source of encouragement and advice and taught me
a great deal about the organization and presentation of Information.
Thanks also go to Professors Juris flarti,.annis and James Braable
for serving on my special committee, I had many valuable discussions
of parallel processing with Professor Charles >ioore and of logic
with Professor Robert Constable and Marvin Solo?on.
The superb typing of this thesis is the work of `,!rs. Caroline
Marold who did much to improve its layout and appearance.
Finally, I am very grateful to ny husband Jack for his help and
support throughout this research.
iii
TAB'?E or CONTENTS
Page
Chapter 1. Introduction
1.1			Introduction
1.2			Outline of the Thesis			s
Chapter			2. Se?uentia1 Progra?s			7
2.1			The Scouential Progran6¶ing Language (SL)			7
2.2			The Deductive Serantics			a
2.3			The Interpretive ?odel			16
2.4			Consistency of the Deductivo Syate? and tho Interpreter			24
Chapter			3. parallel Prograns			26
3.1			The Gencral parallel Language (GPL)			27
?.2			The Interpretive o+".odel			30
3.3			The Deductive System			36
3.4			Consistency of the Deductive System and the Interpreter			45
?.5			Auxiliary Variables			52
3.6			?jtua1 Exclusion			63
Chapter			4. The Restricted parallel Language CRPL)			71
4.1			The Language			72
4.2			The Ir.terpretiv0 ?odcl			76
4.3			Axiora and Inference Rules			1
4.4			Consistency			93
iv
Page
Chapter 5.			Additional Properties o?.			Parallel Progra?.?s			95
5.1 ?Iutual Exclusion			95
5.1.1			C;PL			96
5.2.3			RPL			97
5.2 Rlocking			112
5.2.1			Prograa Blocking in CPL			113
5.2.2			t)cadlock in ?PL			122
5.2.3			Program Blocking in RPL			124
5.2.4			Auxiliary Variables			132
5.3 Termination			133
Chapter 6. Consistency and Completeness of the Deductive System 136
6.1			Consiatcncy			13?
6.2			Completcncss			149
6.2.1			The Program T			153
6.2.2			The Functions pre. post and I for T-			164
6.2.3			Assertion Functions			171
6.2.4			lmplications of the gelative Completeness Theore:			132
6.2.5			Proof of Lcrjsa 6.31			135
Chapter 7. Conclusions and Co;r?ents			192
Bibliography			196
v
C1iAPT?P I
I.\?RODUCTlON
1.1.Introduction.
The purpose of this thesis is to present an axiomatic metl?d for
Pr0vlnb certain properties of ;?arallel procracs. The most fundar?ntal
property is partial correctness: a pro?ram is partially correct if
it either co:putes the recuirc? result or fails to terminate. Total
correctness includes the requirement that the program terminates.
iloare [11o69i has developed axioms and inference rules for proving
the partial correctness of sequential progra?s written in an Aleol-like
syntax. and with certsin adaptations this deductive system can be
used to establish total correetness (.?anna [`1a74]). Its extension
to parallel programs (Iloare [Ilo72]) is the basis of the work in this
thesis.
The importance of correetnesa proofs for seq?iential pro?rams has
lon? been recogni?ed. The advocatea of structured programming have
argued that a well structured pro:ran should be casy to prove correct.
and that progracs should be written with a correctness proof in mind.
The need is even greater with parallel programs. If several processes
are executed in parallel. their results can depenJ on the unpredictable
order in which actions from different processes aro executej. For
exaaple the tvo siaple processes below can interact in six different
ways to produce four different values for y
proccas I: x:?l			process 2: x:'2
y:=x.l			y:=5?x
Such complexity greatly incr?aaes t?c probability that the progr??er
will makc niatakes. f.vcn worse, the ristacs ray not be detected
during program testing. since the particular intersetiona in which the
crrors arc visible esy not occur. It is inportant to structure parallel
programs in a way which elininates son of this con.p'?caity, and to
verify their correetness with proofs as well as by pro:ran testing.
A number of methods have been used in proofs for parallel prograns.
The most cor?on is reliance on infernal arguments -- a ria&y bus?ness
`given the complexity of parallel prograr.. int,sractions. "ore fornal
approaches have included application of Scott's mathenatical serantics
(Cadiou and Levy (Ca73]), Lipton's reduction nethod'(Li74b]. and Rosen's
Chureb-Rosser approach (Ro74]. The work which is ;ort directly relatol
to this thesis is based on Floyd's inductive assertion nethod (Fl671
for sequential programs. In this approach assertions ate attached
to the arcs of a flowehart, and a verification condition is developed
which guarantees that whenever control follows an arc the corresponding
assertion is true. This verification condition for sequential progra:s
is fairly simple, but for parallel prtgr??s it can be quite co--Hplex.
Asheroft and 4anna [As7l] express a parallel progran. as a nondetersin-
istic sequential protean. This gives a sinplc verification condition.
but the nunbee or assertions is an exponential function of the nunber
of progran. statements. In [As73]. Ashcroft uses a similar technique,
but argues that in practice the nunber of distinct assertions will not
be too large. Lauer [La731 and \.`ewton (\.`e74) attach assertions to
AXtO>ATlC PR(nF T?CIL\lqUES FOR PARALLEL PROGaA?'iS
Susan Speer Owicli Ph.r).
Cornell University 1975
This thesis presents an axionatic method for proving certain
correctness properties of parallel programs. Axioms and inference rules
for partial correctneas are given for two parallel program?ing languages:
the General Parallel Language and t?e Restricted Parallel Lancuage.
The General lan?uage is flexible enough to represeit most standard
s)?chronizers (e.g.. senap?ores. cvcnts), so that programs using these
s)?chroniters nay be verified using the GPL dcductlvc syatem. ilowever,
proofs for GPL programs are in gcner.'l quite complex. The Restricted
language reduces this complexity by requiring shared var?ables to be
protected by critical sections. so that only one process at a time
has access to then. This discipline does not significantly reduce the
power of the language. and it greatly simplifies the process of program
verification.
Although the axioms and inference rules are primarily intended for
proofs of partial correctness. there are a number of other Important
properties of parallel prograns. We give some practical techniques which
use Information obtained from a partial correetness proof to derive
other correetnesa properties, including program termination, mutual
exclusion. and freedom from deadlock. A number of e.?amples of such
proofs are given.
Finally. the axioms and Inference rules are shown to be consistent
and complete (in a special sense) with respect to an interpretive
model of parallel execution. Thus the deductive system gives an
accurate description of program execution and is powerful enough to
yield a proof of any true partial correctness foraula.
s
1.2.?tlineoftheThesis.
Chapter 2 is a review of hoare's axioms and inference rules for a
sequcitial proeranming language (SL). There are no new results here,
but many ot the corcepta needed for parallel prQ?rsms arc introduced
at this time. In particular, an interpretive model for sequcntial
execution is developed which is later exterjed to provide for parallel
coa?utations.
In Chapter 3 we move on to discuss parallel programs. The language
presented here is called the general parallel language (GPL) because
it is powerful esough to represent most of the primitive operations
su?gested for syncronizing parallel processes (e.g., events, Oij?stra's
seraphores). The deductive system and the model from Chapter 2 are
exterded t3 include parallel operations.
In Chapter 4 we consider a parallel programming language and
deductive system suggested ty Ijoare. This restricted parallel language
(flPL) is r?re hichly structurcd than the one given in Chapter 3, and
this greatly simplifics progra? proofs. In fact, the size of the
pro?fs again becomes linear in the size of the program. as it is for
se?jential programs. Once again the interpretive model defined in
Chapter 2 can be extended to cover the new language.
Chapter S discusses methods for proving other properties besides
partia cerreetness. Using both the deductive s"stcm and the interpre-
tive model of program exec?tion it is possible to derive easilv-verified
sufficient conditions fzr guaranteeing mutual exclusion, termination,
and safety from bloc?ing.
Chapter 6 considers the relationship bet'?een t:?? deduetive and
interpretive semantics presented in earlier chapters. The two nethods
are shown to be consistent for all' three lsngua:es, and the deductive
system for RPL is sho?? to be cor?lete with respect to the interpreter.
Finally. Chapter 7 sumrari:es our results and 5u???5t5 extensions
and areas for future work.
control Points in the flowchart of each parallel process. This nakcs
the number of assertions lincar in the size of the pro?ram. Unfortunately
the verification condition becomes more complicatej, hecat?se it is
necessary to check that the statements in one process do not invalidate
the assertions in another. This again introduces an exponential
complexity Into the proof process, but in practice all but a few of
the checks are trivial.
All of the inductive assertion methods deal with flowcharts but
they can be used as the basis of an axiomatic description of parallel
programming languages. Instead of having assertions attached to points
in a flowchart, they arc applied to program statements according to
a set of axioms and inference rules. Working with language statements
rather than flowcharts makes it easier to enforce restrictiona which
?ke programs intellectually manageable; it is even possible to
co:pletely eliminate the exponential factor mentioned above. The
axioms and inference rules provide a sound formal techniqum for proving
partial correctness, but they are also intuitive enough to be used
as the basis of reliable informal proofs. One of their main advantages
is that they give guidance in structuring programs in a way that makes
them easy to understand as well as to prove correct
Although the deductive system describcd above is designed for
pro?ing partial correctness, it can also be used to demonstrate other
important properties of parallel programs. For example, mutual
exclusion, the property that two or more proceasca cannot execute certain
statemanta at the sane time, can be proved using axiomatic techniq?wa
and certain theorems about program execution. Similarly. we can find
6,
practical, sufficient conditions, in terms of the axiona, for showing
that all processes cannot becore blocked (deadlocked). These results.
combined with `lanna's work, make it possible to prove program termination
in many cases.
There are two questions which naturally occur in considering an
axiomatic semantics for a prograrming language. The first is: do the
axioms and inference rules correctly describe the results of executing
a program? The second: are they powerful enough to make it possible
to prove all true atatemcnts about a progrLa? A partial answer can
be obtained by defining an interpretive model of program execution
and then asking the questions with respect to that model, The first
then becomes do the axioms and inference rules correctly describe
the results of executing a program under our model;? If they do, the
deductive syster. is said to be consistent with the model, It has been
proved that bare's sequential deductive system is consistent with
several models of program execution (Cook [Co7S], bare and Lauer
(1l074b]) The second question becomes: is th. deductive system
powerful enough to prove everything which is true about program execu-
tion in this model? If so, it is said to be complete with respect to
the model, Cook [Co7S] has recently proved that the sequential axioms
and inference rules are complete in a restricted sense which will
be discussed later, In this thesis, we will show that the axio:s
given for parallel processing are consistent and complete in Cook's
sonso for one model of parallel execution,
cal?ulus. For eaafl.p'.e the forula (xy<' =:?(x.y)I2 (x"??) expresses
the fact that if x < y ?ten the statement ::=(x?y)/2 begins.
x < y < z will be true wher. (and if) the statenert finishes.
Table 2.1 gives two axion. sehemas (Al ad A2) and four inference
rules (AO, A3-AS) for sequential proerans. The notation
pp			p
n
for inference rules means that P can be proved by proving each of
the P. and then applying the inference rule.
Al-AS correspond to the five kinds of progran statements. ?ule AO
requires some additional cor.?ent. The notation P ? Q means that it
is possible to prove q using P as an assumption. The deductive
syatea to be used in proving Q fro:n P is not g?ven: it could be
any systen. ?hich is valid for the data types and opcrations used in
the pro?rar?.T.ing language. For exanpie if the program?ing language
contails natural numbers and the operations and the deductive
systea could be based on Peano's axioms.
Figure 2.1 gives an example of a partial correctncss proof. The
proerso po?er cooputes z-x ir y > 0 (x and y arc integers). The
partial correctnesa condition is
(y>O) po?er
Lines 1-2 describe the statement labelled init 1, lines 3-4 describe
init 2, and lines 6-10 describe the loop. Finally. the effect of the
three statements together is &iven in line 11.
10
AO conscquc?ce			S(0')PP'0'?Q
(PI 5
Al assir,nmcnt			(pX) x:?L (PI
?hcrc prX rcprescnts he rcsult of suostitutin? c for each free
occurrence of x in P c.g. if P is (a>OV b-l) Pa.? is
(s'b>O v b-l)
A2 null
A3 composition
A4 alternation
AS itoration
(PI)5(P2),(P2)?2??3???n?5n??n?l?
(P 1 bc?in 5			5			cnd (P			1
I			n --H n.1
AEl?i(q)(P.??B)?52fQ)
(P)			if B thcn			else ?2 (Q)
(P A a) s1 (P)
tP: ??jle II do
A ,II
Table 2.1 A?ioms and lnfcrencc flules for sequential Pro:rars.
Cit1PTE? 2
sEQu?\.T1AL PROGRk'tS
Wc begin our studv of parallel programs by describing a simple
sequential language which will be the basis of our two parallel
languages. Th? sequential language is a fragment of Algol. ?or which
Noare has given a set of axioms and inference rules, ?c definc a
si:ple interpreter for this language and sletch a proof that It Is
COfl5i5tCflt wi',h Hoare's deductive system. Chapters 3 and 4 will extend
the language to include constructs for parallel programming.
?.a.Theae?uefltialProerammin?Lanrua?e(SL).
The programming language SL contains five statements:
1. assiancent o+- x:-E where x is a variable and E Is an expression
2.			null
3, compound -o+ be?in 5			`S			end
n
4.			alternation ,- if			0 then			else
5.			iteratIon -? while			0 do
where a is a Boolean expression and the 5. are statements.
?ote that there are no declaration statements; it is assumed that
all variables are globally defined, This simplifies the axioms and
the model of progr?i execution, but declarations could be included
without changIng any of the results, Sea Lauer (La7l] and Cool: ?o7S)
for the treataent of variable declarations.
?/ .%?..
?e also choose not to spccify the s)fltax of expressions. ?ost
of the time wC will USC the atandard Al?ol syntax for integer and
logical expressions. but the techniques apply equally well to other
data t)pes and operations.
At times it will be user?l to spC5l of the relation between a
stateoent and the atatemCnts it contains.
Let s be an SL statement.			____________________
2.1.uetinttjon.			The primarycorn?onents
of s are
1) none if s is an assignaent or null
2)			S1.S2s			if s is bc?in S			o+Sn end
__			1--H			2
3)			?l' ?2			if			s is if			8			then			else S
4)			s1 if			S			is while			8			do ?l
The propercon?onents of s are the primary components of S and their
proper components. The components of s are S itself and its
proper components.
2.2.Thefleducti?eSc?antics.
Hoare (IIo69] has dcveloped axioms and inference rules for proving
the partial correctneas of sequential programs. He uses the foraula
(P) S (Q) to represent the partial correctnesa of the program s with
respect to assertions P and Q . This fleans that if P is true of
the program variables before executing s and if s terminates, Q
will be true of the program variables after execution of 5 is
complete. P and Q must be formulas of the first-order predicate
13
fy>o)
powcr: be?in			:-1; tcmp:?x;
A :.xY?tCff.P)
loop: w!'ile tcmp>O ?o
v-t
(ter..p>o A z-x' flP)
?ult: bc?in z:-?c.z; tcmp:-tcnp-i cnd
(tcr..p>o A z?xX?tCr"P)
(tcn.p>O A z?xY?tCn.P A
end
?i:urc 2.2. An Infornal Partial Correctncss Proof.
14
Civen peCS') and post(5') for each coponent 5' of 5 it is
posssble to recenstflct a proof of (PI, 5 (Q) if pre(5') and post(5')
s.?tisfy certain requirements.
2.2.Definition: Let pre and post be functions which rap ce.-?onents
of 5 to assertions. Then pre and post are assertionfunctions for
(p) 5 (q) iff they obey the following restrictions for each coaponent
5' of 5
1)			P ?			pre(S) and post(s) ?			Q
2)			if			5' is x:"E , prc(5')			? poat(s,)?X
3)			if			5' is null, pre(5') ?			post(5')
4)			if			5' is bepin 5 5			end
a)			pre(5') ? pre(51) and			P0St(Sn) ? post(5')
b)			P0St(5j) ? prc(5i?l?			i-In?l
5)			if			5' is if B then 5			else
a)			pre(5') A B ? pre(51)			and pre(5') A 18 ? pre(52)
b)			post??l? ? post(5') and post(S2) ? post(S')
6)			if			5' is while ? do
a)			pre(5') A 8 ? pre(51)
b)			post(s1) ? pre(5')
c)			preCs') A `8 ? poat(5')
A proof of (P) 5 (Q) and a p?ir of assertion functions for (P) 5 (Q)
are very closely related. Civen eit?er one, the other can be derived
as shown in the next two theorera. In ieneral, we will first give
a partial correctness proof, then derive assertion fur.ctions fro? it.
11
po?er: be?in initl: :::?l; init2: tc¶.p:.)r;
loop: while ter.p>O ?o
ault: bc?in up:: ::?x.::;
downteop: ter..p:.tcmp?l
end
end
1.			fy>0 A 1-1) :::-l (y>o A :?l)			Al
2.			(y?o) z:-l (y>o A -1)			1, AO, using y>O ? (v?O A I-I)
3. (y>o A ::?l A y?y) temp:-y (y?O A --1 A tenp?y) Al
4.			(y>o A -1) tcrnp:-y (tc?p>O A ??xY?tCrflP)			3, AO
S. fte?.p-l>O A ?*?"?Y?(tC???l)) z:-x.z (tci.p-l>O A z?x? (tcrnp-l)1 Al
6. (te?p>o A ???Y?temp A tcw.p>o) ::-x.:: (tcn.p-l>O A ???Y?Ct?n.??l)? S, AO
7.			(te?.p?l>O A ??Y?(tC0??l)) tcn.p:-tcr?p-l (te?p>O A ???Y?tCtfl?)			Al
8. (t?opo A ,-??Y?te?p A tcn.p>O) nult: be:in ?:-x,,z; tcmp:-tcmp-l end
?temp>O A ::`xY?tC1flP)			6, 7. A3
9.			_____ tcnp>O do mult
fteop>O A ??Y?tC??) loop: whilc
(temp>o A ::??X?tcmp A `(te?p>O))
(te?p>o A ???Y?t???) loop
10.
11. (y>o) power
8, A?
?, AO
2, 4 10, A3
?iguro 2.1. A Fornal Partial Correctnesa Proof.
ffi.?.
12
c?urse this is a very tedious proof of a si?ple result -o+ much
like an algebraic proof that (a'b)(a?b) a 2ab b when every
use of the cor.?utative and distributive laws is presented. Figure 2.2
contains a more informal version of the sare proof -- assertions
enclosed in braces () are interspersed with the progras, while some of
the proof steps arc combined or omitted. `.!oat of our proofs will be
presented in this style. hhen proving progrars correct in a practical
manner, we use the formal methods only in the difficult parts and
use less formal techniques on the simple parts. The most difficult
part of sequential programs is iterative loops. and it is usually
worthwhile to carefully apply inference rule AS to each while statement.
On the other hand, assignment statements and be?in ... end blocks
are relatively simple and can often be treated informally.
In Figure 2.2 the assertion P (temp>O A =?y?temp? appears
iuat before atate9.ent mult. This corresponds to the fact that P `mast
hold whenever mult is ready to be executed in a corputation which
atarta with y 5 0 . P can be called a pre-candi-ion of mult, and
Q (temp>O A ?????t??P) is a post-condition. A proof of (P) 5
gives at least one pre- and post-condit?on for each component of 5
For example, line 3 in the proof of (y>O) power (?.??) gives the
pre- and post-conditions for mult cited above. Lines 9 and 10 give
two post-conditions for loop, namely (teapsO A ??y?temp A ,(temp>O))
and
At times it will be useful to single out a particular pre. (or
post-) condition of a statement 5 and call it pre(S) (or post(S)).
17
section usca an operational approach, in which the effect of a program
is ?eacri?cd by gi;iflg an interpreter for the prograT.a.ing lancuage.
This interprotive eodcl is consistcnt with the dcducti?'e systcm. It
will be used extensively in Chapter 5 whcn Jiscussing nutual cxclusion
and blocking, which cannot be cxpreaaeJ directly in teres of partial
correctness.
The interpreter for an SL progran consists of a set of states
3rd a state-to-state transition function. A program state has two
coaponents -- a control, which gives the next instruction to be
exccuted, and a variable state which gives the current value of each
vari-ble.
2.5.Definition A proeramstate for a program S ia an ordered
pair. a"(c,v) in which
1) the variahestate v is a function from variable n&trea of S
to valucs.
2) the controlstate c is a tree in which every node is labelled
with a atateflent fro? 5 in such a way that if 1 is a
corporen of , and ?i and both appear in c , ?l is
a descendant of 5, . (flere each node is considered a descen-
dant of itself.)
The variable state v is a function defined on all program
variables, although the value returned for an uninitialied variable
`s not specified. The notation L(si will be used for the value of
expression E in state s"(c,v) . Thus. if v assigns 0 to a
6,
18
For an assertion P we say P is trje in a if
P[s]?true
The control state for a sequential program is a de:?nerate tree
in which each no?e has zero or one sons. The single leaf is t?e
next statenent to be executed. n order to sinplify notat?on we will
assign a unique label to each stateTent and use the staterent and its
label interchangeably. Fi?ure 2.3 conta?na exarples of states for
the program power of Figure 2.1. Note that the derin?tioi. of control
state guarantees that no staterrent appears more than once in the tree
For 5 is a conponent of itself, and i- 5 appears at nodcs m and
n m must be a descendant of n and vice versa. So ti?n
The execution of a atateent can affect both cenponents 0'
the program state. The control is e?dified by rep?acing a leaf by a
(possibly eapty) tree.
2.6?e'.inition: If t and t' are trees, and n a leaf in t
eplace(t,n,t') is the tree obtained by replacing n by t, in t
Examole:			t -			t' -			e
g			f
dffib
replace(t,d,t?)
ffib
fe
replace(t,c,r) -			a
d?Thb
where r is the eapty tree.
IS
The assertion functions are useful in proving the consistency of the
deductive syste? and in discusaing vario?s prooortics of parallel
programs in Chapter 5. The key point is that pre(S?) must hold whenever
5 is ready to execute and post(S?) must hold whenever S. is
finished.
2.3.Theorem: If pre and post are assertion functions for (P) 5
it is possible to prove (pre(S?)) 5 (post(S')) for each component
5' of 5
Proof:			By induction on the structure			of			5' . Two cases will be
:iven; the rest are similar.
Caso 1:			5' is x:-E
1.			(post(s,)X?) 5' fpost(S'))			Al
2.			(pre(S')) 5' (post(S'))			1			AO and requirement 2 for
pro and post
Caao 2: 5' is wh:le B do
1.			(pre(s1)) Sj (post(s1))			induction
2.			(pro(S')AB) ?l (pre(5'))			1, AO. requi--H.ements 6a, 6b
3.			(preCs')) 5' (pre(5') AiB)			2, AS
-A.			(pre(S')) 5' (poat(5'))			3. AO, and requirement 6c
2.4Theores.: 1 there is a proof of (P) 5 (Q)			there are assertion
functions pre and post for (I,) 5 (Q)
Proof: Pro and post can be obtained from the proof; they will be
defined in such a way that (preCs')) 5' (post(5')) is a line in the
16
proof. for tach component 5' of 5 . Since the proof may contain eore
than one line which refers to 5' we a?st specif,v which line is chosen
to give prc(S') and poat(S') e elirjnate all lines w?ich do not
contribute to the proof of (P) 5 (Q) (for example. line 1 in the
proof of (x?) ?:?(x.y)I2 (x<zy') below).
1.			((x'y)/2>O) z:=(x.y)/2 (:>O)			Al
2.			(a<(x.y)/2v) z:-(x.y)?2 (x<zy<)			Al
3.			(x?) z:-(x?y)?2 (x<z?)			2. AO
In this reduced proof there will be one line which refers to 5 and
uses one of rules Al to AS. It is fro.? this line that we choose
preCS') and post(5'). Any other lines with the form (P') 5' (Q')
must be derived from (preCs')) 5' (poat(S')) by one or more
applications of AD. Thus P' ? preCs') and postCS') ?
Now we must verify that pre and post satisfy Definition 2.2. Two
representative cases will be considered. If 5 is x:-E
fprc(S')) x:.E (post(5')) is an application of Al. Thus pre(S?) -
post(S')E and 1 is satisfied. If 5' is w?ile B do
(pre(S')) 5 (postCS')) is an application of AS. This implies that
post(5') - (preCS') A `B) satisfying 6c, and that (preCS')AB) 51
(preCs')) has been proved. Since (pre(S')AB) ?l (preCS')) is a
lina in the proof. preCS') A B ? pre(S1) and post(S1) ? pre(S?)
satisfying 6s and 6b.
2.3.TheInterpretive`odel.
In the last section. the se=antics of the Algol fragment SL was
defined by axioms and inference rules at a very abstract level. This
ard
c			replace(c,S.?)			if 5 is assign:s?nt or null (			is the copty tree)
rePlacetc.S.tSl) if 5 is be?in 5			o+S? cn
5,
IS
- repl?ce(c,55 ) j; 5 is if 13 tber c el',e ? a
1			--H			--H			.			nd Il[s)-truc
- replace(c.5,5,) if 5 is if 13 then 5 else 5 and B[s)-false
--H			--H			1--H2
- replsce(c 5 Sj)			if			5			is ??ile			B			do			?l			and			B[s)-true
- replaceCc.S.?)			if			5			is while			B			Lo			?l			and			B[s)-false
rx.-??'.e: See Figure 2.3.
We have not described the effect of next if an arith.?tic or
Boolean expression can't be evalustcj for sore reason (for example.
it invol"ts division by zero or an `ninitialized variable). There
arc two ?ays in whien the interpreter could respond in such a
situation. O.?e is to stop execution; the other is to choose some
arbitr:iry v?lue for the expression, for exar.?le, 0 for numeric
expressio?s and tsue for Boolean expressions. In the interpreter we
will `0110w the second alternative. For exarple. the effect of
execu'.in? the st?terent x:-4/O is to assign 0 to x - The axioms
ard nferer.ce rjles can be madc to reflect this choice by assi?ning
he s??e value as the interpreter to expressions which arc normally
consi?cre unJerined. For the stztcrcnt x:-4l0 Al can be a?plied
0 cive a proof of (4,0.4/0) x:-4/0 (x-4/O) or (true) x:-4/O (x-O)
The deductive system used in thc rule of consequence (AO) must be
22
c?oaen in a wav, which is consistent `?ith the assinent of values to
expressiors like x/rj but this should ca'jse no ?ro??ens.
Notc that (tru?) s:=4?0 (?=0: is also consistent with an
iaplenentstion in which execution stops on encountering the illegal
diviajon, si?cc in that case the statement does not tertinate, and
t'P) S (Q) is true fer any P and Q
For seouential programs there is only one order in wh?ch staterents
can be executed, but for paral lcl proraas this is no longer the
case. In order to provide a baais for the parallel interpreter, we
define a "computation', which recorla th order of ataterent execution,
and then define some useful properties of computations.
2?9.Oefinition: A coT.?1tatior. a for program S `Deginning with
variable state			is a secuence of statenents			... S			such
v0			?l ?2			n
that if ?o (S,v0) the seoucoce of states 5. next(s -1' ? i? is
defined, i,e. , S is a leaf in 5i-i If a - S1 .. S is a
I			0
computation, let value(s0,u) = 5n If ? is an assertion we say P
is trueaftern iff P[vaiue(s0,e)]=true
Lamnie: From Figure 2.3, o (poer, initl, init2, loop, mult, up-,
dowoteip, loop) is a cor?utation for po'?er beginning with state v0
Value(s0,a) - a? , ,-[value(s0,e)] - 2 , and ?-?? is true after a
2.10.lefinition: Staten?nt S it reauytuexL.cu'a ?-fter computation
m iff S is a leaf in the control of value(s0,o)
F:xa.?oles; From Figure 2,3, initi is ready to execute after a --H (power)
and init2 il ready to execute after a - (poer, initl).
> > ?
o ?
CM `a
? g E
o+ a			a
c 0 0 0
in
oC?
6/ %?o+?.
20
Tr.e vart?ble ?tatc can be noJif??d by an assignment state:nent. The
nc? variable state will be the sane as thc old except at the variable
?hich recei?cd a
2.7.flcfinition: If v is a variable state function and E is an
expression, v<aJE> is a new variable state f?nction defined by
x[v<ai>] - x(v] if x 6 a
- E(v] if x a
The effect of each type of statement is defined by the state
transition function `next". An assignnent statement chanres both the
control and the variable state; all othera change only the control.
Note that if S is a compound statement (be?in . end, if or while),
nextCs.S) describes the effect of startin'			S in state 5 rather
than the effect of a coeplete execution of			S
2.a.riefinition. The state transition function
next: (program states) X(stateoents)			(program states)
is given by
next(Cc,v).S) - Cc',v')			if S is a leaf in c
- undefined			otherwise
v			- v<xjc>			if S is x:-E
- v			otherwise
where
25
Proof: The pro3 uses ind'?ction on the length of a If a is
e=pty 1) is satisfied beca?se P is true for and P ? prc?S)
2) does not app?'...
tor a a'T preC?) is true ater a by in?uetion. Proving
t?at `,) ard 2) arc satisficj for a' is a straightforward but teJio?s
applic3tion a t?e definition or assertion functions. The details
are given in CI:apter 6.
.10.L.,rojjar?. If ?`P? 5 can be proved, it is true for the
interpreter.
Proof: By Thcortr.. 2.4. there are assertion functions pre and post for
IP) 5 (Q) Ne? suppose a executes 5 from state 5o with
true. Thcn by the last theorem, post(S)(valuo(50.a)) true
and qr?value(s0.a)) true since post(S) ? Q . So (P) 5 (?) is
true for the interpreter.
This inishes our review of sequential programs. In the next
c??pter the axioza and the mo?el are extended to parallel programs.
CIlA?TLP 3
PA??LLL P:?oG:?'ts
In tha ch?pt?r we introuce par?1lel prograns by exte?Aing the
l?n?ual:e of Chapter 2. Two ncw st.dtt?ents Will be added co?e?ir.
cound to in?tiate prallel exccj'tion, and a synchroniat?ofl state=ent
calleJ a?ait to coorJjnatu proceast's executir.g in parallel. The await
atateeent is very flexible in fact it ia too ?eneral to be
ispl?r.ented in an efficient wa:/. It is included here because it can
be used to represcnt ¶.any standard synchronizing prir.?t?ves, such 35
es'cnta and s??aphorea. Thus, the proof techniques for GPL can be
applied to prograns which use these s>mchronlzers.
Thc lanruage in this ch?pter is relatively priritive ard provides
only li.:ited facilities for strjcturin,, the interactions of processes
using shared variables, ?e will see that the axie.?s for the parallel
and synchroni?ation st.?te.ments are easy to understand; they state
quite easily when we can knew that parallel processes don?t "interfere'
With each other Put proofs usia',,' the,, Will be difficult because of
the esporential nurber of chec'?s that ray be necessary to satisfy
this noninterference criterion. In C:?apter 4' we present another
lanuage in which the usc of shared variables is closely rezulated;
this nales proofs of prograr'. correctacis r,jch siapler. `lowever, no
suCn larguage is yet in usc (see Irinch flansen [Br74)) so the results
in this chapter are nore rea?ily applicable to prograns written in the
lanuages which are currently available.
26
-.?L.Lcr11.1t1o.?: If a is a computation for S and S' is a
c??poneflt of S a finishes S' iff
1) s' is an assicnnent or null stateaent, and S. is the last
statenent in a , or
2) s is while B do S1 S is the last stateaent in a , and
3 is false after a , or
3) S is berin S ;Sn e?d and a finishes S , or
) S' is if 3 then S1?else S2 and a finishes S1 or
Esan-ole: Fro? Fifure 2.3f, a - (power, initi, init2, loop, body,
up:, downterp) finishes downtemp and body.
2.12.Definition; a executes S iff a is a computation for S
which finishes S
cxa--H?le: Fror. Figure 2,3i, a - (power, initi, init2, loop. body,
up:. downte?p. loop) executes power.
Note that for a ?iven initial state 5o there is at most one compu-
tation which eAccutes S This is not true for parallel programs.
If s contains an infinite loop. no computation executes S
2.13.Definition: exicute(a,S) --H value(s,a) if S is ready to
execute in a snd a is a computation which executes S from state a
If s is not ready to execute in a , or no such a exists.
execu:e(s.S) is ui,defined.
This completes the description of the interpreter for sequential
Pro:ra;as. In Chapter 3 it will be extended to include parallel programs.
y
24
2.4.Conr,:ste?cvert'.:cIJeJL'ct.vevarer.antheInterreter.
Sections 2.2 and 2.3 specify tre serantics of the language SL in
two diff?r?nt ways. In this icetiun, we state a theorem to the effect
thit the two n?thods are consiste.?t. To keep the reader froo
gettin,, bo,ged dot? in details, we only sketch the proof here, delaying
a co?..plete presentation until Chapter 6. Ilopefully, both nethods
corrcspond well enough with the reader's intuitive idea of program
execution that he is willing to believe they are not contradictory.
In order to show that the deductive syste.' and the interpretive
?odel are consistent, we must sho? that (P) s ?Q? can only be proved
when it Is true for the interpreter.
2.14.I)e?initinn: (P) s (Q) is truefortheinteflreter iff an7
coaputation 0 which executes 5 from state 5o with P(s0] - true
has Q(value(50.e)i true.
order to show that a proof of (P) 5 (Q) irplies that (P) 5 (Q)
is true in the model, we first derive a stronger result using assertion
functions.
2.15.Thcorcm: If pre and post are assertion functions for (P) 5 (Q)
5' is a component of 5 , and a is a computation for 5 from a
state a0 with P[a0] true, then
1) if 5' is ready to execute after a , pre(S') is true after a
2) if a finishes 5' . post(5') is true after a
29
P(sen.): s?ait sen)O then scn.:=sern-l
?`(se:i.): await true th?n sen:?stn?1
Lipton (Li7?a] describes a n?rnbcr or ecnerali-ations or semathores;
311 can be ir?'e:'ented usine await statenents.
l? [Di6Sb). Di?kstra :ives a s1i?htly different definition of
the seraphora operations.
P?(sem): se?:=sern-l if sercO then the process is suspcnded
on 3 ojeue associated with sem.
V?(sec): sen:?se=.l if scn<O awaken one of the processes on
the sc:t?aphore?s queue.
A possible irp1er.e.?ration or these operations uses a Boolean array
waitins. wi?h one elenent for each process. Initially wsiting[i]?false
and waitin?[i].-true pr??ess i is on the queue.
P?(se--H): await true th?n
be?in ser.:?ser-l
if serAo thcn waiting(this process] -true
enj
a'?ir ,?aitine[this process) then;
V?(se:): await true then
beein sem:-sea.l
if ae?O then
30
c?ir coose i suc? t?at wa?tinr[i]-trje;
`aitine(iJ :?false;
ent.
end
The operat?ons P and V are an abstraction of P and V
There arc some cases in hic: th ef?eets of the two are not idertical
but for thc properties discussed in this thesis -- partial correetness
mutual exclusion, and Icadlock the diffcrenccs are irrelevant. See
Lipton ([Li74a]. Chapter 3) for a co?parison or the t?o o+k-inds of
sceaphore operations.
in order tn provc the eorrcctncss of a prograr. o+?hieh us?s
sesaphores, the scraphore operations can be replaced by the correspondin?
a??it statc?ncnts. The rcsult is an eqJ?valent CPL prograr.. which can
be proved correct using the retauds presented in this chapter. There
arc a num'jer of other synchroniration priritives which can Ire
modelled usinL' asit, and the sare technique can be Saplied to
prograes which contain such pr?mitives. it is this flexibility which
prompted the n.,ee "general parallel lan?'uage".
.L.fhcInter?r':tsve0051.
The model of sequcntial pro ran. execution defined in Section 2.3
will now he cxtendej to include paralloliar. Pecall that the inter-
preter had two components: a pro'ran state consisting of a control
and a variable state, and a state transition function "next". The
program state is defined exactly as before, althou,,h execution of a
?.I.The?encra?ParaiieiLaflcus?(?.L)
The language of this chapter is the sequential lan?uage of
Chapter 2 plus two statements for parallel processing:
parallel execution			coberin S ?/			//Sn ce?nd
synchroni.-ation -- await B then
where 5, is a statement and B a Boolcan expression. The frirat
state,ent initiates parallel execution of ?l . h?cn 311 of the
5. have finished, the parallel statement terminates and execution can
proceed to the next statement. There are no restrictions on the way
in which parallel execution is implement?'d; in particular nothing is
asauned about the relative speeds of different 5. . The primary
conponents of a cobecin ... coend statement are called parallel
processes.
3.1. Definit
________________ Components T1 and T2 of 5 are in diffcrent
processes iff 5 contains a stateaent cohe?in 5?/?. `1,5n coend
with T1 and T2 cosponents of different S? . Otherwise. T1 and T2
are in the sIreprocess.
Note that according to this definition, the cobecin statement itself
is in the sIre process as each of its co:nponents. A program can be
visualized sa one large process which may contain a number of
difterent subprocesacs. Since parallel statenents can be nested. any
process may contain subproceasea.
The second new statement, await B then 5 is designed to
provide synchroni:ation between parallel processes. and it can only
r
23
pp?ar inside a colc?in stat'-?nt. i is a 5nolean expression. and S
is a sen?ential statenent hi?h does rot contain a cobesin or another
a?ait. ?hen proccsa atter.,?ts to execute a synebronitation staterent
it ia delayed until tne condition 3 is true. Then the statenent S
is executed as an indivisible e;)?ration. If t?o or nore processes
arc waiting for the sane eond?tinn 3 any one of then nay be allowed
to proceed when 3 becoses true. In acne applications it is necessary
to specify the order in which waiting processes are sc.w.ed.J?.ed. for
example on a first-come first-served basis. Por the problens discussed
in this thesis, however, any scheduling rule at all is acceptable.
The await statement can be used to turn any sequential atate?ent
into an indivisible operation. This would be quite difficult to
implement. and it is not suggested that the await staterent is a
desirable language feature. Instead It is presented because it can
be used to represent a nu?ber of standard synchronlzing prioitivea.
such as Dij?stra'a senaphore operations (Ui6'a).
A senaphore is an integer var?able which can only be acceaxed
by two operations, P and V
PCsem): if sem>O sem:?aeo-l otherwise the process is
suspended until sensO
V(aem): sem:?aen?l
The P and V operations are Indivisible. They can be represented
by synchronization statements as follows.
33
si
0 ?			u
v:			v:
v:;
00
34
it is not. T?c soutien iCt proirars so t.?at i:?? ass?.ption
of indivisihility is reaionable one. For exarple, if exeiutin two
Jctions sir.ultaneo?sly is tic ia.?e as exicutin," one and ten tIe otler,
it is res?onable to treat then. as indivisible. This certainly is the
case if the actions do not .?a'.'e an? variables in coron. If they do,
sone care is rc,'ulred.
3.S.!)efinitinn: TIe variable x is shared in cc".er-. S,//. ?/?S?
coend if it is referenc?d in t'?o or T.?ore of the S. and chin:ed
__________			I
appears on the left aide of an assigninent) in at least one
of thc?.
It is refer?nces to shared vari?ilcs `hich cause problens whcn actions
are treatea as in?s?ia?ble. Lut for actions `hieb r?ke at rest one
reference to a shared variable t"e assuoption of indivisibi it'1 is
reasonable. If two such actions are executed sicultaneously. one
of then' nust Saki the first access to the shared variable. The e?feet
in parallel will be the sane as if this action was executed first
and followed by the other action.
In the interpreter, three kinds of actions are assuted to be
indivisible:
I) an assignment atatirent
2) evaluating the ?oulcan expression in an if or while
a) synchrenitation statement.
3 is no proble¶., since a s1nchroni?ation statement ii interded to be
indivisible in parallel esecution. I and 2 are 3ustified if each
aaai,'r,n.ent and each if or w\Nil' condition contains at ?ost one reterence
31
parallel proeran. unlike a sequential pro?ram. can lead to a control
tree with more than one leaf. The function `next must be extended
to handle parallel and swnd?roni?ation statements. next(s,S) ia
defined for all statements S which are ready to execute in a
3.2.Defin??u,,. A statetent S ia current in the proeram state
s-(c,v) iff S ia a leaf in c
3.3Definition: S is readvtoexecute in state a?(c.v) iff S is
c?rrent ir. a and if S is await B then S1 B[sj?truo.
Xote that for sequential prograns thia reduces to the previous
definition of "ready to execute'.
3.4.Definition: The state transition function
next: (program statea)X(statementa) (progran states)
is given by.
next(Cc.v),S) undefined if s is not ready to execute in (c,v)
- execute(Cc',v).S1) if S is await B then S1 where
replace(c.S.S1) (see Definition 2.13)
--H (c?.'.) if S is coberin S1//.. coend, where
c' is the tree obtained by deleting S in c
and adding ?? as sons of S'a father, if
any. and otherwise as roots of unconnected trees.
- Cc v') of Definition 2.8 if S is asai?nment,
null, sequence, if. or while.
32
The de?nition naxt((c.v). aait B thtr. S1) - execute((c v)`5l?
retle?ts thc assur.ption that executing?an a?ait ataterent is an
indivisiblc op?ration.
Figura 3.1 contains examples of t?e application of next. Note
that in 3.lb the control state is actually a forest rather than a tree.
In this model parallel execution ia si:,.ulated by nondeterainism.
lnstaad of executing the processea in cobesin ? //Sn coend
simultaneously it perforra one action at a time. choosing nondeter
ministically which process to work on ne?t. This reans that in the
program
newx: be?in x:'O
cohe?in A: x:-x?l /1 B: x:-x-l coerd
end
either A or ti is cxecuted f?rst they cannot overlap. TIja use
of nondetereiniam is standard in models of parallel execution, but it
requires some justification. For example. the program above, executed
by the interpreter. must finish with x"O . A true parallel imple-
mentation might finiah with x-l if the actions took place as
follows:
1.			A			evaluatea			x.l
2.			?			evaluatea			x-l
3.			a			stores -l			in			x
4.			A			stores 1			in			x
The discrepancy arises from the fact that the assignment x:-x.l is
treated as an indivisible operation by the interpreter, when in fact
AO cor.scq?cr.?e
37
5. (??`, ?			0 ? 0
ip;. s (Q)
Al assi?flr..cflt			(P?) .?:--L jP)
A r:jll
A3 con.?osition
A4 a1tcri.?t1On
AS iteratiom
A6 s>?c1.ror.iation
A? parallel
t'P1)S1(P2' .(P2)?2(?3?P?)S?(P??1)
b('tin S			nd
(PA B) S1 (Q			(PA `? S2 (Oj
(P) i 13 thcn S1 clsc S2 (Q)
`.P A 3) S `?.`
(P)			hi			3 d? 5 (P A `13)
A 3) 5
(P) ??ait B t?cr. S (Q)
(P ) S (1 )			(P ) 5 (Q )
In n			n
(P1 A.. A P ) ?c?'n ?l??. /AS? cocnJ
(Q1 A.. A
provided (P1) ?l (Q1).. (P?) 5? (?) ?re
intcrr%rence- free
Tab1e 3.1. Axic,ms and Interence ?ulea for CPL.
ocs nt r.?J?fy any s?arcJ vj?i.bi??. T,is ra,:es t?e proccsscs cots-
p'?tcly ir'jc??ndc.?t. it ir, ,oo ?rc.s,,' ? rcn??'rctsent. A ore serul
r'?triction i? ti?:it t.;C ..ts?crti'r: ic in prr'vifl; S (1.? arc
I			I I
in':?rsant as stat?oonts fror. other pro?esses are execuzt:? For
tic ns?ertion ?.x?.' I.'. 5,- re.-'.-a?ns true throughout t.'Ie
eseC-.it?on or x:?x'l in 5 ,r.c ,nvarlance or an assertion P o'cr
a sratcr..ent S `s. e.<pre?sed by ne forrula.
(P.'?re(S)) 5 (P?, o+??erc pre(?i) is a prc-co.?dition of 5
hi. in'J.?r1.-Lno? rc.?nini, is tic- b?sis ot the irtarrcrer.ce-rrce criterion.
We will first deine interfer?nne-free in terra of asaerti3n functions
and then relate it to proran. proots.
3.11.Ic-finition; Suppose 5- is a C.PL progran. and pre and post
arc functions which rap corponents of 5 to assertions. The' are
assertionfunctions for (?) 5 (Q) they obey the following
restrictions for eseb conponent 5' 0= 5
l)-6)			Sac ss liefinition 2.2
7)			if			5' is awant ? thcn
a)			precS') A ? pre(S1)
b)			post(S1) ? poat(S' )
S)			if			5' is coherin 5i1,? ?15n coend
a) prc(S') ? i1? pre(S?)
A			P05t(Si) ? post(S')
i?l
3S
to a sh?red variable. ?e will only ?iscuss programs which satisfy
these resuirerents for such prograes parallel and nondeteroinistic
execution :i?e the same results.
Because of the nondeterainism in the interpreter, a parallel
pr?rrmn can be executed in a nu?.ber of different ways. A conputation
gives one pessible order in which stateoents can be executed. Coaputa-
tions and their properties are defined in much the same way as in
Chapter 2.
3.6.Definition: A cornutation for program S beginning with
variable state v0 is a sequence of statements ? ? such that
if ?o (S,v0) . the sequence of states s? - next(si-i'Si)
n is defined, l.e., 5. is ready to execute after 5 5
I			n
In this c?ae value(ao.a)?sn and an assertion P is tfleaftera
iff P!'alueca0.e))?true.
3.?.Definition:			If			a is a computation for 5 , and 5' is a
co?ponent of 5			a			finishes 5' iff
1) 5, is an assign, null, or await statement, and 5' is the last
staterent of a from the same process as 5' , or
2)			5' is while B do 5j , and 5'			is the last statement in a
from the sane process as 5' , and			B[value(s0,a)]-falae , or
3)			5' is heein`5n end and a finishes 5 , or
A)			5' is if B then 51use ?2 and a finishes ?l or			, or
S)			5' is cobeein S??????/?S? coend , and a finishes all the
1<i <n
36
3.b.)e?initinn: a cx?c?tCs S iff a is a corputation for S
which finishes
At tirus it will bc uiefjl to ipek of a state?ent bein "in
e?czutlon' in a conputation.
?.`j.efinitton: S is ine?rcLti?n in a co.?pJtation a iff a
component of S is cLrrent after a . Thus. a stateent is n
exec?tion fran the time it is current until it has finished.
Finally, we review tne ?e,inition of o+`true in t',.e interpreter".
which is the same for SL and GIL.
3.10.Definition: (I) s (Q) is truefortheinter?reter ff any
conputation a which executes S fror,, state 5o with P[s0]?true
has Q[value(s0,a)]?true
3.3.TheDeductiveSyster.
Table 3.1 Lives the axioms and inference rules for GIL progra?.s.
They assume that the progr?m obeys the restrictions on shared variables
discussed in the last section. AO.AS are identical to the rules for
sequential programs. A6, the inference rule for synchronization
statements, is quite atraightfor?ard. ll?t rule 7 for parallel state-
ments requires sane discussion. It basically states that the effect
of executing ?l ?n in parallel is the combined effect of
executing cach of the 5 by itielf. provided that the processes do
not interfere with each other. Of course the key to this state--H,.ent
is a definition of "interfere". One possibility is to require that
S)			c) pre and post are in?e?fe';?;???-fn& for S			S			i.e.
n
if T is a corponent of S. and T ia an assienrent
or a?3it in S. . (i6i) and neither T nor T is:'
proper co=ponent of an a?ait stateoent. then
(pre(T).?re(T?)i T' tpre(T)?.
(post(T)Apre(T?)) T (post(T))
can be proved.
- The interference-free te?t in Sc guarantees that the assertions on Sj
--H.e=ain true as atater-ents in S. are c?ecuteJ. It is only necessary
to check for invariance over asaigneent and s?rnchronization staterents.
sine all changes in data valucs take?place In such atateaenta. Proper
coeponents of await statenents arc not includcd in the tests because
await staterents are indiviaible operations. and the state of
variables at intereediste stages is not inportant.
The interference-free criterion for proofs. as reouircd in A7
is definel in terns of assertion functions.
3,12.fleinition: The formulas (P1) S1 (? ) ??n? ?n ??n? arc
?.???rference-free iff there are assertion functions prek and poatk
for ??k? Sk (?k) such that if T is a corponent of Si and T is
an assienoent or await statement in 5. Ci$j) and neither T nor
is a proper component of an await statement, then
(pre?(T)Apre?(T?)) T' (pre1(T))
A
49
(post?(T)APre?(T?)) T' post5CT))
ban be proved.
Just as 5n Chapter 2, a pre?rar. proor and a tair or assertion
functions arc closely related.
3.13.Tiecren: If pre and pea, are assertion functiona for (P) 5 (Q)
it ja possible to prove (pre(S')i 5' ipost(5')' for each co'ponent
5' of 5
Proof: Same as Theorca 2.3.
3.14.Theoren: If there is a proof of (P) 5 (q) there are assertion
functions pro and post for fp) 5 (Q)
Preof: Sane as Theoren: 2.4.
I:>:snples: Figure 3.2 contains a p?rtia1 correctness proof for a very
simple pro,"rao. The fact that (x--n,'x?2) 51 (x"lVx"3) and
(x?Ovx-I) 52 (x=2,'x"3) are interference-free can be verified by four
tests.
1. (preCsl)Apre(S2)) 52 (pre(S1)?
i.e., ((x-OVx.2)A(s-oVx?l)? 52 (x?GVx-2) which can be derived from
(x-O) x:?x.2 (x"2) usin? A6 and AO.
2. (post(51)Apre(52)) 52 (post(5l))
`a. (pre(52)AproCSl)) 51 (pre(S2)l
4. (post(52)Apre(51)) 51 (post(52))
Note that pro(s) ? (pre(Sl)ApreCS2)) and (post(5l)Apost(52)) F post(s)
S: cobeeifl
(??o ? N=2?
S': ?ai true the, x:-?.1
(x-1 ?` x?3)
`I
?x=O V x'1)
S2: a??1t true then x:-x?2
?`x?2 V x=3)
41
?i??re 3 2. A Partial Correctn?s5 Proot of a P?ra11cl Progran.
42
c.\a?,S?e of sn??.r.f r.3rc rcaIis??c p-.oblcr., tt?siier t:?e
rrn¶ra Fir.?p3s in I?ure .3. a essest4aly tar. as a prt?ra
whi,c co,rt?tr?s.s as pr???? I.y kC5e.s t?o7?) C.ivcn an array x of
interers. it r.?nJs t;.?irat rositive cosporent x(J if t?ere is
one jair ?`o paraliul procc?t'S to cntc'. t?? odd as e'?en suoscripted
arraa,' cicrerts. [i?ure 3.4 ,?:ca the aasert?uss used in an axicratic
prouf. It ?s not hard to see t?:at the:? eor.sti.tJte a pr?af r-rov?dcd
that the assertions for .addsearz. and r.?'ensearch are interference-free.
To verifa thiS We oust show that for each statenent T in Evenseare".
and each assirn:nent T' in Odr.eareh
(preCT)Aprt(T?)) To+ ipreCT))
(poat(T).?pre(T')) T' (post(T))
cThe argurent that Lvenseareh does not interfere with Oddseareh is
aysj??ctric.) The on?y part of th assertions in evensearch wbich could
be ehanged by an assignoent in ?Jdseare:.' is
> ?.in(o?dtop.e':entop)
which aight be ehaneed when oddyca sets oddtop:?j . So we r?st
ehee?
-. ein(oddtep,eventtp) t. pre(oddyes)) oddtep:-j
> e.in(oJdtop,e?entop)
43
Findpos: bc?ii, integer M x!L:?)
initiali=e: i:?2; i.?1 eventop:?oJJtop:??.1;
search: cobe?in
evensearch: whi!c i<r..in(oddtop,?ventop) Jo
eventest: ?f x(i]>O
t?cn			cvcn?'es:			eventop:-i
else			evenno:			i:-i.2
od?scarch: ?hile ?<rin(o?dtop,cventop) do
oddtest: ?f x(j)?O
then			oddycs:			oddtop:?j
els?			o?dno:			j:??2
coerd;
k:.:inCe?entop?oddtop)
end
Fi;ure 3.3 The Progra?? Pindpo$.
?indno?: `.-`??r.'
`.1-i?.'-t?: i:?2; j :1;
??jrch: e?!??y1.
l:vens?arc?.ii i?rin(cdc?top,c?'cntQ?) `a
.f.S A i<??..to?
eventest:			o+?r1j>0
t!.en (Is			A x(i??O) c':cfl:'cs: evcr.top:'I (rs)
e!?e (LS !. j<even?op A x?i]<?,' c'?cr.,.o: i:=i.2			(?S)
1/
(5 A i>,.,tn(oddtop,e'iantc'r,?)
(os)
Oddscarel?: -.4iIa j<?ir. (oc!?tep evantop) do
(05 A j<oeLtop A j<!?1)
oddtes?: ir xfj]>0
then (r)S A )<`A?l A x!j]>o) oddycs: oddtop:-j
else (05 A j<oddtop A x(j]<O) oddno. j:-).2
(05)
(0' A j>rnin(oddtop,eventop))
coend
(o A 5 A i'-n.n(o?.dtop?cvcntop) A j>?jn(oddtop,ever.top))
k:-min(oddtop.eventop)
A Vi (0< i<k --H x(i)<O) A (k?t ?
end
??hcre 5 - (eventop<.'l?1A'rk((k even A 0<?<i) ? x(kJ<0) A i even -
A (eventop x[e'.cntop)>0))
os - (oddtap<:4?l A ?k((.': odd A o<k<j) x!I:]<o) A J odd
A (oddtop< x!oddtop]>0))
(05)
(05)
Figure 3.4. Partial Correatnoss Proo?. of Find?os.
Since
45
preCodd?'es) (05 A j < ?dtop A x[jl >
>			< oddtop)
the test is satisfied.
3.?.Can?istctc?'ofI';?e!uctives'???.-`heI
In Secion 2,4 we discusscj consistcncy for the two dcfinitions
of the se?antics of SL. Here we deri?'c sluilar results for CPL. Once
sesin a foreal proof of the rain theorcr is delayed until Chspter 6.
3.15.Thearer: If pre and post are assertion functions for (P) 5
5 is 3 corponent of 5 and a is a computation for 5 from 5o
with P[s0]=true then
I)			if			5'			is curren' after a preCS') is true after a
2)			if			a			finishes 5' post(5') is true after a
Prof: By induction on the length of a . The details arc given in
Chapter 6. I' a is cepty, 5 is the only leaf and pro(s) is true
after a sirce P ? pre(s) . For CL m'T if 5' is current after
a it either btc?.e currcnt when T was executed or was already
current after a' . in the first case, pre(T) is true after a' by
the injjction h,'?othcsis, and starting T makes pre(5') true lust as
in a sequential program. In the second case, T and 5' arc state.?cnts
fr?? different parallel processes. By induction, pre(s') is true
after a' and pre(S') remains true as T is executed because of thc
interference?free property.
3.Ib.ton': (Cen?i?tcrn?y for ?L) If `:P'? s :0) can he poved
It Ia true for the int?rpretcr.
Proof: Since ?P 5 iQ? can bt noved there arc assertion runctions
pr and po?t for (Pi' 5 (q) (Teurer.. 3.14). No',,' surplie a executes
:1 tron ???? ?6 with P[s0)tr?e Then bv, the last theore..,
post(S)(value(s0.?)]?true , an':' .?[value(sc.?)].true ain::e post(S)-? Q
So (P) 5 (q) is true for the interpreter.
As a thin e?a?9le of a ?,?L prt?f, `,,e considtr a standard proble?
fron' the litvrature of parallcl prozrar.r.in,,. A producer process
generates a stre:,m of vaucs for a ccnsur..er process. Since the produc-
tiOfl and consunption of values proceeds at a variable but reurhly
equal pace, it it profitable to inter,rose a buffer bet-?een thc two
processes, hut since storage is l?r.ited the buffer can onlI' contain I,'
val?cs. Fi?uro 3.5 shea's on? toiutien to this probe.. lore the
variable o+`in? counts the n??ber of va'?uos a'n?ch have beeadded to
tIC buffer, and buffcr[in and ;j is the next erpts' b.?ffer position
(if Lhcre is one). The variable "out" counts the n?r.'aer cf valees
which have boon rc.'.'.oved, and buffer(e.'it rod.'?] is the ne?t full
position. There arc (:r'-out) values in the buffer. The a'?.?it staten'ent
in the producer prevents a ??:-? roe being added when t:?erc is no
availabl space, while the' ?`...`.i. in the consunor do's/a reroval until
there is a value in the buffer to be renoved.
Figure 3.6 ccntains a prone fl ah?ch eo-.putes l['?)
- 1 ... `I usine this pneducen-consuo.er sencre.
Fi:une 3.7a-c sives assertion functions for (`.!?O'i f:l `E[?).f(g(A(&')))
fgl: ?c?in
ln:--Hout:?O; i:--Hj :?1;
(i A i?in?I-1 A j?ou??1?i)
ccb??in
A i?in.1?i) pro?u??r (I)
A j-out.1?1) cons??r (i A ?(k]?f(g(A[k))). 1<k<M)
coer?J'
(B(k)-f(g(A[k))), 1<kr'.)
en?
I - ((b?ffcr[(?-1) ?od NI?gfA[k]),out<k<in) A O<in-out<N A
1<i<??1 A lj<?<?.1)
Figure 3.7a. Proo= oE cor..p?tc??1 (main pro?rarn).
(T A i??in'I??:
prot!t:c?r hi Ic i
A =in?1 A <`I)
??,i? x:(A[i))
(I A j??n? A i''I A x--H.g(A(i1))
a??it i;-?ut?N tht-r;
(1 A i--Hin.I _ A x=?(A(i]) A in-out<\?,'
?dJ: buf?cr[in r?d :1
(i A i=ir?I A <`.1 A ?uf?cr[in r?d .\].rCg(A[i))) A ln-out<N)
?ar?in: i.?:?in?1;
(I A i-in A
I :???I
?I A i?in.1)
(I)
cnd
J - ((buffer[Ck-I) rod :?J=?(A('&?), cut<k<in) A O<in-ojt'N
A 1<i<?'1 A 1j<?<'1.L')
Fi?urc 3.7b. ?roof of co.?ut?'r-g1 (prolucor).
be?in coT.?cnt tjffcr(o:N-1] is the sh?red bufrer
in - number of values ad?eJ to bur'?fer
out - nuaber or valucs rcmovC? rro.¶ buffer
ir.?out - nurber of ele?..ents in buffer;
end
in:-cut:?O;
c?bettr'
producer:
await in?out<? then;
add: buffcr(in mod ?.]:.ncxt value;
markin: in:?in.l;
coend
conauner:
await in-out>O t?en;
remove: this value : buffcr(out mod N];
rarkout: out:?out.l;
Pleure 3.5. Prod?cer and Consuser Sharine a ?ounded Buffcr.
f?1: hc?in c?nent bu?r?r[O:N-l) is to shared b??=cr
in n?n..ber o e1?'rcnts added to `)ur?er
out nur.I,?r of e1e.?ents rer.??cd ??on bucrc.r
1n?out = n?r..ber of elenents in burfer;
in:=o?t:=O;
1=5:1
eobe?in
producer: bile i<Y. do
begin x:g(A[il);
sait in?out<N then;
add: buf?er[in r?d x]:-x;
r.a??in: in:?in.1;
i:?i.1
I,
end
consumer: while 5<. do
be?in swa:t in?out>O then;
reeve: y:=bufcer[out rod N];
markout: out:-out.l;
end
coend
end
Figure 3.6. Computation of ?(ki-f(g(A[k])). !<k<'i..
SI
(1 A IC A j-out?1.1)
constw?er: whi)e j<M do
(i A IC A j-out?1 A _
beein await in?out>O th?n;
(i A IC A j?out+l A j<M A in-out>O)
remove: y:?buffcr[out mod \.`];
(1 A ?C A j?out.1 A j<M A y?gCA[j]) A in?ou?O)
markout: out:-ouz.1;
fi A IC A i-out A i&M A y-s(A(i]))
fi A IC A j.out A ?<M A B[j]-f(gCA(j))))
j:--Hi.1;
(I A IC A j-out.1 A j<."?1)
end
(I A IC A j--HM.+1)
(I A 3[k)'fc?(Atk))). 1<k<'()
I --H (?uffer[(k?1) mod Nl-gCA[k]), out<k<in) A Ocin-out<N
A 1<i<'.?.1 A
IC - (B(k]-f(:(A[kl)), lik<i)
Figure 3.7c. Proof of computefgl (consumer)
5..
52
Tile reader can verify that the assertions satisfy Definition
3.11. To satisfy the interferenec-free critria, asserti?ns in the
cons??er must be invariant over stateTnts in the producer and
vice versa. Consider the fern of the assertions in the constL9.er. Each
consists of the invariant I plus sone relations between variables
which are not chaneed in the producer. In addition. two assertions
contain the clause (in-out > 0). The assignnents in the producer leave
these three cor-ponents unchanged: I is also an in?arisnt in the
producer; the variables in the second conponent are not affected; and
the only assignment that changes (in-out) is markin: in:=in'l which
leaves (in-out > 0) true. Sinilar reasoning shows that assertions
in the producer are invariant over statements in the consuser, so
the interference-free criterion is satisfied.
?.a. j'uxilisrv ?arianies.
In many cases the axior-s and inference rules AO-A7 are not
strong enough to prove a partial correctness forrula which is true,
Figure 3.8 is an exs:nple of a program where the deductive systen. fails.
The formula (x"O) add! (x-2) is true, but it can't be proved using
AO-A7. To see this, consider post(sdda). If the program starts with
x"O , it can finish adds with x-l or x"2 depending on whether
or not addb has been executed. So the strorgest possible assertion
for post (adds) is (xl V x?2) . The asme Is true for post(addb).
Since (post(adda) A post(addb)) ? post (add!) , the strongest possible
assertion for post (add!) is (x-l V x?2) , in spite of the fact that
after executing add!, a must have the value 2.
ss
add2: beein
y:.O; z:?O;
cobe?in
(x?: A y-o)
await true thembe?in x:?xt1; y:-l end
(x??.1 A y.i)
(x-)' A x-o)
await true thenba?in x:-x+1; ::-1 end
(x-y.1 A z-1)
coerd
(cx.?.1 A y-l) A (x-y.1 A z-1))
end
Pigure 3.9 The Program add2.
F -
S6
were			c V
()?l(tin',: ?:--H-F
2 irplacIng aw?it tr?e tin x:= 0:: . provide x:?E i?a?es
at no?t one refcrcn?e to a snare variable (In tbis case, x
does not have to be an elenent of AV,)
?. ?eplacing be??n S e?d by S
We will write S-red?ce(S' ,S0) where S0 is the statenent eli=inated
in goin, fron S' to S i.e. , in 1) S0 is the assignent, in 2)
the await statenent, and in 3) the bein- ed.
In our example, adel can be obtained fro. ac'd2 by repeated
applications of the operations above. `.;??? that in order to reduce
await true then l'e'in x:?x'l; y:?l end to a'?ait true then x:'x?l
we nust first delete y:=l (operation 1), then t;?? berin - cd brse'?ets
(operation 3). The a?flchronizati0n atatenent cannot te re--Haved
because x:"x.l contains t?o references to a . It is safe to re?ove
a synchroniration state.m,-.nt when rule 2 applies, because then the
assignment statcnent can be treated as indivi?ible anr?ay.
!;ow we give the inference rule which alle'?s us to conclude
(x"O) addi fx'2) fron a proof of (x"O) add2 (x-2)
ASAuxiliarvVariablec.
If AV is an suasliary var?ab1e set for S S a reduction of S'
with respect to AV, and P and q assertions which do not contai'
free any variables fram AV, then
(P',S'(0)
(p) s
S3
fx?o)
addi: cobc?in
(x-o v x-1)
adda: await true then x:?x.1
(x-I V x-2)
(x?O V x?1)
a?d?: await true then x:-x?1
?x-1 V x-2)
cocr?
(x-1 V x.2)
Figure 3.8. The Progra? addi.-
54
\?ow consijer Figure 3.9 an c,panded ?`crsi3n of ad?l. T?e reader
can verify tiat the ass?rtions in Figure 3.9 are irterference-free
and yield a proof of (x--O) add2 (x=2 . The proof depends on the
variables y and . Since ajj2 has the sar? effect on x as aAdl.
we would like to be able to conclude fron this that (x-O) add `x.2)
In order to do this we will decinC the concept of auxiliary variables
and then ???? a new inference rule to allow th?ir use.
The program add2 has ess?ntiallv the sane behavior as addi
in spite of the fact that it contains statements and variables which
do not appear in addl. This is because t?e additional variables.
nd the statecenra usin then., do not affect the flow of control or
the values assigned to x . \`ariables ?hich are used ii. this way
in a progran. will be called auxiliaryvariables. The need for
auxiliary variables in proofs of parallel programs has also been
recognized by erinch hansen [8r73] and Lauer [La73].
3.17.Detinition: Let AV be a set of variables which appear in 5
only in assignment statements
x:?E where x c AV and any variables may be used in E
Then AV is an auxiliary variable set for 5
3.18.lefinition: Let A" be an auxiliary variable set for 5 . 5 is
a reduction of 5' with respect to AV iff 5 can be obtained fro? 5'
by one of the following operations.
fg2: be?in co=r.cnt buff?r(O:l:-l'j is the sharcd buffcr
full			nu?ber of full placca iu b?tfcr ?scmaphorc)
e.?ty - numbcr of cmpty placcs in buffer (scmaph?rc).
full:-O: empty:"N; i:--Hj:-l;
cobe??n
producer: whjlc j<'.I do
be?jn x:.:(A(iI);
PCcmpty);
buffcr!i ?od N]:-x;
V(full);
i:.i?l;
I,
end
consumer: while j<M do
be?In PCfull);
y:-buffcr(? mod Ni;
VCenpty);
B(jJ:-f(y);
i:-j.l:
end
end
coend
?igure 3.10. A Second Version of the Producer-Consumor Program.
I;.
60
f?2' : hcpin conent Pen'pty, Vc?pty, Pfull, ?`full are auxiliary va?iables
rull:--HO; eopty:??; i:?j:?l;
Pfull:-Vfull:?Pe..q?ty:?Vc.?ty:?O;
cobegin
producer: while i<',I do
begin x:g(A(1]);
aw?i eptysO then
beein e?pty:.empty-l; Pe=pty:?Perpty.l erA
buffer[i r..o? N]:.x;
awa:t true then
be?in full:?f'jll.l; Vfull:.Vrull?1 erA
i:?i+l;
end
end
coend
consumer: while j<?. do
begin await tull?O th?n
begin full:.r-ull-l; Pfull:"Pr?ll?1 erd
y:?buffcr(j mod N);
await true then
be?in enpty:.empty?l; Veopty:"'Ie:pty?l e::d
end
Figure 3.11. Program f:2?: A Translation of fg2 into CPL.
57
In order to establish that this infercnce rule is consi?tcnt with the
interpreter, we rust show that if (P) 5' fq) is trua tor the
interoreter, (P) 5 (?) is too. To do this we will show that there
as a relationship between the co.T?utations of 5 and 5'
3.19.Lc=na: Suppose S'reduce(S' is a reduction of 5' with
respect to AV, snd a is a conputatlon for 5 . Then Ia' a compu-
tation for 5' such that
I)			x(value(a0,a')]			x[value(a0,a)] for x t AY
2) if reduce(T,50) is current after a , T is current after a'
where T is sny corponent of 5'
Proof: Let a' be like a except that 5o is executed in a' as
soon as it is ready to be exccut?d. The only difference between a
ard a' is trat a' ray contain occurrcnces of . S0 may change
the value a' a variable In A", but it has no effect on other values.
The variables in AV do not affect the flow of control, since they do
not appear in the conditions of if, whilc or await statements. Thus,
the flow of control is the asme in 5 and 5' and a 15 5
corputation for 5' for which 1) and 2) above are true.
3.20The?rea: If (P) 5' (Q) is true for the interpreter and the
requirerents of AS are satisfied, (P) 5 (Q) is true for the interpreter.
Proof: Let a be a coaputation for 5 with P[s0]-true . Let a' be
tho co?putation for 5' fros Leoaa 3.19. Since (P) 5' (Q) is true
in the model, Q(value(s0,a'))?true . Then Q(vslueCs0,a))-trua , since
Q has no variables from AV. Thus, (P) 5 (Q) is true in the model.
Auxiliary variables can be a o+:ery po.?crful aid in prograr. proofs.
Startin with a progran such as sddl new ?ar;'ables and atatenents
can be a?deJeld a prorran like add for which a praof is possible.
Then AS can be applied repeated.:' to g)'?e a proof for the original
program. If the new statements obey the following restrictions. it
will always be possible to rerove then again using AS.
1. asaignoents must be to the ncw variables.
2. synchroni'ation statements trust contain at nest one statement
(and that oust be an assi:nTent) froa the original progran.
3. be?in end may be used freely as long as the result is s)?tacti-
cally correct.
4. no other kind of statement is added.
As another example of the use of auxiliary variables consider a
second version of the producer and consurer progran of Figure 3.6.
The program f?2 in Figure 3.10 uses senaphores ?full?' and `?empty
to aynchronize access to the buffer. Cigure 3.11 shows the translation
of the aeaaphore operations ito GPL (as defined in tection 3.1). and
includes auxiliary variables Pepty. Ve.Tpty, Pfull Vfull. Firjre
3.12a and 3.121) gives assertion functions for (>0) fb2 (a(kj=
f(g(A[k))).l<k<..f) (the producer is oritted but it is sinilar to the
consumer). The reader can verify that these assertions satisfy
Definition 3.11; the proof is essentially the same as for the earlier
version of the producer and consuer. Using AS. the auxiliary
variables can be removed to yield a proof of (`.1>0) fg2 (u[k)-f(3(A[5))).
Ilabermann [11a72) presents this solution to the producer-
63
consuner problem and pro??ides an informal proof of its corrcctness.
For the pr?or. be uses special functions which count the number of P
and V operations on each semaphore; yhese play the same role as our
auxiliary variables.
3.6.`??tualExclusion.
It is often necessary to ensure that certain critical sections
in separate processes cannot be executed at the s?me time. `test often
this is because the critical sections nanipulate shared variables.
and it is essential to prevent them from interfering with cach other.
Ore of the standard ways of ensuring mutual exclusion is the use of
a secaphore ?utex whose initial value is 1. Each process executes
P(mutex) on entcring its critical section and?V(mutex) on leaving.
Our techniques can be used to show that this discipline does indeed
ensure autual exclusion as long as there are no other operations on
the semaphore mutex.
Figure 3.13 shows a group of cyclic processes containing
critical sections. The statements in the critical and noncritical
sections are not specified. but they do not operate on mutex. In
Section 3.1 we suggested a representation of tho P and V operations
as
PCse?) --H await sem>0 then sem:-sem-l
V(sem) - await true then sem:-sem.l
Thus the code for implementing mutual exclusion in GPL is
64
bc?in
mutex:1;
cobegin Si /?
?/ Si: ?b?le true do
be?in noncritical part;
P(r.?tex);
critical section i;
V(mutex);
noncritical part;
end
coend
// Sn
end
mutox is not chan?ed in t?e critical and noncritical sections
Fi:uro 3.13. Critical Sections with ??tual Exclusion.
61
?g2?: be?t'n
fu11:?U; e?pty:?N; i:-j:?i;
PEull:-Vfuli:?Pcmpty:.?cn.pty:=o;
(1 A Vfull.Pcn.pty A ?=Vfu?l.i.l A Vetnpty-Prull A j-\cmp?y.l??)
cobe?tn
(i A Vfull-Pc;npty A i-?'ful1.1??)
producer
`I
co?r.d
f? A Ve?pty?Pful1 A j?Vc.?pty.1-i)
cons?cr
(i A ?(k]--Hfc:cA[k])), 1<k<M)
cnJ
(B!k1-fc:cA!?1)). ?<k<M)
I - (Cbuffer[k ?od \`]??cAfk]). Vc:nptx<k<Vfull) A full-Vfull-Pfull
A cr?tx.?.'.Vcmpty-Pernpty A i<i<M.1 A 1j<'<M?1)
?i?ure 3.12a. Proof of f?2 (r?in pro?r?)
r -.
62
?`1 A iC A V?r..pty-Pfu11 A j?Vcr?ty?i?1?
consur..cr: ?hiIc 3<>'. do
(I A IC A j'4 A Vc.Tpty-Pfull A j?Vcn.pty.l)
hc?in awlit full?O th?n
bc?in fuull-1; P?j11:?Pfu11?1 c.'.?;
(1 A IC A 3< A Vc?pty?PfuI1-1 A j?'cflpt)'.1 A Vfu11?Ve.Tpty)O)
y:?bur?cr[j nod ?);
(1 A IC A j?'! A Vcr..pty?Pfu11.1 A j-Ven.pt>.1 A
a?ait true thcn
bo?in cmpty:?cn.pty.i; Vcn.pty:?Ve?pty.1 end;
(1 A IC A 3<M A Vc.?pty-Pru!1 A j-Ven.pty A y-g(A[j]))
B(3J :?r(y)
(I A IC A 3<tI A Vcopty=Pfull A j.Ve:npty A 8(i]-'CsCA[jl)))
3:--H3.1;
(1 A IC A j<>l'1 A Vcopty?PfuI1 A j'Ve:npty.l)
en
(I A IC A 3?!.?)			(B(k]?f(g(A(kJ)), 1<k<>1)
(Cbuffer(k wed .\`]?gCA[k)), Vcopty<k<Vfull) A fu11-Vfu11?P?u11
A eopty-N?Ver;ty-Pempty A 1<i<>I?1 A 1<3<M.1)
IC --H f8[k]?f(gCA[k])), 1<k<3)
Figure 3?12b. Proof of fg2 (consur?r).
67
Since (inCS[k)-lAl) is t?e throughout the critical section in
process k (inCS(i)"l A inCS!i)?l A I) is true aftor a . 8ut
(inCS!i]-l A inCS(j).l A I)? mutex<O A mutex>O? false. So no such
a exists.
Froofa of mutual exclusion will be discussed rnore extensively in
Chapter 5. For now we close by giving an exanple of the use of mutual
exclusion in a proof of partial correctness. Figure 3.15 is a
rewriting of the program addl of Figure 3.8. lere, instead of
representing x:.x+l as an indivisible statenent, it is written .15
a:-x x:-a.l where a is a local variable. Scrnaphores are used
to guarantee mutual exclusion for the critical sections whid? operate
on x . Figure 3.16 is an extension of this prograrn, using auxiliary
variables. The proof of the interference-free property for the two
parallel staterents ma?es use of mutual exclusion. For exa??le, to show
that pre(sddl) (x'a"z A y-O A inCS!l)-l A I) is invariant over
add2 we must prove
(pre(addl) A pre(add2)) add2 (pre(sddl))
But preCaddl) A pre(add2)?false so this is the same as proving
(false) sdd2 (pre(addl))
Now (false) 5 (false) can be proved for any statenent 5 as can he
shbwn by induction on the structure of 5 . Since false P for
any assertion P . (false) 5 (P) can also be proved. So in particular
?e can prove (false) add2 (pre(addl)) . ln general. an assertion ?
add3: becin
mut?x:?1;
cobc?in
SI: be?in P(rnutex):
a: x;
x:?a?1;
V(mutex);
end
52: begin p(n.?tex);
x:.b?1;
vcmutex);
coend
68
end
end
Figure 3.15 The Pr0?r?? add3.
6S
await nute.?>O then ??tex:?n.utex-l
critical section i
aw?it true then nutex:?mut?x?l
In order to prove that this acconplishes nutual exclusion we will use
an array of auxiliary variables inCS[l:nI . Initially. inCS[i)?O,
l<i<n and it will be manipulated on enterin? and leaving critical
sections.
await mutex>O thenbe?in eutex:-mutex?l
inCS(i) --H1
end
critical section i
await true thenbe?in nutex:?mutex?l
lnCS[i):?O
end
Figure 3.14 shows the program of rigure 3.13 with the auxiliarx
variables. The assertion that inCS(i]?O on reaching the critical
section code and 1 throughout the critical section is justified
because there are no other operations on inCS[iJ . Similarly the
assertion that I holds at all tires assumes that there are no other
operations on nutex. The interference-free requirement for assertions
in?process i is easily verified because each assertion is a statement
about inCS[i) which is not changed in Sj if i 6 j and I, ?ich
is invariant over the statements in process j
Now suppose that there is so,e computation a in which S. and
o+ i ,E j o+ are executing their criticsl sections at the sane time.
66
(trjc)
beein nutc?.:?l: inCS:-O
(l A inCSri]?O, i?l
c&?cgin Si ?/ .1/ 5:' cocnd
(false)
end
(false)
(I A incS(i]?o)
Si: while true do
be?in (I A inCS[i)?O)
noncritic?l section;
(I A inCS[l]?O)
await n.utex>O thenbegin ?utcx:-?utex-l; inCS(i]:-1 end;
(I A inCS(i]?l)
critical section i;
(I A inC5(i]?l)
await true thenb??in mutex:-eutcx.l; incstil:-o end;
(I A incS(i]?3)
noncritical section;
(I A incS(i]?O)
end
(false)
I - (mutex-(l ? inCS[k]) A e?tex>O A YjCinCS[j]-O or 1))
:nutcx and inCS are not changed in the critical and noncritical sections
eigurc 3.14. .?utual Lxcluaion Program wit? Auxilia::" Variables.
CHAPT?R 4
Th? RtSTRICTED PAPALLEL LANCtIACE (RPL)
The prograrraing language prcscnted in this chapter is essentially
a restricted version of the general parallel language of Chapter :?.
The powerful await statemcnt is rcplaceJ by another. nore limited
s>nchroni:lng statement called withwhcn. The use of shared variables
is governed by strict syntactic requirements which guarantee that
only one process at a ti:ne has access to a given variable. Since much
of the co?flexity of parallel progran hchavior Is due to interference
between processes accessing a commo,. variable. the result of t?ese
restrictions is that R?L programs are aore Intellectually manageable
than prograas written in CPL. They are also much easier to prove
correct. The proof of a program in GPL requires that parallel processes
satisfy the interference-free property; verifying this is in general
an exponertial problen. The corresponding property for R?L programs.
called o+Einisch'jr.esfrei. can be verificd in linear time. This
saving is accomplished by restricting both the syntax of the language
and the assertions In the proof. It is similar to the simplification
of proofs when the undisciplined use of ?to statements is elininated.
?L is based on a parallel language defined by lear (Ho72) and
is?si:ilar to one propased by Srinch hansen (Dr72a). bare gave a
set of axiors and inference rules for his language. however they were
not strong enough to provide proofs in a number of cases. The proof
rules AO-A7 in Table 4.1 are derived from lloare?s but are stronger.
71
72
To?et??cr with A.?, thcy form a o+`cor.plete?' deductive syste.--H.. ror the partial
corrcctness of parallel progras in RPL as will be shon in
Chapter 6.
Section 4.1 defines the s?'ntax or ?L and 4.2 and 4.3 g?ve Its
semantics in terms of an interpreti?e rodel and axiors. Section 4.4
shows that the intcrpreter and the axio,..s are consistent. `tuch of
this work makes use of results derived in Chapter 3.
4.1.TheL?n?ua?e.
RPL is defined by adding two statements to the secuential language
of Chapter 2. Parallel execution is initiated by the staterert
resource r1(var?able list)ra(variable			list):
coberin ?1,?? ???n coend
here the resources r1 ... r are groups of shared variables. and the
0
5. are statements to be e,?ccuted,in parallel. Again, no assu=ption
is made about the way parallelism is iir.plementedo+ or about t:?e relative
speeds of the 5. . it is legitirato to nest one parallel statenent
inside another. The only restriction is that the resources in the
two statements be distinct.
4.i.ucfinttion: Components T and T of 5 are in different
I			2
processes of 5 iff 5 contains a statement
resource rr : cobeo+',in 5 ??			1/5			coend
m			1			n
o9
add4: be?in )`:??:--O; :t:tex:".; inCS[L):-inCS[2]:.o;
fx-?z-O A inCS[1]?inCS[2]?O A I)
cobe?in SJ ?, S2 coend
end
Si: fx.: A y-O A incs!1]-o A I)
betin (x=: A y-O A inCS[1]?O A 1)
a?it mutex>O thenhe?tn `r.?tex:??utex-1; tncs(1]:-1 end
tx-: A ?O A inCS(1)-1 A 1)
?x-a- A y-O A inCS[i]?1 A ?)
addi: x:-a.1;
(x-=.1 A y-O A inCS(1?-1 A I)
--H1;
?x-?+1 A y-1 A inCS[1]-1 A I)
aw?it true thenbe?in rutex:-n:utex.1; incs[1]-o end
fx-zsl A y-1 A inCS[1]-O A I)
end
(x-:?1 A y-l A inCS[1]-O A I)
52 is syT??etric: (x-yA=-OAinCS[2)-O?I) 52 (x-y.lA:-lAinCS!2]-OAI)
I --H (:?tex-C1			? inCS(k]) A r.?texLO A inCS(k]-O or 1)
k-1
Fi?ure ?.?6			The Prora? ?dd4.
r
70
in a critical section is invari?nt 0v4r sssigr?ents in ot,?er critical
sections beca?ae t?e inv?riance test redt?es to (falae) S `?:
Pro?,ram addl has auxiliary variables y and irCS The
staternents ?ich manipulate these variables can be renoved using AS,
givine a proof cf (x?o) add3 (x?2)
he have only skotched tl? proof for pro?ra? add4; a cc?plete
presentation would require verifying that every assiantent and a?ait
in SI presened every assertion in 52, and vice versa. Even for such
a small program this would be a lar,e task, and it is a task which
grows cxponentially in the size of the pro,,raR?. Thus, croofa for GPL
prograns quickly becone unmans:esble. In the next chapter we will
introduce a parallel progrs.T?ing language in which nutual exclusion is
provided syntactically. This renoves much of the corplexity in the
interactions between processes and greatly airplifies the process of
proving that a program is correct.
`s
4.3.Defi?ti?n: A parallel s?ateacnt In ?PL must o?ey the followin?
restrictions:
1) Var(S) .?(S) u V1(S) u . u "?(5)
2) No variable belongs to Core than one resource;
3) if x c R(S) x appcars in 5k oni)' in a wit!??a statement
for the resource containing x
A)			If x appears In 5k			x is either a local variable for
or a reaojrce variable.
These requirerents can easily be checked at conpile ti,te. Their
purpose is to guarantee that two proccases cannot intcr?ere with each
other by simultaneousi)' operstin? on any "ariable. Rule I requires
that every variable is a resource variable or is local to acme process
5. or both. If it is a resource variable, it belon?s to exactly
one resource r Crule 2), and is accessible only in a witbwhcn state-
Cent for r Crule 3), which prevents two processes from using it
siTultaneously. If it is a local variable for 5k it is not chan?ed
in any ?i if I , so he reference in 5k is unanbiguous. If a
variable is local to more than one process. it is not changed by any
of theo, so there is no conflict even if two processes access it
sI?ultaneoualy.
In GPL it was necessary to limit the form of statements which
referred to shared variables. For exanple, x:?x?l was not a legitimate
state--Hert if x appeared in more than one'procVss. These restric-
tions were required to ensure that the interpreter accurately modelled
parallel execution. IA RPL these problems do not arise, since
6,
76
references to shared variables are sllowed only in crttical sections
and only one process at a tiae car. execute a crit?csl section for a
givcn resource. Stater..en?s lile x:--x.l are acceptable. even if x
is a shared variable.
I: AddS (Figure 4.1) is another version of the pro?rar. of
Figure 3.i. lore withwhen statements are used to control access to
the shared variable x
Examnle2: Producer and Consurer sharing a bounded bufrer.
Figure 4.2 shows a third solution (due to Ijoare [10721) for the
producer and consuler problem introduced in Craapter 3. Note the
similarity to the solution in Ficure 3.5. The critical socton in the
producer can only be started when there is free space in the buffer
(count<N) and the critical sect1on in the censure can only be
started ?hen the hucfer is not empty (count?O).
4.2.Theln???I???JVCAode?.
The interpreter t?r P'?L programs is very much like the one defined
in Chapter 3 for GPL prograns. The pro?rsn state rerains the sare
and the state transition function "next' is extended to cover withwhen
statements. This requires a definition of the states in "hich a withwhen
statement is ready to be executed.
4.4.[)efinition: A statement 5 is current in the program state
s?(c,v) 1ff S is a leaf in c
73
with T			and T
I			o?ponents of dif?erent s			Otherwise T			?nd
are in the sanenrocess.
The second ne? staterent provides for synchronization and protoc
tion of shared variables.
with r when 8 Jo S
has the followin: interpretation: r is a resource 8 is a 8oolean
expression. and S is a statcment which uses the variables of r
S is called the critical section of the withwhen statement. Execution
of a critical section can only be?in when 8 is true and `hile it
is bein: exec'jted no other process can execute a critical section for
the sace resource. If aeveral processcs arc competing r?r a resource
r we r?&e no sss?1ptlons about the order in which they receive it.
The statement with r when true do S can be abbreviated as with r
do S
It is possible to implement the statement with r when 8 do S
usin: the GPL await statement. One method is
betin await 8 A ,busyr then busyr:-true
await true the,. buayr:?false
end
where b'?syr is a new variable which is initialiced with the value
false. For a discussion of the inpiementation of withwhen usin?
74
standard sync?roni'ing operatiors ste osre [11072] and Sintoff and
van La.?a-ecrde (Si7S,l
?jth-h?n statenents can only' be uacd insi?e cc-',e?in stateronts
and ?ith'??en sr.aternents for the same resoLtree cannot be nested.
in or?er to guarantee that operations on shared vsr?ables are
well.define? the ayntax of the language restricts the way variables
are uscd in parallel processes.
.2.I)efiniti?,'?. Let 5 be the parallel stste?ent
________			,/.. .,,S			coend
resource rr0: co?eein ?l			n
??en Var(S) - the set of variables uae? in 5
R(S) - (x: x c r1 V a is in a resource r declared in a
parallel statecent containing 5 with 5 not a
conoonent 0 a critical section for r)
f<(5) is called the resource variables of 5
Vk(S) - (a: a c Var(S) and no atateaent of 5) j i k assiena
a value to
is called the local variables ?? 5k
Note that the resource variables of 5 are those variables which r?at
be protected by critical sect ions when they are used inside 5 . In
addition to tiLe variables fror. r1 .. rm they include variables
from resources declared in parallel staterents which contain 5 . The
syntactic restrictions on variables are expressed in teras of these
cl?ases.
79
Definition: A resource r is busv in program state a iff a
proper conponent of a withwhen statement which use? r is current in
5 (i.e. iff a critical section for r is in execution in s).
4.6.Definition: A statement S is renoytoexecute in the pru?u??
state 5 iff
1) S is c?rrent in 5 and
2) if S is with r when 8 do S1 8(s)-true nnd r is not
busy in a
4.7.Definition: The state transition function next: (proeram states)
X(stater.ents) (program states) is given by
next((c.v).S) undefined if S is not ready to execute
in Cc,v)
- (c?,v) where c' - replace(c.S.S1)
if S - with r when B do S1
- Cc?,v') of Definition 3.4 otherwise.
Note that with r when 8 do S is not ready to execute if a critical
section for r is already in execution. so only one process at a time
can execute a critical section for r
The concepts of a computation. and of finishine or executing a
statement, are d-fined in much the same way as in Chapter 3.
q.a.Definition: A cor.?utation a for program S beginning with
variable state v0 is a aequencc of statements S1 ... S such that
n
80
if ?o (S,v0) the seou?nce of states s? next(s??1.Si) i?l
is Jerined, i,c. S. is ready to execute after S1 ... Si?1 . In
this ease `?iuc(so,0)'5n
4,'i,I)c?tnition: If a is a computation for S , and S' is a
coaponont of S , a finishes S, iff
S is assin, null, while, bc'in ... end, if or cohe'in
coend -- same as Definition 3.7,
S' is with r when 8 do S1 and a finishes S1
4.10.Definition: (P) s (Q) is true in the interpretive model iff
any conputation a which executes S fren. an initial state in
which P is true has q[vslue(s0,a))-true.
In Chapters S and ( we will need to `xnew sone properties of
cooputations and resources. The following ler.?:?s is the basis for
this wor',,'. It states that if a resource r is busy for a computat?on
a , it must he b?sy because sona process has started a withwhen state-
ocnt S1 for r and has not yet finishee: it, From the time that S1
was started in a no other process can have access to r
4.11.Lonma: r is busy for a iff a can be ?Titten
ao+a0 S1 a1 ... 51,. a1, where
1) Si is with r when 8 do 5' and 5, is in execution for a
2)51, are froa the same process;
3)			none of the stateaents in a1,.. a			are from the same process
??
77
aeds: resource r?(x): cobeein
adda: ?it? rx do x:-x.1:
addb: ?tth rx do x:-x.1;
coend
F?guro 4.1. Pro:ram adds.
73
bo?in
corment inpointer p3sition or next er.pty space in buffer
outpointcr position or next full space ir. buffer
count nubor of e.enents in buffer;
count:?inp3inter:.-outpointer:O;
parallel: resourze Cufman(inpointer.outpcinter,count,buffer(O:N?l]):
cobe?in
procucer:
add: uith Bufran when count<.? do
be?in inpointer:.Cinpointer.l) mod X;
buffer(inpointer] -next value;
count:-count 1
end
end
consuner:
re?ovo: with euf?an when count>,O do
be?in outpointer:?(outpointer+l) aod N;
this vaiue:-bufferoutpointer];
count:-count-I
coend
end
?iguro 4.2. Producer and Consumer Using a Bounded Buffer.
83
fP?) s ?q') of the proof of (Pj) Sj (Oj) bc only those variables
?hich process 5. has a right to access at 5 . Those are roughly,
the local variables of 5. plus the variables for resource r if
5 is a coaponent of a critical section for r . For a precise
definition of Ein?ischungsfrei, we need the concept of the proof-
variables of a statement or resource.
4.12.Definition: Let 5 be a statenent and r a resource in
program 5 with r declared in the parallel statement T and let
T be the statement which irmediately contains 5 . Then
Proof-var(r) o+ ?x: x is not assigned a value in T except in a
critical section for r)
lroof-var(5') variables of 5
V?(T?) flProof-var(T?)
if 5'-5
is 5 is the kth pr3ceas
in parallel statement T'
o+ Proof-var(T?) u Proof-var(r)? if T' is with r when
8 do 5
- Proof-varCT?)			otherwise.
Note that Proof-varCr) includes all the variables which belong to
resource r anJ may also contain other variables. The variables in
Proof-var(S') are either local to the process containing 5 or
belong to Proof-var(r) , where 5' is a component of a critical
section for r
4.13.Definition: Suppose 5 is the parallel statement
resource rrm: cobecin ?1?? ..,/S			coend
n
84
Then (P) 5 (?) is Einmisch'r,?sfrei iff it nas a proof in which
I) all free variables in l(r?) arc elerents of Proof-var(r,)
I < j < n
2) if 5' is a enopoflent of 5 , and (P') s' f?s') is a line in
the proof, then all free variables in P' and Q, are in
Proof-var(5').
The variables in Proof-var(5') arc exactly those wich cannot
be chanped by another process when preCs') and post(S') are
expected to hold, i.e, when 5' is ready to execute or has finishec
4.14,Lenma: Let 5 and T be statenents in different processes
of a pro?rafl S' , and a he a computation for 5' . Suppose 5 ij
current after a , or a finiahes 5 . Then, if .T is read>' to
execute after a , T does not change a variable in Proof-var(s)
Proof: Since 5 and T are in different processes of 5' , tl:ere
is a stateacnt T'"resource r1,..,.rno+: cobe?'2, Tl//???//Tn coend
with 5 a conponent of T1 and T a coaponent of T i ?
Suppose T chanees v?riable x . Then x A Vj(T') , so if x c Proo
var(s) it aust belong to a resource r with 5 a proper co.':ponent
of a with?hen staterent ?l for r , T must also be a proper
corponent 0 a withwhe for r because of t?e syntactic restri
tions of ?PL, ?i ? , since they are in different processes, and
both are in execution for a . This is not possible, so x ? Proof-v
Rules A6 and A? are presented in a way `?hich nakes it easy to
produce proofs which are inn.ischungsfrei. The pre- and post- assert
31
4) If T is in a. (i>l) the variables in r aro not referenced
in T
Proof: r is bttsy for a iff a critical scction which l1sea r ja in
execution, and this can only happen if a with?h?n staterent appears
in a and is not finished by a . Then a can be written in the
form above, satisfving 1-3. To see hat 4 is also satisfied, recall
the a)?tactic restrictions of Definition 4.3. If T uses a variable
froa r , T must be a component of a withwhen statement for r
But then if T appears in a1 o critical sections for r are
in execution at the same time, and this is not possible.
?. Ax?oms an? Interence ?ules.
Table A.l gives the axioms and inference rules for the restricted
parallel language. They are similar to the axioms tor parallel progr,as
given by Iloare (1072]. Ilowever, Iloare does not provide for auxiliary
varisblea, and his version of A7 is more restricted in the variables
whicI, can be used in assertions. AD-AS and AS are the sar'o as the
correstonding rules in Chapter 3, while A6 and A7 give the senantics
of the two new stste:ents. Both rules use the resource invariant ICr)
an assertion which describes the acceptable states of the variabl?s
in resource r . A7 includes the provision that the proof of
f? ) s (			be Einmischun,,sfroi. This condition is related to the
i i
interference-free requirement for GPL programs, but it is oore easily
verified. It requires that the variables used in each line
AO			conacquenco			(P')5(r)PFr0'?v
(P)			s			(Q)
Al			saaI?nn.cnt			(pX) X'?L fP)
A2			null			(?)
? tp I
A3			Conposition			?)?23`?n?5n??,..l?
(P1?			be?ir 5			o+.. 5			cnd
n --H
(P A 1? 5 `0' `P `. `B) 5, (Q)
A4			altcrnation
(P)			it B t!?cn			else ?2 ???
AS			itoration			(PA1)5`0)
(P) `h'le 11 dos (0 A?B)
A6 critical ??????? (0AIA1(r))5`9A1(r))
(0) with r w.?en I ?o S (Q)
(0?) 5. (Q.) is i??ischungsfrei, l<i<n
A7 parallel			111
(0 A...A 0 A I(r ) A...' I(r )`,
1 n I n
resource r1( )rm( ): cobe?in S??????//S? coend
(Q1 A...A ?n A 1(r1) A...A 1(rm))
Al auxiliary variables
If AV ja an auxiliary variable set for 5', 5 a reduction of 5'
with respect to Al', and 0 and Q assertions which ?o not contain
free any variables fron. AV ???5'i'o)
(0)			5 (Q)
Table 4.1. Axioms and Inference Rules for the RC5tticted Parallel language.
87
Exan?Ie2: Figure 4.4 cortains a pro?r3.? which computes
f(g(A(k))) .`.1 using the producer?consumer scheme
of Figure 4.2. Figure 4.3a?c gives the cutline of a praof f?r'this
program. Note the use of auxiliary variables sent and received. The
variables in the progra?. fall into the categories below:
Var(psr f g) (A.B.inpointcr,outpointer,count.x.y.i.j.sent.received)
R(par f g) - (inpointer.outpointer,count.buffer)
V1(par f g) - (A.inpointer.x.i.sent)
V2(par f g)			(A.B,outpointer.y.?.received)
Proof-var(Bufman) - (A.inpointer.outpolnter.count,sent,received,y)
The reader can verify that the assertiona in Figure 4.5 are
Einmischungsfrei. and that they lead to a proof. The only nontrivial
part is showing that
buffer(? :od X]?g(A!k']). received<?<sent
is true after the producer?s critical section; the fact that sent-
received-count<N is needed to show t.?at the store operation does not
erase a value which is still needed.
It is often useful to express a program proof using assertion
functions like the ones defined in the last two chapt?rs.
4.1$.Definition. Suppose pre and post are functions which map
co:sponents of a progran S to assertions, and I maps resources to
assertions. They are assert?onfunctions for (P) 5 (?) iff they obey
the following restrictions for each component 5 of 5
83
fg3: b'.?in
inpointer:?outpointer: count:--O;
par f g: resource ?utaan(inpointer?outpointer.count?bur?cr): cobegin
producer: ?ni1e i<'.4 do
beejn x:?g(A[i?);
add: w:'th ?ufman ?hcn count<N' do
be??n inpointer:.Cir.pointer.1) ?od N;
buffertinpointer):-x;
ceunt:-count.1
end
I,
end
end
i:--Hi.1;
consuner: wh:'?e ?<`. do
begin remove: ?ith euf?an `hen count>O do
be??n out?oint:"(outpointer+i) mod ?.`;
y:?buffer(outpointer];
count:.count-1
coend
end
end
B[j):--Hf(y)
Pi:ure 4.4. Computation of 3[k) - fCg(A[k])). k - 1
35
of the parallel statement will usually contain an assertion shout
the local ?`ariablcs of each process (Vk) and an asscrtioh ahout
each resource. The resource invariant holds when parlIel execution
begins. and is presened by each critical section. Since its varishles
are only ?oaified inside critical sections., this means that the
invariant holds whenever no critical section is in execution; in
particular it holds when parallel execution ends.
Inrerence rule A6 reflects the fact that a process may assume
that the Invariant holds when it gains access to the resource. but
that nothing else is known about the shared variables. Ihen the
process leaves the critical section it cannot ,?ske any assumptions
about the state of the resource, since that ;nay be chaneed unpredictably
by another process.
?xamfl?e1: Figure 4.3 gives an Inforual proof of the procram add6
which is o'?tained from addS by inserting an auxiliary variable
y(1:2] . The program variables are x and y , and the variable
classes of Detinitions 4.2 and 4.12 are:
Var(par)
R(par) -			(x)			Proof-varCrx) - (x.y(l),y(2))
V1(par)			- (y[l])			Proof-vsr(adda)			-
V2Cpar)			- (y(2])			Proof-var(addb)			-
The reader can verify that the proof is iinelschungsrrei, Repeated
application of AS :ives a proof of (x-O) addS (x-2)
o+ o+/.
he?inCO!.i?nt )l). y(2] are a?xiliary variables;
y[i) :?y(21 :0;
(y[l]?O A >(2]?o A l(rx))
resorcL rx(x): cobc?tn
adda: with rx do
(y(l]-O A !(rx))
be?in x:??.l; y(l]:=l ed
fy!1]--H1 A l(r?))
I,
end
addb: with rx do
(y[2]=O A I(rx)?
bc?in x:"x+l; y(2):?l end
?y[2)--Hl A ICrx))
coend
(y!l]?l A y[2?--Hl A I(rx)?
J(rx) -			y[l]
?i;urc 4.3, An Informal Proof of (x-O) add6 `.x-2)
91
(?-reccivc??l?l A ?<`.i??)
con5??ncT: ?hi1e Jr do
(j?r?cciveJ?1 A Jr A B(k)?f(g(At??)). 1<k<i)
be?in
(j?recci??d?1 .` J<'t A B(??=f(gCA(k))) l<k<j)
rc?ove: with Burman ?h?n count>O do
(J?rcccived?i A Jr! A B?k??f(g(A(?l)). ljk<J
A i(aut?an) A coLint?O)
be?in outpojntcr:.(outpointer?l) ?od .?:
y:?burf?r(o?tpoilltcrl
count: count-I;
rccejvcd.?rcccived?l;
end
?J?recei?ed A Jr.t A ?t?)?fc?cAtk1)). 1<?<J A y?g(A!J))
A IcBufoam));
(J=receivcd A J<M A at?1?f(&(A!k?)). 1<?<J A y?gCA(J1))
8[J):.f(y);
(J?recciYed A Jr' A B(kJ?tc:(A[?])). 1<):?)
J:.J?1;
(J?receivcd.l A J<Mtl A ?[?-)?t(g(?[k])) l<k<J)
erd
?j?rcceivcd?1 A J<M.1 A ?B(':)?fcgCA(k1)) ij?<J) A
(recciyed"(. A B(k1?f(:(A(k1)) 1<k<'I)
PL?ro 4.Sc. Proof of fg3 Ceonsumor).
92
l)-6J			Sam			as licfinition 2.2			for sequential progr?s
7)			if			5			is ?ith r ____			do S1 then
a)			pr?(%?) A ii A 1(r) ? prc(S1)
h)			post(S1) h post(S?) A			1(r)
3)			if			5.			is r?sorce rr?: cobein S1 Ii.../I S? coer? then
a) pre(S?) ? (pro(S1) A .. A prc(Sn) A 1(r1) A ... A
b) (post(S1) A ... A post(Sn) A 1(r1) A ... A I(rn))? post(S)
c) if T is a propor co?por.cr.t of 5 the free variables in
proCT) and post(T) are elements of proof-?ar(T)
J) the free variables of 1(r) are elements of proof.var(fl
4.16.Theoren: Ix pre . post and 1 are assertion functions for
(p)			5 (QI			it is possible to prove (p) 5 (Q)
proof: Similar to proof of Theorem 2.?.
4.17.Theoren: if (P) 5 (Q) can be proved without usior AS there
are assertion functions for (P 5 (q)
proof: Simil?r to proof of Theoren. 2.4.
if the proof of (P) 5 (q'. uses A8 it is not always possiblo to find
assertior. fjnctiona for (P) 5 (Q) . ?or exanpie. the proof of
(x-O) add6 (x-2) eivea assertion functions for add6 with
pre(adda)
poat(adda) -
39
(>1)0)
fg3: bc?incort,.ent sent and receivod are auxiliary variables;
inrointer:?outpointer:?count:?O;
i:--H5 :--Hl;
sent:?received:-O;
(I(Bufaan) A i?sent.l-l A j-received.l?l A al>o)
par f a: resource Bufaan(inpointer,outpointcr.count,buffor):
cobe?in producer ,/ consumer coenl
(I(Bufman) A received?1 A 1l(k]-f(g(A[k])) 1:-i`I)
erd
(??k]--Hf(?CA(k])). L--Hl>1)
uhero l(Bufman) - (Osc?unt<N A count-seIt-received A inpointcr-sent mod N
A outpo?ntCr-received ?od N A buffer(k `nod N)
g(A[k]), received<k<sent)
Figure 4.Sa. An Informal Proof of fg3 (main program).
YA?:
90
(i?scnt.1?i A i<'i.1)
pro(Juccr: fli?C i<" (0
(i?sent?1 A _
bc?in x:??(A[i]);
(i?scnt?1 A i<.'4 A x
add: ?ith ?u.an ?hcn count?N do
(1?scnt.1 A i<? x?g(A[i)) A IcBuc??r.) A count<.\')
begin inpointer:--(irpointcr.1) rr?od N;
burfer(inpointcr]:-x:
count:-count.1;
scnt:-scnt?1;
enj
(1?sent A ?<:? A 1(?ufman));
(i?s?nt A i<.'i)
i:?i.1;
(i--Hscnt'i A i<'&?1)
end
(i--Haont.1 A i<M?1 A `Ci<x))
?igure 4,Sb, Proof of fr.? (nroducer).
OLAPTER 5
AnDITIO\.?AL PROPERTIES OF PARALLEL PROGL?'1S
So far o'jr work has been directed toward proving partial correct-
ness as expressed by t?e fornula (P) 5 (Q) A number of ot?er
properties are relevant to parallel prograas. Four of these -? mutual
exclusion. blocking. deadlock and tcrrr.ination -- will be discuss?d in
this chapter. The techniques for verifying each of thcse properties
rely on the assertion functions defined in Chapters .? and 4. so the
first step in each case is a psrtial-correctncas proof.
`.?ual exclusion is discussed in 5.1. blocking and deadleck in
S.2 and termination in 5.3. In most eases CPL and RPL programa
are covered separately.
a.t.utualexclusion.
Two statetents in a program arc mutually exclusive if they can
not be executed at the same tine.
5.1.Definition: Components ?l and of 5 are mutually
exclusive iff there is no computation for 5 which has both 51 and
in execution.
The next t?o aectiona present methods for proving mutual exclusion in
GPL and RPL programs.
95
`4
0.6
5.1.1CPL
?,tual exclusion for CPL procras was discussed inornally in
Section 3.S. At that time the primary interest was in using mutual
exclusion in verifying that parallel processes arc interference.free,
Now we provide a encral technique for proving that ?utual exclusion
is accomplished.
5.2.Theoren: Let pre and post be assertion functions for (true) 5
Consider statements			and ?2			Let PI and P2 be assertions
such that
components ci			1
precS1,) ? P1 for all			of 5
pre(52,) ? P2 for all components ?2, of
Then if P1 A P2 ? false, ?l and ?2 are mutually exclusive.
Proof: Assume that there is a computation a which has both cl and
in execution. Then some component ?1' of ?l is current in e
and so is some component ?2' of ?2 By Theorew 3.15,
pre(S1,)(value(s0,e)]?true and precS2,)[value(a0.a)i?true . Tnen
(P1Ap2)[vslue(s0.e)]=true , but this is impossible since P1AP2 ? false
So no such a exists, and ?i and ?2 are mutually exclusive. -
As an example of the application of Theorem 5.2, consider the proof
for mutual exclusion using semap:?orea presented in ?igure 3.14. ?erc
and ?2 are the critical sections in processes i and I with
i 6 i P1 - (lAinCS(i)-l) and P2 - (lAinCS[1]-11 . Since
P1 A P2 false , ?i and ?2 are mutually excluaiye. This proof
But these are not assertion functions for addS which does not
operate on y , and in fact there are no assertion functions for
(x"O) sd?5 (`.-2) . This will be retlected in the proof of Theorem 4.20.
?. Consistency.
Rules AO-AS are consistent with the interpretive model, i.e.. if
(P) 5 (Q) can be proved, it is true in the model.
A,lS.T?eoren: Suppose 5 is an RPL program, and pre , post , ?nJ
are assertion functions for (P) 5 (?) . Let 5' be a component of
5 and a be a computation for 5 from ????? with P[s0)-true
Then,
1) if 5' is current after a pre(S') is true after a
2) if a finishes 5' post(S') is true after a
3) if resource r is declared in a statement which is in execution
for a , and r is not busy for a , then 1(r) is true after
a.
Proof: By Induction on the length of a . The details are given in
Chapter 6. T'i,e argtL--Hent is much the sara as for Theorem 3.15.
4,l?.Theorra: (Consistency of AS) If (P) 5' (Q) is true for the
interprative model and the requirements of A8 are satisfied, then
(P) 5 (Q) is true for the irterpretive model,
Procf: The sam as Theorem 3.20. which expressed the consistency of
AS for GIL prosrams.
94
4.20Theoren: (Consistency for FtPL) If (P) 5			can be proYed
it is			true in the interpretive rodel.
Proof: dcc induction on the nurber 0.' uses of AS in the proof of
(P)			s (q)			lf there are none let pre and post be assertion functions
for (p? 5			. Now suppose a executes 5 fron state 5o with
P[a0]?truc			Thcn by Theorer.. 4.18 and the fact that post(s) ? Q
Q[value(s0,o))?true so (P) 5 (Q? is true in the codel.
If the proof of (P) 5 (Q? uses AS It can be rewritten so that
all the steps using AS appear at the end of the proof. Let (P) 5 (Q)
be the last step which does not use AS. (P) 5 tQ) is true in the
model. By Theorem 4.19, each application of AS preserves this
property. So iP) 5 (Q) is true in the model.
99
for'? 0
philosupher 4			nhi?o?ophcr 0
philos-
opher 3
philoopher 2
p)'i!os-
opher I
Figuro 5.1. The Dining Philosophcr$.
/44
loo
dining philosophers: be?in cor?c'nt Integer array af!o:4]
af[i) is the nuaber of forks available to philosopher t;
af:?2;
resC?jrce possforks(sf): c&?e?in
phil 0 II...,, phil 4
coond
enJ
phil i: while true do
be-,in
getfork i: with poasforks when af(ii.2 do
begin af[iOl]?af[iOl] - I;
af!i?l)-af(i?l1 - 1;
end
end;
cat i: eat";
releaseforks i: with poaafor)ca do
begin af(iOl]-af[iGl] 1;
af(i?l].af[i?l] * 1;
end;
think i: "think"
Q and 0 indicate arithactic :odulo 5
Figure 5.2. Program for the Dining Philosophers.
07
depends on the auxiliary variable inCS but the next theorem can be
used to show that the critical sections in the ori?insl program
(Figure 3.13) are also mutually exclusive.
5.3.Thenre?: Suppose ?i			and 5,.			arc mutually exclusive
co?ponents of a GPL program			5 , and			5 is obtained by reduction of
5' as in inference rule AS without eliminating either 51 or
Then			and			the corresponding reductions of ?i' and
are mutually exclusive.
Proof: If not, let a be a computation for 5 which has ?l and
in execution. By Lemma 3.10 there is a corresponding computation a'
for 5' which has ?l			and			in execution. But this is impossible.
since ?l' and 5 ` are mutually exclusive. So 5			and
2			1			are
mutually exclusive.
In the semaphore example of Figure 3.14 the references to the
auxiliary variable inCS can be removed one by one, to yield Figure
3.13. Applying Theorem 5.3 at each step shows that mutual exclusion
is preserved.
5.1.2.RPL.
The RPL withwhen statement is designed to provide mutual exclusion
for statements which operate on shared variables. )iowever there are
tises when the programmer must control the 5?h?d?l??ffl? of resourcea
directly and must provide his 0%', code for?mutual exclusion. In such
cases mutual exclusion can be verified using techniques much like those
93
used for (;PL, but thc problem `,s corplicated by the restrictions on
variables used in the assertion f,,?nctions.
As an e.?anple, censider a standard synchronization problen., the
five dinine philosophers Fi?'c philosophers sit around a circular
table (see Fiure 5.1), alternately thinking and eatin spa?hetti.
The spaghetti is so long and tangled that a philosopher needs two forks
to cat it, but unfortunately there are only five forks on the table. The
only forks which a philosopher can use are the ores to his ir.?ediste
right and left. 3bviously two neighbors cannot eat at the same time.
The problem is to `rite a pr9grso for each philoaopher to provide this
synchronization. Hoare's solution [1072) is given in Figure 5.2. The
array af[O:4] indicates the number of forks available to each
philosopher. In order to eat, a philosopher oust wait ?ntil two forks
are available; he then takes the forks and reducca the number availablo
to each 0' his neighbors. Figure 5.3 gives pre- and post- asaertions
for some of the statements in the dining philosophers program. `etc
the use of an auxiliary array variable, eatin,-?'O-.4] . The staterents
labelled "cat i" and "think i" do not change either eating er a
We would like to use the assertions in Figure 5.3 to prove that
mutual exclusion is accerplished, i.e., that two neighbors do not get
to eat at the same time. The technique used will be essentially the
same as for a CPL program: assume that the statements are not mutually
exclusive and derive a contradiction. So s'Jppose there is a
computation a for which both eat i and eat iQI are in execution.
For this computation, eating(i]?l A eatine[iQl]-l . If I(possfor?'a)
is also true, we havo the desired contradiction, for
103
Proof: First show that ?l does not chsn'?e any ??ariablea u?eJ in
To see this. suppose ?l chances the value of x If x is not a
resource element, the s?,ntactical restrictiena prevent x from
appearing in . If x is an element of resource r must
be a component of a critical section for r Since ai?i does not
finish this critical section, r is busy in ai?i . By Lemma 4.11.
S2 does not refer to x
By similar arguments. ?2 does not change any variables used in
snd ?i and are not both with?hen statements for the same
resource.
\.`ow 1-2 can be proved using induction on the lencth of a2 If
a2 Is empty. a - a1S1S2 and 6 - a1S2S1 . Since Si and 5 do
not ?odify each other's variables. they can he executed in either
order with the same result. and 1 and 2 are true.
If a2 - a'S' let a - value(s0.a1S1S2a') . By induction.
value(s0.a152?1a') - 5 . Then. 5' is ready to execute in a and 13
is a cor;utation. Also. vslue(s0.13) - next(a.S') - value(s0.a) and
1 and 2 are satisfied.
S.S.Le:??.a: If a - a1S1m2 is a computation for 5 where
is not the last state?ent in a critical section, and tho statements in
a2 are not from the same process as 51 then
1)			13 - a1a2 is a computation for 5			and
2)			if T			is current after a			and T is not from the same process
as ?l			T is current after			13
/.
104
Proof: Lcen? 5.4 can b applied several tires to obtain the coaputation
a' - a1a2S1 with vslue(s0.e) value(s0,?') . Letting a - a1e2
satisfies 1 and 2.
This is equivalcnt to `tacking up" one statement in the process
containine ?i
5.6.Lcona: If a statcment S which does not properly contain a
withwhen statement. is in execution for a there is a cor?utatiom a
such that
1) S is current after a
2) if T is current after a and T is not in the sate process
as 5 T is current aftcr a
Proof: Lemma 5.4 can be applied stveral tir?a to "back up" until 5
Is current. (Since 5 does not properly contain a withw?en none
of the statements to be deleted finishes a critical section.) At each
step the deleted ststeaant is a component of 5 so 2 is preserved.
Provin?utuatxc?usion.
With this background we can state and prove a general theoren which
can be applied to prove outual exclusion for the dining philosQohers.
?.,.ucrini?jun.			r			isresource in 5 1ff no wit??hen
statement for r			in			5			properly contains another `?i?hen state=ent.
5.8.Theoree: Suppose 5 is an RPL program with assertion functions
pro. post and I for (true) 5 (Q), ?i and ?2 are co?panent5 of S
and P1 and P2 are assertions such that
101
(true)
dining philosophers: bc?in conTent eating(O:4) is an auxiliary array
eating[i)?l iff phiiosophcr i is eating. 0 otherwisc.
af:=2; eating:?O:
resource possforks(af): cobe?in phil 0 ??...// phil 4 coend
end
(false)
(eating[iJ?O)
phil i: while true do
begin (eating(i]=O)
getfork i: with possfcrks when afLri]?2 do
(catinc[i]=O A af[i)?2 A l(possforka))
be?in sf[iGl):?af[iel)-l; af(i?l):--Haf[iOl)--Hl.
eating[i]:?l;
end
(catlng(i]--Hl A l(possforks));
(esting[i]-l)
eat i: o+`eat'?;
(eating!i]=l)
role?scfork i: with posat-orks do
(eating?i]=l A I(posstorks))
be?in sf[iel):-af(iel].l; af[iel):--Haf(iOl)+l;
eatin?(i) -0;
erd
(cating[i]-0 A lcpassforks));
(esting[iJ--H0)
think i: "think
(eating[i)'0)
end
(false)
I(possferks) --H ([0<esting(j]<l A Ceating[))-l ? af[j]-2)
A af[j)-2-eating(j0i)-cating!?el]], 0j<?<4)
Figure S.3. Assertions for the Dining Philosophors.
6
102
esting(i)?l A e?ting(iii]?l A l(possforks)
af(i]?2 A af[i]?2			r?lse
Unfortun?tely l(posaforks) is not necessarily true. since soce other
philosop?er nay be in the ai?st of executina a critical section for
posst?rls Nevertheless we will show t?.at
eating[i]?l A eating(iQl]=l A I(possforka)			false
?uarantees that eat i and eat i?l arc nutually exclusive. This will
be done by deriving from a another corputation a for which
(eating[i]=l A eating[ial]=l A ICpoasforks))[valuaCa0.a)]?true
Since this is a contradiction. t?e orieinal coeputation a did not
exist ?nd eat i and eat i?l are a?tua1ly exclusive.
?Backlnup?'aCoa?uation.
The technique uaed in obtaining a from a is the deletion of
so?c elewents of a in a way which is equivalent to haclir up some
of the processes. This ted?nique. ?hich was auglested by Lipton?s
reduction method [Li74b], will he used a?ain in Chapter 6. It is
justified by the fol1o'?ir.g le??as.
5.4.Ltr?a: If a a1S1S2?2 is a comp'?tation for S ?here S1
is not the last statenent in a critical section, and ?l and S2 aro
from different processes. then
1)			a - a			a			is a cor?utation for 5			and
2)			value(s0.a)			value(a0,f)
I"
10?
%Titer must have exclusive access. Fi?ure 5.4 gives a solution to
the readers and writers problen due to Brinch Hansen (Br72a): it gives
a higher priority to the writers. i:icure S.Sa-c shows s.?se pre anti
post assertions for the program using auxiliary variables rcadin?.
waiting, and writing. Applying Theorem S.S we can see that reader
excludes writer j since
reading(i]?l A writing[j)"l A I(control)
? ar>O A aw?O A (ar?O V aw-O) ? false
Also. writers exclude each other. since
wrlting[i)'l A writing(j].l A I(control)
? aw?2 A aw<l ? false
if i A i . So. the code provided does synchronite access to the file
as required.
Suppose now that the null statements labelled "read i" and
"write j' are repls=ed by statements which actually operate on the
file. In order to obey the syntax requirements of RPL, they must use
withwhen statements. even though this prevents read?r processes from
using the file simultaneously. Actually the withwhen statements are
redundant: the statements which use "control" are like a pro:rammer-
defined withw?en statezent for the file. This suggests an extension of
RPL to include programmer?Jefined eritic?l sections. The progr?r.mer
could specify the code to be executed when acquiring and releasing a
los
pre(51,) ? P1			for all components			?l'			of Si
pre(52,) P2			for all components			?2'			of
Let R --H (r: r is a sirple resource declared in a statement con
taining ?i and			and neither			nor			is a
proper component of a with?hen statement for r)
Then If PI A P2 A ( A 1(r)) false. and ?2 are mutually
reR
exclusive.
Proof: Suppose ?l and ?2 are not mutually exclusive. Then there
is a co?putation a such that ?l and ?2 are in execution for a
We will derive a cot'.putation 8 which has ?l and S2 in execution.
and if reR r is not busy in 8 - Then by Theorem 4.15
( A 1(r))[value(50.8)1-true
reR
my Lenaa 4.11, if r is busy in a so?e withwhen statement for
r say ?o is in execution for a . Since r is a simple resource,
Lerna 5.6 can be applied to back up until 5o is ready to execute.
If a' is the new computation. r is not busy in. a' . Since
and 52 are not components of ?o they are xtill in execution for
a' . Also, if r' is a resource which is not busy in 0 , it is not
busy in a' since no statements which cnd critical sections were
deleted. So t?is operation can be repeated for each reR to derive
the desired computation 8
Since is in execution for 8 , some component 51' of
is current for 8 . Then by Theorem 4.18, pre(S1)(vaIue(a0.8))?true
106
Similarly. pre(S2)(value(s0,?)J?true . But then
(P1 A A ( A l(r)))[v?lue(s0.)]?true . Since this is impossible.
r?R
and			arc mutually exclusi?e.
Lxan?le: Return?ng to the dining philosophers proble.... let
P1 --H (eatin?(iJl)
- (eating[i--Hlj-l)
R			(possfor?s)
Then P1 A P2 A ( A 1(r)) ? false and "eat i" and "eat iel' arc
rR
mutually exclusivc in the progra1. ?ith auxiliary variables. To show
that they arc rutually exclusive in the original progra? %e need the
followin? thcor?n.
5.9.Theorem: Suppose ?l'			and			are autually exclusive
coaponents of an RPL program			5'			and			5 is obtained by reduction
of 5' ma in inference rule AB, without eliminatina either S?' or
Then ?l and			the			Corresponding reductions of S1			and
5			are mutually exclusive.
Proof: Same as Theorem 5.3.
User-DefinedCriticalSection?
Another standard synchroni-ation problen.. called the readers and
writers problem. involves a nuober of processes sharinz a file. Any
number of readers may have access to the file at the same time, but a
ill
(waiting[j]-writine(j]-O)
??iter j: while true do
be?in
(waitine(jJ?writing[?]--HO)
ask write ?: with control do
beein ww:'??.l; waiting[j):?1 end;
(waitlne[j]-l A writine(?]?O)
start write j: with control when ar-O A aw-O do
beein aw:?3w?l; writing(?]:.1 end;
(waiting(jJ=writing[?].1)
write j:
?waiting(j]?writin?!j]?1)
finish write J: with controL do
be?in ww:??-l; aw:-aw-1; waitin?[j]:-writing(j]:-O end
(waiting[?]-writing(j]"O)
end
(false)
I(control) - (ar ? reading(i) A ww ? waitine[j] A aw - ? writingU]
i			j
A O<aw<l A (ar-O V aw?O) A (writing(j)-l --H waitin?(i)-L)
A O<waiting!j]. writin:(i]. readine!i]jl)
Piguro S.Sc. Assertions for Readors and Writers (writer ?).
112
resource. As Ion as this code guaranteed autual exclusion the
prograw.ser-defined critical sections could be used in programs and
proofs in the same way as the stjndard wsthwhen.
There are a rn?ier of waYs in which such an extension could be
incorporated in ?PL. One possibility is the declaration ot a r?nitor
sooewhst like Ijoare's !I'.o745] for each resource. The progr?¶er could
either provide his own code for the nonitor or accept a standard syste:
implementation. We are currently working on syntactic constructs to
provide for this feature.
S.2.Blockins.
Anather problem which is peculiar to parallel processes is that a
progran can be forced to stop before it has acco.-?lished its purpose.
This can happen in CPL or RPL programs because of the await and withwhen
statements.
S.lO.l)efinition: If S is a corponent of a GPL or RPL program s
and a is a computation for S S' is blocked for a iff S. is
in execution for a but no cooponent of S' is ready to execute
after a
ln other words. St least one conponent of S' is current for a . but
none of the current components of S' are ready to execute. ror a
CPL progs?m this means that all the current components of S are
sw?'r statements; for an RPL progran they must be with?.en statements.
or
(true)
be?in ??:-sr:-O;
coT=ent rcadinc[i]-l if reader i is active, 0 otherwise
writin:!i]-1 if writer i is active, 0 otherwise
wsitin?[i]?1 if writer i is waiting or active,
0 otherwise;
reading:?writing:=?aiting:=0;
(l(control) A Vi(resdin?[ii-O) A V?Cwsiting[j]?writing[j]-0))
resojrce contro1(sr,w?) : cobe?in
reader I ...../? reader n ?/
writer 1 ??.../? writer ?
coend
end
(false)
I(control) --H (ar			? resding(i) A			- ? waiting(jJ A 5w			--H ? writinr[j)
i			j			j
A O<sw<l A (sr-O V aw"0) A Cwriting(i)-l wsiting(i].l)
A 0<waitin?!?], writins[j), resding(i)<l)
Firure S.Sa. Assertions for Readers and Writers Casin pyogrsm).
(rcajino(i]O)
readcr i: whi?e true do
be?jn
(ro?ding(i)O)
start re?d i: ?4ith control ?hen w-O do
bc?in ar:?ar?l; roading(i]:?l end;
(readingFi)?l)
road i:
(reading[i]=l)
finish read i: ?iTh control do
be?in ar:-ar-l; readin:(i]:-O end;
(readin?(i]?O)
end
(falae?
ICcontrol) far ? reading(i) A ww - 1r waiting(?] A aw ? writfr.:Ui A
i i j
O<aw<l A (ar-O V aw-O) A (writing(j]-l waiting(il-i) A
O<waiting[j),writin:(j].reading(i]<l)
Finure S.Sb. Aaaertions for Readers and Writers Creader i).
lis
In the ?utual exclusion pro:ram (?igure 3.14) c3Ch s. h35 two
aw3lt statewents:
T1 swalt r.utex>O thcn
T2 - ?sit true then
Then.
N			i i
D1 - A (post(Si) V (pre(T1) A mutex<O) V (pre(T2) A false))
i-I
- A (false V (pre(T1) A mutex<O) V false)
i-i
N
- A (1 A inCS(i]-O A rutexcO)
:i--H1
x
? mutex<O A mutex-l			? inCS!i] A Vi(inCS(i]-O)
i--HI
mutexcO A mutex-1
? false
Thus this method of using semaphores to implement mutual exclusion is
safe from blocking.
We next consider blocking in pro?rsms with nested pnrallel state
ments. This is essentially the asme as the case with no nesting, but
the details are more cumbersome.
5.13.Theorem: Suppose 5 is a CPL program with assertion functions
pre and post for (P) s (QI . ?or each parallel statement T -
116
let			______
- 5W5it B then ..
which are not co1?ponents of another
cohe?in			11/			I/Tn coon			in 5			______
the await st?tcr..enta in T.
parallel statement inside T. . Let
11(T) - A (post(T?) ?` (V (orc(T.) A `Bt)))
I			1 1
02(T) - V V (pre(T?') t.
ii
Then if 01(T) A 02(T) ? false for all parallel T in S 5 cannot
be blocked with initial condition P
Proof: Suppose 5 ia blocked for aooe corputation a which starts
- with P true. Then at least one parallel statesent is blocked for a
Let T be a parallel atatement which is blocked for a with no
parallel statement inside T blocked for a . Then T must be
blocked at one or more of the ?1?. and n1(T) A 02(T)tvalue(s0.a)J?t?Jo
as in Theorem 5.12. Since this is a contradiction. 5 cannot be
blocked.
Exannle: Figure 5.6 is a program which uses 2 senaphores for rutual
exclusion. In an earlier exanple we showed that aingle parallel state
rents which use semaphores in this way cannot be blocked. Similar
reasoning can be applied to each of the parallel state?enTs in the
pro:ram nestedl; since neither of them can be blocked. the prolras
cannot be blocked.
Unfortunately Theorem 5.13 is not strong enough in osny cases.
Figure 5.7 shows a program o+nested2' which cannot be blocked. ?owever.
113
5.1.Deinition: if			5 is a component of th			?PL or rPL program 5
5 cannotbeblocked&,nstartingconditionP			iff there is no
computation which starts with P true and has 5 blocked. 5 can
not be blocked if it can not be blocked with starting condition (true
In nany case blocking is harmless: an await or wi.thwhen statement
Lay be blocked and then unbiocked many ti?ea during prQ?ram execution.
Ifowever. if an entire program is blocked, or ii, a set of parallel
processes is deadlocked in acquiring resources, tr.e prograa cannot
recover. In Sections 5.2.1 and 5.2.3 we describe techniques for proving
that programs cannot become blocked while in 5.2.2 a well.known method
for avoiding deadlock is related to RPL programs.
5.2.1.ProeramBlockin?inuPL.
A GPL program can become blocked if every parallel process is
stopped at an await statement whose condition is false. In order to
prove that blocking is impossible in a particular program we asaume
that it occurs and derive a contradiction. We first consider the
relatively easy case of a program with only one parallel statement.
Sin le Paralle
& itatenent:
5.12.Theore?: Suppose GPL program 5 contains one parallel statement
T - cobetin T1/?.../?T0 coend and let pro and post be assertion
functions for .:p) 5 (0) . Lot Ti. - await fi then ... be the await
statements in Tj. Then if
114
n			i
1)1			A (pust(T?) V (\` (pre(T.) A ?Bt)))
i--Hi			3			3			3
1)2			V V (pre(T.) A ,??)
i3			? 3
and I)) A 1)2 ? r.?lse 5 cannot be blocked ?ith starting condition P
Proor: Suppose 5 is blocke? =?r the corputation a which starts with
P true. Sin?e 5 can only bc blockcd at s?ait statezents in T
a has becun parallel esecution of the T For each process T.
1			I
either a has finished T. and po5t(T?)[vslue(s0.a)]'true cTheorem
3.15), or Tj is blocked at one of Ti and Cpre(T.) A
3			3
?%?.)!value(s0,a)]=true So ))1[value(s0,a))?true Since St least one
T. is block?d for a D2(?'alue(s?,o)]-true . But this is a contra-
diction, since D1A D2 "a fase , so no surh a exists.
\.`ote that if 5 contains no s?it staterents, II, is the e?pty
union, which conventionally has the value false; in this case 5 cannot
become blocked.
Examples: Chapter 3 conta?ncd several exa=ples of progrL?s in CPL.
Findpos (Figure 3.3) cannot be blocked since it contains no swait
statements. In add) (Figure 3.?) both of the await statesents have
B1? a true . The expression D2 becomes
D2- (pre(adda) A `,true) V (pre(addb) A ,true)
- false
Then D1 A D2 ? false and add) cannot become blocked.
119
the parallel statenent inner can be blocked when Si is executing
its crit?cal section. so Theoren 5.13 does not apply. The following
nore general theorem can be used in sucI cas?s.
5.14.Theorem: Suppose 5 is a (;PL program with assertion functions
pre and post for (P) 5			. For each parallel stat?ment T -
cobetin T1?/ ?//Tn coend let T1 - await ii then ... be as in
3--H
Theoren 5.13. and let Sk? be the parallel statements in Ti which
are not components of another parallel stateaent inside T. . Let
- (V			?
(Pre(T?) A ?Bj) V (V DSi
1:
D1(T)			--H A (post(T?) V D(Tj))
D2(T)			- V D(Tj)
Then. if D1(T) A D2(T) false for every parallel T which is
not contained in another parallel statcment, 5 cannot be blocked
with initial condition P
Proof: Suppose 5 is blocked for acne computation a which starts
with P true. First we will show that if T is a parallel component
of 5 which is blocked for a D1(T) A D2(T)[valuc(s0.a)]-true
First. suppose that T contains no nested parallel statements. In
this case D1(T) and D2(T) reduce to D1 and D2 of Theorem
5.13. and Dl A D2(value(s0.a)]-true . If T contains nested parallel
statements consider the state of each Ti after a . There are
three possibilities:
120
1) a finishes Ti and post(Ti)valu?(soa)]?truC
2)			T. is blocked at one of the Ti			and			?
I			CPre(T?)!. `B?)(valueCs0.a)i.
true
3) T is stopped inside loT..e .?k?. and by induction
cDl(sk?.) A l?2(sk))(va?ue(s0.a))-true
This gives D1(T)[value(a0,?))?true and since at least one Tj rust
be blockcd for a D2(T)(value(s0.a)).-true Then if T is blocked
for a 01(T) A L,2(T)[value(a0,a)]?true
N'o?? if S is blocked for a at least one of the outer=?ost
parallel statements T' is blocked for a and 01(T?) A 02(T?)'
(value(s0,a))?true ?ut this is a contradiction so no such a exists.
?ote that Theoren 5.13 describes the special case of Theore? 5.14
in which 01(T) A 02(T) --H false for all parallel T -
This theorem can be used to prove that the program nasted2 in
Figure 5.? cannot be blocked. Figure 5.8 shows sore pre and post
assertions which can be derived by expressing P and V with await
statanents as done in Figure 3.14: Than
D1(inner) - (post(S2) V (pra(wait2) A eutex<O)]
A ?post(S3) V (pra(wait3) A eutex<O)]
? (incs[2)-inCS(3)-O) A T
01(outer) - (post(Sl) V (pre(waitl) A autexjO)]
A !post(innar) V O1Cinner)]
> (inCS[l]-inCS(2)-inCS[3)?O A I)
mutox-l
117
nostedl: be?tn ni:?m2:-l;
outer: cohe?in
SI: be?in P(ml);
critical section 1,
V(ml)
end
end
S2: ?e?jn P(ml);
critical acction 2;
inner: cohc?in
521: bc?in P(?2); critical a?ctinn 3; V(m2) cnJ
522: be?in PCm2); critical section 4; V(m2) cnj
coend;
coend
end
Figure 5?6. Neated Parallel Statements 1
118
nc?tcd2: h(?in ml:?;
outcr: O)??in
51: h???n ?ait1: P(rrl);
critical accticn I;
V(ml)
`I
cnd
inncr: cobcv?n
52: bcgin wait2: P(tnl);
critical section 2;
V(ml)
coend
coend
end
53: be?in ?ait3: P(ml);
critical section 3;
ond
end
Fi?ure S.7. \?ested Parallel State?ents 2.
121
rcsojr?e rl.r2: cobe?in'
51: with ri do with r2 Jo
?I 52: with r2 dowith rl do
coend
If 51 acq'Jires ri and 52 ac?uires r2 neither statement can
proceed and the program is desdlockej.
5.16.Definition: An RPL program 5 is deadlock-free 1ff there is
no computation for which 5 is deadlocked.
There is a well-known technique for avoiding deadlock; each
pracess must request and release resources in some standard order. In
an RPL program this C3fl be accomplished by reatr?ctiona on the nesting
of withwhen statements.
5.17.Theorem: An RPL program S is?deadlock-free 1: its resources
can be put in an order r1			r.			such that no withwhen statement
I			1m
using r1 properly contains a wthwhen statement using ri With
1			k
k<j.
Proof: Suppose 5 is deadlocked for t?.e conputation a . Let 5
l<i<n be the components of 5 which are deadlocked, and let i be
the largest irdex of a resource such th?t one of the 5. is blocked
at 1 withwhen statement for r. . Then some 5. is blocked inside
a critics! section for ri say at a withwhen statement for r.
i			1k
Then k > i but this contradicts the choice of i So 5 cannot
be deadlocked.
124
Of courae, there are ot.?er o+?ys of avoiding deadlock, but the
tcchniq.?e above is especially convenient since it can b checked
syntactically. Note that a pro?ra.? with no nested cr?tical sections
is Jc.idlock-?rt.c.
Ix.r.nlc: Figure 5.9a and b gives two additional solutions to the
dini?o+, philosophers problem; they are also due to Ifoare [Ho72]. The
first is in danger of deadlock, since if the five philosophers sie'ul-
taneously pick up the fork on thc right no one will be able to pick up
his second fork. The next solution avoida this problen. by rollowing
the discipline of Theorem 5.17, ao it is deadlock?free (the order is
forko, forklforl4). `lowever, it has the undesirable feature
that when philosopher 4 is eating, the other four esy be forced to
wait?until he haa finished. The solution in Figure 5.2 is preferable,
because it does not stop a philosopher from eating unless one of his
neighbors is eating.
5.2.3.Prog'ranilockin,inP?L.
Deadlock is one way in `?hich a program can be blocked; blocking
can also occur if all procesans are waiting at with?hen staterents for
conditions which are not satisfied. This situation is related to
blocking in GPL prograns as presented in 5.2.1, but it is coplicated
by the fact that the statement with r when 3 do 5 can be blocked
either because r is busy or because 3 is false. l?hen a deadlock-free
program is blocked we can sss??e that at least one statement is blocked
because 3 is false.
fi A inCS(i)?O)
Si: be?in
(I A inCS(i]-O)
%`sit i: P(¶.1),'
(i A inCS[i)?l)
critical section i;
(? A inCS(i]-1)
(i A incs(i]?O)
end
(1 A inCS[i]--HO)
?2l
I --H (il --H 1 - ? inCS[i1 A ml>O A (O<inCS(i]jl). i-l,2.3)
Figure 5.8. Somo Assertions for S? Of Figure 5.?.
122
??(outcr) - (pre(waitl) A nutcs<O] V (pre(wait2) A mutex<O)
V (pre(wait3) A autex<O)
? nutea?O
`)1(outer) A fl2(outer) --H false -
So the program cannot be blocked.
This corpletes the discussion of blocking in uPL prorra?s. In the
next two sections we consider two kinds of blocking for RPL programs.
t.2.2..?eadlockinRPl.
I)c'ad?ock is a particular kind of blockin which can occur when
parallel processes arc corpeting for resources. lt occurs when a
set of processes reach a state in wh?ch each is tryin to acquire )L
resource which is alresdy controlled bx another. In an ?PL pro3rL1
resources are acquired b/ with?hen stater?nts, and deadlock can be
relat?d to withwhen.
?.??-IJetinitlon: An RPL proIram 5 is deldlozkeA for a conputation
a iff thero are components S? l<i<n of 5 such that each Sj
is blocked at a withwhtn statenent for a resource r. and sone 5.
is blocked inside a withwhen staterent for ri. i.e.. has
slread? acquired r,
As a simple example consider the program
127
D1 .? (P05t(Tj) V DCTj))
i			i
- V V (pre(T.) A iR. A l(r.))
--H ii
D3 - A 1(r)
rcq.
Then, if D1 A D2AD3 false 5 cannot be blocked with initial
condition P
Proof: The sr?ur.ent is essentially the same as for Thcorem 5.12.
Suppose 5 is blocked for a which starts with P true. First.
note that if r is a simple resource, control cannot be blocked inside
a critical section for r , so r is not husy for a . Thus,
D3!value(50,o))-true
Each of the T. is either finished or blocked after a . If T.
is blocked, it is trying to enter sone Ti. , so pre(T1.)
? [value(s0,a)]
-true . If r is a siaple resource, it is not busy for a , so T is
blocked because B1?.[value(sn?a)]-false Thus, if Ti Is blocked,
D(T.)			is true. Since each			T			is either finished or blocked,			D
1			i			1
is			1 2 A D3(value(s0,a)]--H
true, and by Lenra 5. iS, D2 is true. So			D A D
true . out this is impossible, so 5 cannot be blocked,
There are several examples in Chapters 4 and 5 or programs which
cannot be blocked.
uinin?Philosopners(Firure5.3): The program has no nested wit?.hen
atateeer.ta and so is deadlock-free.
128
- (poasforks)
D(phil I) - (prc(gctfork i) A af(ii#2)
V (pre(releasefork i) A false)
- eating(i)-O A af[i)A2
- Aj (Poat(Tj) V DCphiL i))
- A (falac V (eatin?[i]-O A af(i]?2))
- A Ccating[i)-O A af(i)?2)
1)3 - I(possforks)
(O<catin?[i)<l A af[i)-2-eating[iOl].eating[iel))
Dj A fl3 ? A (af(ilA2 A af[i]-2) false
so the dining philosophcrs prograr.. cannot be blocked
ReadersandIritera(FieureS.4?: A very' similar proof shows that
this proeran. cannot be bloc?ed.
P.L,.dCo.????(Fi???A.S): Again, there are no nested withwhen
statements, and the program is deadlock?free.
126
5.!.-..cara: If S is a J?adloc-free P.PL pro?ram ?nich is blocked
tor a there is at least one stcte?eflt S - with r whe,. B do -?
which is blocked for a with (pre(S') t. ?B A l(r))(value(s0.a)i-true
Proor: Let T. with r whci, S. do .. be a list of the withwhen
I			1 1 --H
stateeenta at which 5 is blockea?. If all the r. are busy for a
S is deadlocked so there is at least one r. which is not busy
for a - This inplies that			l(r?)(vslue(s0.e)]-true			Also, since S
is blocked at T. ,			A ?r?)(vslue(s0.a)]?true
1			(prcCl?)
Now we derive some results which can be used to prove that lPL
prograns do not become blocked. The first case considered is progra:s
with only one parallel statelent.
Sin?lcParallelState?ent
5.19.Theorem: Suppose 5 is a deadlock-free RPL pro,,rra:a containing
one parallel etatement T			resrurce rra: 2we?in T11?. ?//T?
coend , and pre. post, and I are assertion functions for (P) 5 (Q)
i			..			I			i
Let the withwhen statements in T. be T. - usto r. when 11. do
1			3			--H			3			3
Ilefine
R - (r. r a simple resource of 5 CDefinition 5.7))
o+ ,ai if r. e R
3 3 3
- true, otherise
i i
DCTi) - V (preCT.) A P.)
1 3
131
i			i			i
D(Tj) - (\ (p:?(T.) A P?)) V (V Ul(Sk,))
?			k
01(T) - A (Po5t(Tj) V 0(Tj))
- v (preCT' A `B A 1(r))
-w??? r w?.en 13
a conponent of T
03(T) -			A 1(r)
rcR(T)
Then if 01(T) A 02(T) A 03(T) false for each parallel T which
is not a proper conponent of another parallel statement, 5 cannot
be bloc'?ed with Initial condition P
Pro?f: Suppose			S ia blocked for some coaputation a which starts
with			P true.			First, ?e will ahow that if T is a parallel component
of 5 which is blocked for a , D1(T) A 02(T) A 03(T)[value(s0,a))
true
First, ,.ote that no preceaa can be blocked inside a critical
section for a simple resource, so no simple resource is busy for a
which implies 03(T)(value(s0,o))-true
?%??t, by Leras 5.IS, 02(?alue(s0,a)]?true
Finally, 01(T) holds after a . If T does not contain any
nested parallel statement, ?i(T? reducca to 0 of Theorca S.l?,
and by similar reasonin: fl1[value(a0,o))-true If T does contain
parallel statements, there are three possible states for each Ti
1) a finishes T1 , and poat(T1)(value(s0,a)J-true
-w/ .?
132
2)			is blocked at sowe Ti			and			?
J 3 value(s0.e)].truo
(pre(T?) A P.)[
3)			is blocked inside some 5k1			and by induction
`I(Sk5,)(value(s0.e)].-tr?e
C?mI.ining l)-3) yields D1(T)(vslue(s0.e)i-true
`.:?? if 5 is blocked for a at icast one of the oterroat
parallel stateaents in 5 say T' rust be blocked for m and
U1(T?) A l)2(T') A D3(T')[value(a0.e))?true . But this iS a contradic-
tion so no such a exists and S cannot be blocked.
S.?.?.nuxiliary?`ariablc..
All of the pro?ran.a which were shown to be safe from blocking in
Sections 5.2.1 and 5.2.3 have included auxiliary variables. The next
theorem shows that the progra.?s are also safe from blocking if the
auxiliary variables are removed.
5.21Thcorem: Suppose 5' is a CPL or RPL program which csnnqt be
blocked. and 5 is obtained by reduction of 5' according to
inference rule AS. Then 5 cannot be blocked.
Proof: Suppose 5 is blocked for sore cor?utation a . By Le??s 3.39
there is a corresponding co-putation a' for 5' which is also
blocked, Since this is inpossible. 5 cannot be blocked.
By repeatedly applyin? Theore? 5.21. all references to auxiliary
variables can be deleted. and the resulting progr?i cannot be blocked,
129
R
D(producer) - prc(add) A counz>N
? sent<M A count>N
Dcconsusaer) - pre(rernove) A count<O
? received<? A co?.nt<O
D1 - (post(consun.er) v D(consurner)) A (post(producer)
V D(producer))
--H (sent-'i V (scnt<'i A count>\.')) A (received-M V (roceivcd<'l
A count<O))
D2 - D(consun.er) V D(proJucer)
--H sent<.'I V rcceiycd<'
D3 - I(?ufn.an) ? count-sent-received
Consider the va?ue of D1 A D2 A D3 for the two cases of D2,
Case1: aent*
D1 A sent<M A D3 ? (scnt<M A count>\?) A
(received-.' V (received<'I A count<O)) A count--
sent-received
? sent<at A count>N A rcccived-M A count-sent-received
if N>O
? count>N A count<O false. if N?O
Case 2: received*?
o+ /o+
130
I) A rcccivcj?? A `1
I			`3
(st-.nt?'A ?` (acnt<'1 count?)) A (received<M A count<O)
A count?sent-reccivod
acnt--'4 A rccoivod< A count<O A count=sent-received, if N?O
? count<O A count>O
false
So fl A 1)2 A 1)3 false if `-`0 This loads to the reasonable
rc?uirc?ent that the buffer used for ca??unication ru..at have at least
one' element so that the prograa csr?ot be blocked.
?estedPa??St??er?.,cr.t5.
Theoroa S.ln applies only to proera,.s in which there are no nested.
parallel statements. The theorern below is more ?enoral, and is
analagous to Theorem ?.l4.
S.23.T?eorem: Lot 5 be a deadlock?free RPL progr?T. with asae?tion
functions pre, post, and I for (P) 5 . For each parallel
component T = resource rrm cobe'in T1/?.. /iTn ecend let
Si
k be the parallel 5tate7?enta in T. which are not proper co.Tponcnts
of another parallel atatemon inside T and let T1. be the withwhen
atateoents of Ti which are not contained in any sk?			Define
0(T) = tr: r a sir'?le resource declared in a statement
which contains T)
- ?l? if r c 0(T)
- true, otherwise
13S
wax while other? reqL:ire a r?del in which there are deftnitc ruics
for sc?e?jline competing processes. I?pefully, future work will
broaden tbc range of properties which can be proved with axiomatic
iothoia.
Cii?PTF.P. 6
CO\?lSTENCY A.fl CO?'PLET??ESS OF ThE DEDUCTIVE SYSTE'?
Throughout this thesis two different nethods have been used to
describe the senantics of a program?ing language. The de2uctive syste:,
consistint of axiors and inference rules, is convenient for proving
that a prograa performs correctly. The interpreter is a mudel of the
wav statements are executed on a real nachine, and provides considerably
more detail than the deductivo systen.. In this chapter we discuss
the relationship bctween those two methods. Either one could be ta?en
as the primary definition of the secantics of the languages. Here we
have chosen the interpreter as the basic definition, since it is closer
to our intuitive unerstanding of what parallel pro?ra=s o+`mesn'?. Fron
this point of view the consistencY, theoren's in Chapters 2. 3, and 4
state that the deductive systen. is correct, in the sense that it
accurately describes the results of program execution. Section 6.1
is devoted to rather lengthy proofs of these three theoreos. Their
meaning could be summarized as "anything which can be proved is trj&'.
The converse of consistency is completeness, or "anythin,, which
is true can be proved". The axioms and inference rules give signifi-
cantly less detail about P?0?r5?? execution than the interpreter. If
the deductive system is complete with respect to the interpreter, we
are justified in saying that no essential information is lost by using
the axioms. Section 6.2 considers the completeness of the deductive
136
133
S.3.Ter?instlon.
Progra,. terrinsion is an irportant property for both p.?rallel
and scquential prorraas, although th?r arc corrcct paralici program',;
whic? do not terminate, Vario?s techni?ues have been suggcated fcr
proving termination of sequential progres (oar [IIo?9], `,¶anna [`ta741),
and the sane nc',?ods can often be applied to parallel programa. A
sequential prograo can fail to terninate for two reasons: an infinite
loop or the execution of an illegal operation such as dividing by zero.
With paralici programs there is an additional possibility: the
program can be blocked, (It is e"en possible that a program can be
blocked for one co?putation and loop infinitely for another.) iut if
a program cannot be blocked, termination can be proved just as it
would be for a sequential program.
One sppr?sch to proving terninttion is to show that each statement
terminates provided that its primary components terminate. We ?`ill
not attempt to prcaent general rules for doing this, but will give
autficlent conditions for pro?ing that a parallel statenent terminates.
For similar conditions for sequential statements see ,?1anna (?a74].
S.22.Definition: T			??esconditiona?iv if it can be provcd
to terminate under the assuaption that it does not become blocked,
S.23Theoren: If T is a cobe?in statement ins GPL or I:PL program
S which cannot be blocked, and T is not a component of another
parallel statenent, T terminates if each of its primary components
terainates conditionally.
134
Proof: Suppost. T does not tLTT\.?nate. None of its processes can
loop Lndcfinitely, so after a finie tise each one either finishes
or is hlocxed, At that point T is blocked, and since it is not a
propcr cowponent of a parallel statement, 5 is also blocked. Since
this is impossible, T must rerminate.
L-Y.an?le: Consider the producer and consueer prmgram in .e?gure 4.5,
We have already proved that it cannot be blocked, so we need only show
that the producer and cons'j;er processes terminate conditionally.
Assuming that the operations required to corpute g(A(il) do not
stop execution, the producer rust cither becore blocked or perform
M iterations of the loop and terminate. So the producer process
terminates conditionally, and the consuner process is similar, By
Theorem 5.23 the statement par f g, and thus program fg3
must terminate.
Note that in this example the producer can be blocked at "add"
when count'N . `owever, it cannot be blocked there forever, since
the consumer is not blocked and will eventially renove a unit fr?
the buffer. In ?eneral conditional termination irplies termination
if a process can only be blocked temporarily, as is the case here,
This concludes the discussion of correctness proofs ?hich include
pro?erties besides partial correctness. There are many other pro-
perties which could be considered: priority assigr?ents, progress for
each process, blockin cf some subset of the processes in a program,
etc. Many of these properties are difficult to define in a uniform
139
in Chapter 2. in conn?ction ?ith the rule of consequence). This
censiatency ir-plies that if P ? Q and P is true. then Q is also
tn:e.
Proofcf1): Induction on the structt:re of 5' If ?` is an assign.
null or w?ile statement, s' T and I) is true by ass??ption. If
5' - be?in ...			___			and by induction post(5 )
5n e,.d a oust finish 5n n
is true after a , Since poSt(Sn) ? post(S') post(S') is true
after a . If 5' is if B then ?l else S2 a finishes either
or In either case. post(Si) is true after a , and
P05t(Sj) ? post(S') . so post(5') is true after a
Proofof2): By Ler?s 6.2, 5' - succesaor(T) . Considcring nefinition
6.1. either			5'			- while a do			T'			or			5'			follows T'			in a se4uence
of			statements.			In either case,			a			finishes			T' . ma&ing			post(T')
true after			a			and postCT') k			pre(5')			- Thus, pre(S')			is true
after a
6.4(2.15)Theorem: If pre and post are assertion functions for
(p) 5 (q) . 5' a cooponent of 5 and a a computation for 5 from
a state 5o satisfying pre(S) then 1) If 5 is ready to execute
after a , pre(S') is true after a and 2) if a finishes 5
postCS') is true after a
Proof: Use induction on the length of a . If a Is empty, 1) is satisfied
because 5 is current initially and pre(5)(s0]?true . 2) does not apply.
If a a'T consider the cases for T
a) T is a:-" . Then a'T finishes T
pre(T)(value(s0,a')1?true by induction
140
postcT)XEivsiueC50,a')1?true since pre(T) ? postCT)XE
post(T)(value(50.e))=true since oxecuting x:"E assigns tho value
of f to x
ay Lenma 6.3, I) and 2) arc satisfied.
b) T - null By induction preCT)(valuecs0,a')i=true Now
preCT) ? post(T) and T does not change any variables. so
postu)ivaluecso,a))=true			Applying Lerma 6.3 shows that?l) and
2) are satisfied.
c) T is be?in T1Tn?cn? . T is current after CL' so by induction
pre(T)[vslue(s0.e'))"true			Then, preCT)[value(s0.a))=true			since
T does not chanse any variables, and pre(T1)[value(ao.o))?trUC
since pr?.(T) ? pro(T1) . Thjs 1) is satisfied. and 2) does not
apply.
d) T is if B then T1 else T2 . By induction precT)(vaiue(ao.e')J
true . If a?vsluecs0.e?))?tr?e T1 is current after o'T
Also. (pre(T) A B)(value(s0.a'T))?trUC giving pre(T1)(valuecso.C)l
"true . If ?B!valueCso.o?)]=true , T2 is current after a'T
and pre(T2)!value(a0.a))?truC . Thus 1) holds and 2) does not
apply.
e) T is while B do T1 and ?(valueCs0.a?)1"trUC . This is
handled in the same way as case
f) T is while B do T1 and B(valueCs0.n')l.?false. Then a --H a'T
finishes T . and poatCT)(Yalue(so.e))?truC since (preCT)
A ?B) ? poat(T) . Then by Leema 6.3. 1) and 2) are aatisfied,
137
syster for RPL. 1?e will show that the a.?ions a?d infcrence rules given
so far are cor?lete in a special scIse defined by Cook.
6.1.Cor.siste,.cy.
In this section we will give proofs for Theorena 2.15. 3.15, and
4.18. thus establishing the consistency of the deductive systers and
the interpreters for SL, CPL, and RPL. The proofs follow the same
pattern in all three cases.
ocouentiaiLd(??u???.
The proof of Theorco 2.15 (and also of the other consistency
theore?s) requires a rather tedious analysis of computations and program
states. A few preliminary definitions and lemmas are necessary. The
following definition gives a characterization of successor(s), the
statement which is next to be executed after S finishes.
6.1.Definition: If 5' is a component of an SL program 5 and a
primary component of the statement T then
suc:cessor(S')			- T			if T - while B do 5'
-?T'			if T - be?in ... 5'; T' ... en?
--H aucceasor(T) if T - if B then 5' else T'
if B then T' else 5'
be?in .. 5' end
if S' - 5 i.e., 5' is not a primary component of any T . 5 baa
no successor.
38
6.2.Len.oa:			If a			is a cor?utstion for an SL trograr. S and a
finishes 5			then			sjccesaor(S') is current after a
Proc..: his anounts to sho?ing that program flow in the interpreter
follows the usual pattern. Use structural induction. starting with
5			5 - In this case a cxecutes 5			and na ataterent is current
after a			)uat as 5 has no suctessor.
.?ow if 5 is a prir.?ry component of so::e statenent T consider
the cases in the definition of aucccssor(S?) . In the first two
cases. next(s.T) creates a control tree in which 5 is a son of
succeasor(S?) . Thus. when 5 is finished, succeasor(S') is a leaf
in the control tree and is curre.?t. In the l:::at case. when a finis)'es
5 it finishes T , and by induction successor(S?) - succeasor(T)
is current after a
The next lemea will be used to show that pre(S) and poatcS) hold
at appropriate times during progra? execution.			-
6.3.Le??s: Suppose pre and post are assertion f?nctions for fP) 5
and T is an assign. null. or while statement in 5 . I a is a
computation for 5 which finishes T and post(T) is true after a
then
1)			if a finishes 5'			post(S') is true after a
2)			if 5			is current a?ter a			pre(S?) is true after a
Proof: The proof of this lenr...a relies on the consistency of the
deductive systea for the data types of the program (this was discussed
143
6.10.(3.IS)Theoren: If S is a GPL progran. with assertion functions
pre and post for			(P) s (q) .			S			is a component of S and a a
compt:tation for			5 tro.,.			with			P(s0]-true , then
I)			if			5			is current after a , pre(S') holds after a
2)			if			a			finishes 5. poat(5') holds after a
Proof: By induction on the length of a . If a is empty.
pre(S)(value(s0.a)]-pre(5)[s0]-true by asauTption. and no other
s:atement is current after a . Also a does not fii?iah any statement,
so 2) does not apply. If a - a'T there are two cases to consider.
Cast1: 5' and T are from the same process. This is just the
same as the equential problem. It is only necessary to consideF tha
two new cases of T
g)			T - cobegin			coend - Then each Tj is current after
T1 ?I...,/ Tn
a T and since pre(T) ? ?A preCT1)). pre(Ti)!value(50.a)].true.
This ?ak'es 1) hold, and 2) does not apply.
h) T is await B then T . By induction and the fact that T is
___			--H			1
ready to execute after a' (pre(T) A B)(value(s0,a')1-true and
pre(T1)[valua(s0.a')]-true , since preCT) A B ? preCT1) . Now
value(a0,a'T)-execute(value(a0,a). T1) and by Corollary 6.6,
post(T1)[value(s0.e)]-true . But then postCT)(value(s0,a))-true
since post(T1) F postCT) . Applying Le??na 6.9 shows that 1)
and 2) hold.
Case2: 5' and T are from different processes. Note that if 5'
is current after a'T 5' is current for a' and by induction
144
pre(S?)[vale(a0.??)jtr?c. If T is a null if, he?in, ?h'.1e, or
larallel statenent, t?c variables have the sane val?e in e'T as in ??
so pre(S')(valiie(s0,a)]'tne			1? T is an assi:r.nent or a?aIt
staterrent (prc(T) r. pre(S?)) T fpre(S?)) can be proved (this is the
interfcrence-fr?e property). .`?w bv nduction, (pre(T) A pre(S'))
(va:utfs0,?')] true , so pre(S?)(vslue(s0,a?T)]-true
If o'T finishes S , 0			also finis.?es S , and by induction
post(S?)[value(s0,u?)]-true . O,.ce a2ajn the interference-free property
guarantees that postCS?)(vaIue(s0,eT)]?true . Thus 1) and 2) hold
in case 2.
6?1l.(3.16)Corollarv(consistencvofAO-A7forrPL): If S is a CPL
program and (P) s (Q) can be proved, it is true in the interpretive
model.
Proof: In Chapter 3.
6.12.(3.20)Theoren.(consistc?cyofASforCPL?: If S is a CPL
program and S is a reduction of S which satisfies the anxil?ary
variable rule, then (P) s (Q) is true in the model.
Proof: In Chapter 3.
TheRestrictedParallelLaneua?e.
Consistency for tho RPL deductive system can be proved in ??uch the
saLe way as for CPL.
141
6.S.(2.16)Corollary: if (P) s (q) can be proved. it is true in the
interpreti?e nodel.
Proof: Gi?en in Chapter 2. This is the basic conaistenc)' result for
sequential progra:sa.
The following coroLlary will be uacful in the discussion of GPL
progr3=?s.
6.6.Corollary: if S' is current in prograa state a and
pre(S?)(s]-tr?e then postCs')(execute(s.S')]=true
Proof: Recall from Definition 2.13 that execute(a,S?)?value(s.e)
?ere a executes S . Applying Corollary 6.S yields post(S?)
value(s.m)].true
rheGeneral?arallelLafl?us?c.
Next, we prove the consistency of the deductive system for CPL.
The first step is to generalize the definitions and lemmas of the
last section to include await and parallel statemcnts.
o.7.Definition: If S' is a component of a GPL program S , and a
primary component of T
successor(S?) - aucceaaor(T) if T - await B then S or
cobegin o+..			... coend
- successor(S?) from Definition 6.1 otherwise.
142
6.8.era: If m is a corputatlo:: or a GIL proarsa 5 . a finishes
5' , and a stateaent from the ssre process as 5' is current after a
then that statement is succ?'ssor(S')
Proof: Essentially the a:sr? 55 Lewna 6.2. There are two new cases for
where 5' is a priaary corponent of T . If T is a parallel
statemcnt, finishin4' 5, will not n?cessarily finish T since other
processes of T may still be in execution, In this case. however,
no statement from the same process as 5' is current. If a finishes
T , by induction succcasor(T) successor(s) is current in a
If T is await 5 then 5' , the interpreter executes T
indivisibly, and 5' never appears in a computation. So this case
does not occur,
6.9.lemma: Suppose pre and pest are assertion functions for
(I) 5 (Q) . and a is a coaputation for 5 which finishes T , where
T is an assien, null, while, or await statexent. If postCT) holds
after a , and 5' and T re from the same process. then
1)			if			a			finishes 5' post(5') is true after a
2)			if			5'			is current after a preCs') is true after a
Proof: 1) The same as Lemma 6.3, with two new cases for 5' . If
5' - aw.?it..,, then 5' --H T and 1) is true. If 5' - cobe?in
5 co?nd and a finishes 5' a finishes each 5, . By'
n 1
induction, CA post(5.)) is true after a , and since (A post(Sj))
i			I			i
F post(5') , postCS') is true after a
2) Saae as Lemma 6,3.
147
Also B(?'.?lue(a0,a')]-true , ani by inductian pre(T)[va1uc(s0.a')i?true
Then pre(T1)(value(s0.e)).true . since (prc(T) A B A 1(r)) ? pro(T1)
and startine T does not modify any variable values. So 1) holds.
and ,) does not apply.
Case2: 5' and T are from different?processes. Note that if 5'
is current for a'T (or a'T finishes 5' ). S' is current for a'
(or a' finishes 5' ) and by induction Pre(5')(value(s0.e')]?true
(or post(S')[vslue(s0,a')]?true ). By Le?a 4.14. T does not
change a variable in ?roof-var(5') so pre(5')[wslue(s0.a))?true
(or post(S')(vslue(s0,e)]?true )
Finally, we must show that 3) holds. Let T' be the parallel
statement in which r was declared. If T' is not in execution for
a1T 3) does not apply, so assume T' is in execution for a'T . If
? Is current for a Pre(T')[value(s0.a)]?true and 1(r).
[va1ue(s0.o)]?true sinca pre(T') ? 1(r) . If not, T' is in
execution for a' and by induction, 3) is satisfied for a' . There
arc two ways in which a'T could fail to satisfy 3).
a) T changes a variable which is free in 1(r) . But in this case r
is busy in a'T so 1(r) does not have to be true.
b) a'T finishes a critical section for r i.o., T nakes r not
busy. But then from case 1 above, I(r)(value(a0,a)]?true
6.1?.(4.20)Corojjarw(consistencvforRPL): If s is an RPL program
and (P) s (Q) can be proved, it ia true in the interpretive model.
,yA,
148
Proof: In Chaptcr 4.
The consistency results of this section imply that if fP) s (Q)
can be proved. it is true for the interpreter. If the interpreter is
a good model of parallel e?ecution on a resl osehine, then the deductive
systee is also valid for real eachines.
There are several ways in which a real in.ple.?entstion night differ
from the interpreter. The rost fur.?anental is that the interpreter does
..ot allow true parallel execution, but siulates it by nondeter:,snis:.
In this respect it is a model of nultiprogrs??ing, but not of cjlti
processing. In Chapter 3 and 4 we have argued that the languages GPL
and I?L are defined in a way which guarantees thst nondeterninism and
parallelism ive the saae results for all prosrama.
A second possible difference is in the treatnent of expresslons
which are normally considered to be undefined, such as those involvin:
division by zero; this was discussed in Chapter 2. The interpreter
gives these expreasiona an arbitrary value, but it would also be
reasonable to stop execution as Soon as such an express?on was encountered
The axioms and inference rules are also consistent with this treat:ent
of the problem. since any?fornula (P) s (Q) Is true if S does not
terminate.
A third area in which a particular implecentation might differ
fro?. the interpreter is by speefying in more detail the way parallel
processes are scheduled. For example, processes which are cor?eting
for a resource might be guaranteed to receive it on a first-cooe, first-
145
6.13.nefinition: If S is a componcnt of an RPL program 5 and
a primary co?ponent o T
successor(S?)			succeasorCT) if T is resorce rrm
cohetin ...			.. coend
or with r when 8 do 5.
succcssor(S') from Definition 6.1 otherwise.
6.14.Lem,s:			If a is a cooputation for a GPL program 5			which
finishes 5			and a statement froa the same process as 5'			is current
after a then that state?ent is succcssor(S') -
Proof: As in Lenma 6.8. conaidcr the cases for T , where 5' is a
pri?sry corponent of T . If T is one of the five sequential
stste?.?nta, or a cobe'in statement, the proof is the same as Lemma 6.8.
If T is wit', r when 8 do 5' , a finishes 5' , and by
induction successor(S') - succesaor(T) is current after a
6.IS.LeT.. Suppose pre. post, and I are assertion functiens for
(P) 5 (Q) and T is an assignment. null, or while statement in 5
If a - a'T is a computation for 5 which finishes T , and post(T)
holds after a , than
1)			if			a			finishes 5' . post(5') holds after a
2?			if			5'			is current after a , preCS') holds after a
Proof: I) Consider the cases for 5' . If 5' is assign, null,
while, berin, If, or cebeein the argument is the same as for Lemma 6.9.
146
If 5 is ?ith r `hen I :0 ?io+ a finishes ?i and by
1n?L?ctson p3St(S1) holds after a . Since post(S1) h post(s?)
post(S') hol?s after a
2) `same as for Le??a 6.?.
6.16,(4.l.?)Theoren: Suppose 5 is an RPL proersa, and pre. post, and
I are assertion functions for (P) 5 iq) . If a is a co?putaticn
for 5 from state 5n with P[a0]?true then
1)			if			5'			is current after a preCS') holds after a
2)			if			a			finishes 5' post(S') holds after a
3) if resource r is declared in a statenent which is in execution
for a and r is not busy for a 1(r) holds after a -
Proof: ly induction on the len?th of a
If a is empty. pre(S)[value(a0.a)]?true by assuaption, and no
othcr atate?ent is current in a - so 1) holds. a does not finish
any statements, so 2) does not apply. If 3) applies, 5 must be a
parallel stateoent in which r is declared. and 3) holds because
pre(s) ? 1(r)
If a aT we first shod that 1) and 2) are satisfied. Consider
two cases:
Case1: 5' and T are from the same process. This is the same as
case 1 of Theorem 6.10 if T is cobe??n or one of the five sequential
statements. The other possibility is that T is with r when B do
After a , T' is current. Since T is ready to execute after
a' , r is not busy for a' , and by induction I(r)(valuc(s0.a')]-tn?e
ISI
for GPL and SL are also relatively complete but that will not be proved
here.) As a first step we prove relative completcness for programs
in a language which contains the n.?tural nuabcrs with <,-..,. .?nd
(concatenation, to be defined shortly). The language I. used for
assertions in a program proof will be the first-order predicate
calculus language whose nonlogical syabols are
Concatenation is an operation which is useful for representing
sequences of natural nuabers: it is included in the progra?ing
language operations because it will be necessary to introduce auxiliary
variables which store sequences.
0.55.uCtinitlon: The operation of concatenation, written xIJy , is
defined by
xIJy			lO-x o+ 2			if y			0
- (lO*x o+ 1)1 (y-l) , otherwise
A rinite sequence n1,n2 nk can be represented by tho integer
(?.?((0IIn1)I?n2)...)IIn? . here each nuaber n. in the sequence is
represented as n. l's followel by a 2. For examplo, the sequence
2,0,4 is expressed as
((0I?2)II0)I?4 --H 112211112
Note that 0 represents the null sequence.
6.19.Theoren(Relativecomplete.??ufRPL): Let T be a program in
a version of RPL whose data domain is the natural numbers with <,?,..`, and
`74%
152
L?t			he			?on.;?lctc p?u?f syste. for t:?e natural nunbers
(D will not be ?ffecti?'e). Then if (P) T (q) i)L rue in the inter-
pretive nodel it can be proved usinp D and AOA.?.
Prouf: Sections i.2.l.6.2.3 are devoted to a proof of this theorem for
t??e case in which T contains at float one cobt?in statement. If T
contains more than one cobe?in the principle is tl:e st?e; although the
details are more corplicaced. The approach used in the proof is
outlined below:
6.2.1. Construct a progran. T by sdding auxiliary variables to T
Show that (P) T (Q.? is true in the interpretive model.
6.2.2. Define pre post and I for T.
6.2.3. Show that pre. post and I are assertion functions for
(P) T- (Q) which implies that (P) T. (Q) csn be proved.
Then AS can be applied to remove auxiliary variables. givin:
a proof of (P) T (q)
The crux of the proof is defining assertion functions preCS)
post(s) and 1(r) which depend only on the variables in Proof-var(s)
and .mroof?var(r) . respectively. In program T which contains a
single cobe?in statenent T0 -
L			resource r
0 r?1: cohe?in L1: T1 /?.../? L?: T?, coend
Proof-var(r?) - (x: x is not assigned a value in T0 except in a
wit?hcn statement for r-)
Proof-var(s) - (variables of T) if 5 is not a proper corpenent of T0
149
served basis. Such an implementation is consistent with the interpreter.
so it is also consistent wit.? the axioas anci inference fl.les.
All of this suggests that the dcductive system accurately
describes the behavior of parallel programs when exccutcd on a real
?achine. To prove that this is true for any particular machine requires
a proof that the implementation of the language on that machine is
correct with respect to the semantics defined by the interpreter. Such
a proof would be a major undertaking, but a aimilar result has been
obtained for the implementation of a sequential language [?i72)
0..?orT)Ieteness.
The last section established the consistency of the deductive
system and the interpreter; now we would like to show that the deductlvc
system is also complete with respect to the interpreter. Unfortunately
we cannot hope to do this in ceneral, as the following e?ample shows.
If the progra::??ing language SL operates on data types which
include the natural nur'?ers and the standard operations on them, it
can be used to encode a Turing machine. Let 5 be a program which
encodes a Turing machine that does not halt on any input; then 5
does not terminate from any initial state. ?or such a program
(true) s (false) is trivially true. The set of Turing machines which
do not halt on any input is not recursively enumerable, but the set
of?provable formulas is, so in general (true) 5 (false) cannot be
proved.
Although the deductive aystem cannot be complete for any programming
language which includes the integora, this does not' necessarily mean
ISO
that t.?e a\.ioms and inference rules arc inadequate for describirt the
pro?rarming lan?uaee. Part of the preblen is the fact that there is
no conplete first?order deJuctl?'e systen for the natural n?bers.
Recall the fore of AO (the rule of consequence)
(P.)s(?`;pFP?.fl'?Q
Au:
iP) 5
In order to usc this rule, it is necessary to prove 1" fran P and
Q from Q, using sore deductive syster 0 for the data types of
the prollra.?sing language. hen we presented AC in Chapter 2. we rade
no ass?n.ptions about the choice of n except that it is consistent
with the data types of the language. 0 cannot be coeplete if the
?ata types include the natural numbers, by the Gbdel into--H.?pletenesa
theorem, so the incumpleteness of the deductive syste.. for prosracain:
languages is not surprising. ow suppose 0' is some complete
proof systen for the data type? of the language (in general 0, will
not be effective). If using 0' in AO yields a c?-.plete proof
system for the progr?Thrning language, we will say that the original
deductive system is relativelvcorilete. Relative completeness suegeats
that the axioms snd inference rules give "enough" inforation about
progran execution, and that the incorpleteness of the deductive
system is due to the incompleteness of D This approach is due
to Cook (Co7S), who used it to prove the relative campleteness of a
deductive system for a sequential language.
In this chapter we give a proof of the relative coepleteness of
AO.A8 for RPL programs with a wide class of data doisins. (The rules
iss
precedes 81, or 81 precedes Al. or their execution overlaps. The same
is true for A2 and 82, so the 6 posaibilitica in Figure 6.1 represent
all of the interesting cases.
In order to prove (true) Aor? (Afirst"l v lfirat"l) , it is
necessary to add auxiliary variables to Aor8. Figtrc 6.2 shows the
sug?ented progran Aor8' and Figure 6.3 givca th? final variable values
for the six conputations of Figure 6.1. N?te that the final values
of the variables Altiae Altine Iltice . 82time make it >ossible
to reconstruct the order in which atatenents were executed. The rule
is that if xti:e<?tiee . stateaent x was executcd before statement y
If xtice-ytine the two statements were executed at about the same
time, with the exact order irrelevant. In the first computation.
for exarple. we can tell that Al was the first statement executed,
and it was followed by A2, 81, and 82 in that order. For the second
co:putstion, the final values show that Al was executed before Al
and 82, and that 81 preceded A2 and 82. We cannot tell whether or
not Al preceded 81, or A2 preceded 82, but this is uninportant because
the final variable values are the same in any case.
Figure 6.4 gives some assertions for (true) Aorl'(Afirst-l V
8first?l) The reader can verify that they are correct. This is
quite straightforward except for showing that (postCA) A post(8) A
I(rl) A I(r2)) ? (Afirat.l V Bfirst--Hl) . To verify this, asaumo
(poat(A) A post(8) A I(rl) A ICrI)) This inplies:
1. A2t?me>Altime A 82time>8ltiae
2. Alti'e?B2tlmo A 8ltime?A2time
156
AorB : b?rir
Atime:??tine:?r1ti?e:?r2tir..e:?O;
AItime:?A2tin.o:?Blti;no:?82ti?e:.O;
doneAl :?doneL1 =0;
re?ourcc rI(doneA1.r1tirne),r2(done?1,r2ti:r.e).
cobepir
A: bc?ln
Al: with ri do
bein Altine:=1.nax(Ati?e?r1time);
Atin.e:=rltioe:=Altire;
doneAl:=1
end
1/
end
A2: with r2 do
bc?in A2t?:ne:=i?oax(Atime,r2ti?e);
Atioc:?r2tioe:.A2tiee;
8first:"done8l
end
end
8: begin
81: with r2 do
be?in eltine:=1.?ax(8tine.r2tiee);
Bti?e:-r2time:.8itime;
doneBi -i
coend
end
82: with ri do
be?n 82tirr.e:-i.?ax(Btire,r1ti?e);
Bti:re:-r1tirne:-82ti?e;
Afirst:-doneAl
end
end
Figure 6.2. Prograz? Aor8?.
153
Proof?var(T?)			(a: no statement of Tj			? 6 k			assigns a value to a)
Proof-var(S) - Proof-var(T?) ? (			u			Proof-var(r))
5 a proper component
ot a ?itI?hen for r
The details of the proof depend heavIly on the operation of the flPL
interpreter. and the reader may wish to review Section 4.2, especially
Definition 4.4 to 4.10.
Section 6.2.4 considers the implicationa of the relative complete-
ness theorem, and shows how it can be broadened to apply to the
standard pro?rar?ing language data types.
6.2.1.Therru:???
In this section we will define a program T. by adding auxiliary
variables to T . Before describing the general construction for T-
however, we present a simple example which illustrates the techniques
involved.
Ex
?nan"ie-o+TheProtram,?or?.
Consider the progran AorB in Figure 6.1. For this program
(true) AorB (Afirst-l V Bfirst?l) is true in the intei?retive model,
because any computation aJat execute Al before B2. setting Afirst-l
or Bl before A2, setting Bfirst-l . This is illustrated in Figure 6.1
by listing several computations and the final variables values in each
case. ?.`ote that not all coaputations are included. since Al and Bl,
as well as A2 and B2, can be executed in parallel. Since Al and ni
have no variables in coanon, the results are the same whether Al
6,
114
AorB: hein doneAl:-done8l:?O;
resource rl(doneAl) r2(done?l): cobe2in
A: be?in
Al: with ri do doncAl:?l;
A2: with r2 do 5firat:-?one8l;
end
end
Computation
1.			Al			A2			al			82
2.			Al			81			A2			?2
3.			Al			81			82			A2
4.			81			Al			A2			82
1.			81			Al			82			A2
6.			81			82			Al			A2
8: be?in
81: wit: r2 do donell:--Hl;
12: with rl do Afirst:-doneAl;
co?nd
linal Values
Afirat			Ifirat
1			0
I			1
1			1
1			1
0			1
?igure 6.1. Program Aor8 and Sevcral Co?putations.
159
3.			B2time>Altir.e			Afirst-l
4.			A2ti?e>Bltime			Bfirst-l
Aasu=?e AfirstAl . Then from 3 and 2, Altime>i2time from I,
A2time>BltiDe and from 4, Bfirst-l . Thus,
CPostCA) A post(B) A I(ri) A 1(r2)) ? (Afirst-l V Bfirst-l)
The use of variables in the proof is legit?mate, since
Proof?var(A) - (doneAl,Bfirst,Atin.e,Altime,A2tirne)
Proof-var(B) - (doneBl,Afirst,Btime,Bltime.B2tlme)
Proof-var(rl) - (doneAl,Afirst,rlti?e,Aitime,B2time)
Proof?var(r2) - (doneBl,Bfirat,r2time,Bltime,A2time)
The auxiliary variables Altime ... B2time arc particularly useful
because each belongs to the proof.variablea of a process and a
resource. Thus Altime for example, can be used in pre and post
assertions for stateaents in process A , as well as in ICri) . Since
the "time" variables encode enough information to determine the order
of stitement execution, they make it possible to prove that if Al did
not precede B2, BI must have preceded A2.
TheDefinitionofT"
The construction of an auc,,ented program T- for an arbitrary
proarsi T conta'ning at most one cobe?i'n statement is accomplished
by adding two l,inds of auxiliary variables to T . The firat type are
ti?e' variables. like those in AorB' the second are "history"
variables, used to record the values of program variables at ?ey
poimts during program execution.
160
?.`u.cfinjt?on: Rccall that program T of Theore: 6.19 has at
most one cobe?in?statement T0
L0: resource rr??: cobe?in L1: T1 ?I.../I L?: TN coend
Let 5 be any component of T			Then
rescurces(S) - ?r : 5 is a prop?r corponent of a withwhen state-
ment for r?)
var(S) - (variables or T) if 5 is not a proper conponent of T0
- (x: a does not appear on the left side of an asaign:ent
stateaent in T.			i 6 k), if 5 - T
1			1
- var(T?) tj (			L'			r)			if 5 is a proper
rresources(5)
component of Tk
Note that var(s) is the set of variables which nay legally be
used in 5 according to Definition 4.3.
6.21.Definition: The auxiliary variables to be added to the program
T of Theoren. 6.19 are defined as follows. If T contains no parallel
statement then T re?uires no auxiliary variables. If T co-tains
the parallel atateaent T0 -
L0: resource rrM: eobe?in L1: T1 /?.../? LN: TN coend
the auxiliary variables are:
157
o ? ?			? < <
?
ls?
(true) bc?jn
Atiee:-Rtin?e:--rltiee:r2tiT.e:Altin.e:-A2tir.e:--HBlti--He:--HB2ti:e:--HO;
doneAl :=done?1 =0;
(all variables havo the value 0)
resource rl(dont:Al,rltine), r2(donell,r2ti=e): co?e-in
A: (Altiee=A2tirc??tine?O)
bt?in Al: with ri do
be?in Altine:=l.max(Atire?rltifle);
-Ati?c:=rltir.e:--HAltime;
doneAl:-l
end
(A2tjrnc--O A Atime=Altirne>O)
A2: with r2 do
begin A2tirne:--l.;nsx(Atiine.r2ti:ne);
Atir.e:=r2tir=e:=A2ti:e;
B?irst:=?oneBl;
end
(A2t?rne=Atin.e>Altime>O)
end
(A2tin.c>Altine>O)
I,
(Bltirn?=82time=Bti?e=O) B (l2time>Blti?e>O)
(processes A and B are svtaetric)=
coend
(Afirst?l V Bfjrst=l)
end
(Afirst-1 V Bfirst=1)
I(rl) --H ((Altirne>O			doneAl=l)
(Altimc?B2tiee --H both
l(r2) --H ((Dltirne>O ? doneBl-l)
(A2time-lltimc both
A (rlti;ne?Altine A rlti.--H.e>l2tire) A
are 0) A (l2time??ltimeO Afirst--Hl))
A (r2tiee>lltjrr.e A r2tiae>A2ti?e)
are 0) A (A2ti?e>Bltime>O ? Bfirat-l))
Figure 6.4. Informal Proof of (truc)AorB?(Afirst-l V Bfirat-l).
163
clear as the proof proceeds. For now, note that part of their useful
ness stems fro the variety of assertions in which they can appear:
L0initial x belongs to Proof?var(L,?) l<k<N , and Proof-var(r?)
since it is not aodificd at all insido the cobe?in
stateacnt T
L history x where L is a wi'hwhen statement for resource r. in
pracess Tk belon?s to Proof?var(T?) and Proof-var(r.) since
it is changed only inside the statement L
The variables added in creating T" are auxiliary variables, as
they satisfy Definition 3.17. This acans that (?) T (Q) can be
proved by first proving (P) T fQ) and then using A? to remove the
a?ded stste:ents. The following theorem shows that (P) T" (q) is
true for the interpretive :odel.
6.:3.Throren: Let AV be an auxiliary variable set for an ?PL
program s' S be a reduction of s' with respect to AV , and P'
and Q' be assertions which do not contain free any variables from
AV . Then if (P') s (Q') is true for the interpreter, so is
(P') s' IQ')
Pro?f: This is the converse of Theorem 4.19, and the proof is very
similar. We nust show that if P'(s0]-true and a' executes S'
then ?`(value(s0,a')]?true . Given a' which executes S' , lot a
be a computation for a which is like a' except that the statement
recoved from S' is removed from a' . ?ow a and a' have the same
flow of control and the same effect on the variables In P' and Q'
y,.
164
(see I.e?r.'a 3.lcJ). Then P'[s0)-true Q'(value(s0,o))?true (because
(P?) s' (Q?) is true in the model), and thus 0 (value(s0,e')].true
?o (P') s (Q') is true in the interpretive rodel
6.24.Corol?arv: (P) T (Qi' is true in the interpretive eodel.
Proof: (P) T (q; is true for the interpreter, and T can be obtained
fron. T. by repeated r'-d-jcrion steps.
6.2.2.TheFuncti?.-,,?pus?,sneirorI
Lavine constructed the P?0?r5n. T , our ne.?t step will be to
define assertion functions for (P) T (qI . ?irst let us consider
a statenent 5 which is not a proper cocponent of the cobegin
statenent.
6.25.Defin1?son: Let a be a conponent of T' , but not a proper
conponent of a cobein statement. The predicates pre?(S) and
post'(S) defined on progran states are
pre'(S)(s) 5 a a progran. state 5o and a corputation a for T
such that P(a0,l?true ard 5 is current after a and
x[s]"x[vslue(s0,a)] V x
post?(S)(a) 5 a a proarsI. state 5o and a conputation a for T.
such that P[a0)"true and a finishes 5 and
x(s]-x[value(s0,e)) V x
Informally, pre' (5)(a) is true iff it is possible to start T
with P true and reach 5 with variables as given by state a
I)
161
I.			LItiCLti0e - used ike At?mc and lltinc in the program
Aor?'
2.			r1tir			o+?cine -- usc like rltiwe and r2time in Aor?'
3. for each variable x in T . L0initislx -- recorJs the value
of x at the beginning of statemcnt L0
4.			for each statement in process Tk with the fort			L: with r w?en
8 d? S1, and each variables xcvsr(s1)U (L?timcritimC)
Lhistorvx -- records the sequence of values of			x at the
beginning of each execution of L
Of course it is sss'L9.ed that none of these variables occur in the
original prograr.. If this is not true, some variables must be renamed.
?.22.ue:'in?t1on: The program T. required in the proof of (P) T (Q)
is obtained by adding auxiliary variables to T as described below:
1. if T contains no cobegin staterent, T""T
2. otherwise replace the cobe?in statement
L0: resource rrM: cobetin L1: T1 //...?? Lw: TN coend
by
be?in r1tinm:?r2time:".-. :-r,?time:?0;
L1tioe:?L2tine?--H `?L?time:=O;
L history x:-0; (for each L history x of Definition 6.21)
L0initial x:-x; (for each xevar(T))
resource r1C... ,r1tine)			r,? (			r?,time)
cmbeein L1: T1"			.../? L?: ?" coend
end
162
tere Tk is the result of addine auxiliary variables to Tk
.?cxt, replace each ataterent L.th r. w:1?n a d			in
3 --H			0 ?l			procesa Tk
by
becin Lktir..e:*l?nax(L?tine?rjtine);
L history a			L history a			x; (for each xevar(S1.))
r?time:?Lktime;
end
here ?i* is the result of adding auxiliary variables to
The time variables are used as they were in AorB' to give inforration
about the order ifl which critical sections are executed. Setting
Lktimc*1*r.ax(L?tine?rjtimC) records the fact that L was started after
any critical section which has alresdy been started in procesa Tk
and after any other critical section for r. which has already been
executed. Because may contain a witwhen statenent for anot?er
resource, Lktime is updated before starting ?1 Since no other
with?hen for r. can be started until L is finished. r.time is
3			3
updated after , 3ust before releasing control of r.
The L history and L0initial variables are used to record
variable values at key points. L0initial x ia the value a had when
the most recent execution of the cche?in statement L0 began.
L history x contains the sequence of values assued by a at the
beinning of each execution of statesent L (in the noat recent execu-
tion of L0). Tho purpose of introducing these variables will becomo
167
2. for l<1<n
a. S. is current in 5i-I
b.			if S. is ?ith r when B do S			B(s.]-true
1			--H
c.			s?.next(si?1 Si) except that if x ? var(S?)			X!5j) may
ts?e on any value
If B is a local computation. let value(?)?sn
Note that a conputation and a local computation are vary si?ailar.
There are 3 main differences.
1. In the local conputation. 2c allows the values of nonlocal variables
to chance arbitrarily. reflecting the fact that other processes may
nodify their values while Tk is beinr executed.
2. In a corputation for T? each state a. is uniquely defined by
s??nextCs?.1.S?) so the coaputation is detcrmined by the initial
state and the sequence of statenents. In a local computation. a. is
not uniquely determined by 5i-l and 5. , so the local computation
consists of a sequence of ststeaents and program states.
3. In a computation, S? must be ready to execute (Definition 4.6) in
In a local computation 25 and b are sinilar to "ready to
execute", but it is?not necessary to require that r is not busy. since
we are only considering the execution of a single process.
If a is a computation for T it is always possible to derive
a local conputatlon for process Tk which executes the ststemen:a of Tk
in the same order as a . But it is not always possible to find a
computation for T- consistent with a given local conputation for Tk
168
TIls is because Jefinition 6.27 rnay allow nonlocal variables to
assume val?es that never could arise in a real cor?utation.
6.2?.l)cfiniti?n: A local corputation a for o+Tk 15 scce?table iff
its i,.itial state 5c has pre(T0)(a0].true where T0 is t?e
parallel state.?cnt of T- . This inplies that it is possible to
start T with P true and reach the beginning of Tk in stato 5a
A local coeputation contsir.s only ataterents frec one process. A
related concept is the resource cor.putatien. which contains only
ataterenta which operate on a particular resource.
6.29. Definition: A resourceeo??utatson ? for a resource r. is
a			(S1,a1)			s. is a progran
sequence ?o			(Sn?Sn)			Ojn			where			1
state O<i?<n S. is a corponent of a withwhen stateaent for r
l<i(n			and
1. the control state of 5a is empty
2.			if 5. is L: with r. when 8 do S			l<i<n
I			--H
a.			the control of			5??? is empty
b.			the co?trol of			a. is the single node 5
c.			x[s1)?x[si-i? V			xcr
3.			if S			is not a withwhen statement for r3.			l<i<n
1			--H--H
a.			S. is current in			5i-i
b.			if S. is with r			when 8 do S B(s?).true
c.			s??nextCs??i?e?) except that if x ? varCsi) xfsil say
take on any value;
If ? is a resource computation. let valueCy)=sn
165
Post?(S)(s) is true iff it is possible t start T* with P true and
finish 5 with variables as given by state s
N'?w pre and post as defined above are recursively enurnerable
predicates, and as such can always be expressed as first-order formulas
in the lan?uage L whose nonlogical symbols are
6.26.terinition: For 5 a component ??, T' , but not a proper
co?ponent of a cobegin statement, let pre(S) and post(s) be first-
order foroulas of L which express the predicates pre'(S) and post'(S)
1.0.,
preCs)(s] a pre'(S)(s)
post(S)(s? a post'(s)(s)
Pro and post as given above satiafy the definition of assertion
functions (:)efinition 4.lS). As an ex.?9.p1e, consider the case where 5
is the assiennent statenent y.'-E . Part 2 of Definition 4.15 requires.
that preCs) F poat(5)??, The first step in verifying this is to show
that pre(s) po5t(s)X? . Let a be a state with pre(5)!s]-true
Then pre'(5)(a) is true, and
? 50,e such that P(s0].true and 5 is current after
a and x[s]-x(value(s0,o)) v ?
Since 5 is current after a eS is a co:putation, and valuoCs0,eS)-
Value(s0.e)<yiE? . Then aS is a coaputation which finishes S and
X(valuo(s0,e5)]?x[value(a0,a)<yJE?]?x(s<yjE?) V x Ziving
166
post?(s)(s?y:L>)?truo			Thus pre(s)[s]			post(s)[s<y??]			or
pro(s)			post(s)?
Since pro(s)
P05t(S)r: is true for the natural nur?ers
pro(s) ? post(S)?; using D' the cor?lete proof systen? for the
natural njn.bers of Theorern 6.19.
This definition of pro and post is not acceptable for a statenent
5 which is a proper co?ponent of a coberin state:ent, for then pre(s)
and post(s) can only refer to variablos in Proof-var(s) In order to
define pro and post for such statenents ?e need the concept of a local
comlutation for the parallel process containing 5 . Consider a
conputation 0 for the progran. T If a is the subsequence of a
consisting of all staternonts frea process Tk 8 can be called a
local co?putation for Tko+ but where 0 uniquely deter:,ines the
final values of tho variables in Proof-var(T.) a does not detertino
the values of variables in Proof?var(T?) because those nay depend
on the value? of resource variables which are changed unpredictably
by other proceases. For this reason a local co?..putation cannot be
just a sequence of statenc.nts but must be a sequence of statecents and
program states. More foreally:
6.27.Definition: Lot Tk be one of the parallel processes in
program T . A lecalcoinnutation 8 for Tk is a sequence
5? (51.s1)			?5n?5_?			O<n			where s? is a progran state, Ojien
Sj			Is a component of Tk .			l-<i'n and
1.			the control state of a0			contains the aingle node Tk
171
post?(S)(s) a The state a is compatible with some local comput.?tion
which finishes 5 If 5 is 3 propec component of a
withwhen statement for r a is also compatible with
some reso-jrce conputation for r which finishes 5
a The state a is compatible with some reso?rce computation
which is not in the midst of executing a critical scetion
for r
Since pre?(5) . post' (5) and I'(r) are recursively enumerablo
predicates. they can be expressed by first-order formulas in the
lan:uage L containing the nonlogical symbols (<.?...*,II.D.l....)
Moreover, the formulas for pre'(5) and post' (5) Can be written so
that all free variables belong to Proof-var(S) . since pre'(S) and
post'(5) depend only on the values of variables in Proof-var(S) -
5i:ailarly. the formula for I'(r) can be written so that all free
variables belong to Proof-var(r)
6.32.Definition: Let pre(S) post(s) and 1(r) be first-order
formulas of the language L which express pre'(5) post'(5) and
I'(r) of Definition 6.31. The free variables in pre(S) and post(S)
should belong to Proof-var(S) and the free variables of 1(r)
should belong to Proof-var(r)
6.2.3.AssertionFunctions.
The functions pro. post, and I of Definition 6.32 are assertion
functions for fP) T (Q) . In order to prove this we must show that
they satisfy DefLnition 4.15. Most of the requirements in this
172
definition hav? the ??ra P1 ? P2 where P1 and P2 are expressions
involving pre,. post, and I . In order 0 s?ow P1 ? P2 i.e., that
P2 can he ?ro??d fron. usin the Jeductive systtr. D' of
Theorci. 6.19, we first show that P1 --H P2 is a trje statet:tnt about
thc natural nuibers. Then P1 can be provcd from P2 usinz D
since D' is a coeplete proor system for the natural nu:::bers.
The following theorern shows that for each for;:ula ?l ? ?2 of
Definition 4.lS, P1 P2 is true.
6.33.Theore,: The (universal closures) of the followin: formulas
arc true for the natural numbers:
I.			P ?pre(T.) and			post(T-) Q
2.			pre(s) ? post(S)?E			for all assigi=ents			S (y':-?) in T*
3.			pro(s) post(s)			for all null 5 in			T-
4.			for			all 5 bc??'n ?l```` ;s??end in T-
a.			pre(s) ?pre(51) and POSt(Sn)			post(S)
b.			PO5t(Si) ? pre(5i-l? l<i<n-l
5.			for			all 5 if a			then else ?2			in T-
a.			(pro(s) A a)			pro(S1) and (pre(S) A ,B) ? pre(S2)
b.			post(s1) ?poat(5) and post(s2)			?lost(5)
6.			for			all 5 - while			a do ?l in T
a.			(pro(s) A a)			pro(s1)
b.			post(s1) pre(s)
c.			(pre(s) A `a)			? post(s)
169
A resource computation ? for r rcprceflts the execution or.
seqt:ence of wi?hwhen stateaents -. the only statemcnts where the
variables of r are accessible. It has thc form ? = ?l?2
where Y. is a subsequence of ? which executes one with?cn atatcacnt
for r. Part 2 of the definition des?ribes whjt happcns when a ncw
withwhen staterent L is started. while part 3 (the aa,e as 2a-c for
a local eo?putation) describes the remainder of the execution of L -
Because of 25 a new withwhen for r. cannot be started until the
previous one is finished.
If a is a co?putatioo for T- it is always possible to derive
a resource computation for r which executes critical sections for
r in the ss?e order as a . But it is not always possible to fin
a co:putation for T= which is consistent with a particular resource
cooputation since 2c and 3c allow noolocal variables to assume
arbitrary values.
6.30.E)efi?ition: A resource computation y is accentable iff its
initial state 5o has pre(T0)fs0)?true . i.e.. it is p?ssible to
start T- with P true and r?ach T0 in state
\.`ow pre(S) post(S) and 1(r) can be defined using local and
resource cooputations. The first step is to define predicates pre?(S)
post?(S) and I'(r) on program states.
6.31.Definit??. If 5 is a component and r a resource of T'
let the predicates pre?(S) post'(5) and I'(r) be defined as
foll??s. If 5 is not a proper component of the cobe'in statement
170
T0 prc?(S) and poat'(S) ar given in lefinition ?.2S. If S is
a cor.?oflent of process o+k
pre?(S)(a) a j: an acccptable loaal computat?on ? for with S
current after arA x[s)-x[value(?)] v x?Proof-var(S)
and V rcreaourcea(S) ? an acceptable resource coaputation
for r with S current after ?r and x[ai.
x[value(Yr)j V x?Proof-var(S)
poat?(S)Ca) a ? an acceptable local coeputation a for Tk which
finishca S and x[a]?x[value(S)] V xcproof-varCS)
and V r?reaourcesCS) 1 an acceptable resource conputation
? for r which finishes S and a[s)?x[value(?r)]
V x?Proof?var(S)
For all reaourcta
I?Cr?)(s) a 1 an acceptable reso?rce computation y for r with the
control of value(y) er?t? and x[s]?x[valueC?)]
V xtrroof-var(r)
These definitions can be infornallv sur?srised as:
pre?CS)Cs) a The state s is corpatible with sore local corputation
which reaches S - If S is a proper co.?ponent of a
withwhen ataterent for r a is also conpatiblo with
aome reaource computation for r which reaches S
175
Then B(a)?true A ? an acceptable local co?putation 8 for proccas
Tk with 5 current after 8 and x(s]?x[value(8)] Y xc?roof-var(S)
and ? reresources(S) ? an acceptable resource computation ?r
for r with 5 current after ?r and x[s]-x(value(?r)] v
xeproof-var(S) A ? an acceptable resource computation ? for r0 with
the control of value(?) er.pty and x[sJ-x(value(?)] v xcproof-var(r)
Let 8			8(S.s1)			where ?l is the state whose control part
is the sane as the control of next(vslue(8),S) and whose variable
part has x(s1]-x(s] V x Then 8' is an acceptable local computation
for process Tk (see 2a-c of Definition 6.27) with current after
8' and x[s'j?x[value(8')] V xeProof?var(S1)
For rtresources(S) let ?r - ?r?5,5r? where the control of
5r - control of next(valuc(Yr).S) and x[Sr]?X!sl V x . Then
is an acceptable resource coaputation for r (see 3a-c of Definition
6.29) with			and x[s]-x(value(y o+)] V
current after ?r			r
x?proof-var(S)
Finally, lot ?r0 - ??,?2? where the control of is the single
node ?l and x(s2]-x(s] v x . Then ?r			is an acceptable resource
0
computation for (see 2a-c of Definition 6.29) with 51 current
after ? and x(s)-x(value(y o+)] V xcproof.var(5)
r0			-			r0
Thus ns' and ??r' reresources(51) (-resources(S) u
which			satisfy			pre'(S1)(s) , and (pro(s) A 1(r) A 8)			pre(s1)
b.			Show			post(S1) ? (post(S) A 1(r0))
Suppose a is a prograi state with post(S1)[si-true . Then ?
an acceptablo local conputation 8 for process Tk which finishes 51
176
and x[a]?x[value(1)J ? ?tProo.C?var(S) and w rcresources(S1) a
an acceptable resource cor?putation ?r whicl finishes ?i with
x(s]=x(v.?lu?(Yr)J ? x?Proof??ar(S)
Since a ?r ??nish Sj they also finish 5 . Also. since
? finishes 5 the control of ?alue(? ) is ?r.pty. Then a an
r0			r0
acceptable local computation for process Tk which finishes 5
and x!s]=x[value(a)) v xProof-var(S) (since Proof-var(S) C
Proof-var(S1)) and v rcresourcea(S) (=resources(51) ? (r0)) a an
acceptable ?esource co.-put?tion ?r which finishes 5 and has
x[s)?x(vslue(Yr)J V xcProof-var(S) and a an acceptable resource
conputation ? with the control of valueCy ) ?mpty and
r0			r0
x!s)?x!value(Yr )i v xcproof-vsr(r0) a post(S)[a] A 1(r0)(a]
So post(S1) (post(S) A 1(r0))
a. T0 is the parallel statement
L0: reso?rce rrM: cobc?in L1: T1 ??...?? L?: TN coe,.d
a.			.?e r?st show th?t pre(T0)			(preCT1) A.. A pre(T?) A
1(r1) A...A
Suppose a is a program state with pre(T0)[s]-true . Let 5k
l<k<N be the state whose control part is the single node Tk. and
whose variable part has ?[s?]-x[s] v x . Let 1k?5k The.? is
an acceptable local coaputation for Tk ?lk has initial state 5k
and no statements executed) with Tk current after and
x[a]?x[value(0?)] v x . Thus pre(T?)(s)?true l<k<N
173
7. for all 5 - with r whcn B do ?l in T.
a.			(pre(S) t. 3 A 1(r))			pre(s1)
b.			p3st(S1)			(post(s) A 1(r))
S. for T0 L: resource rr?: cob?n L1: T1 //...// L?: TN coend
a.			pre(T0)			(preCT1) A...A pre(T?) A 1(r1) A...A
b.			(post(T1) A.,.A POSt(TN) A 1(r1) A,..A 1?r,M??			post(T0)
Pro?'.:
1.			he aust show P(sJ			pre(T?)[s]			post(T?)[s]			Q[s)
pre(T.)fs] 5 l'a,s0 such that P[s0)?true and a is a computation for
T with T current attar a and x(s]-x[value(s0.a)) V x
Letting a be epty and ?o??			gives P[sj			pre(T*)(s]
post(T.)[s? a 3a?s0 such that P(s01--true and			a finishes T			and
x[s]-x[vslue(s0,a)) V x
Q(a]			since (P) T (Q,? is true for the interpreter.
2.?6. The five sequantial statements are treated in much the asme way.
As an e?aznp1e we show how to deal with assignment statements. If
5 is y:?E we ?ust show pre(S) p05t(5)?
a. The case when 5 is not a proper component of the cohetin
state:?ent was iven earlier,
b. Let 5 be a component of process Tk. of the cobc?in statement,
and suppose s is a state such that pre(S)(s] is true,
174
pre(S)[aJ a I an Jeceptablc local compuation ? for process Tk
?ith S current arter ? arA x(s]?xtvslue(a)] w
xcProof-var(5) and for all r?resources(S) . ? an
acceptable resource conputation ?r for r with s
current after ?r and x!s]?x[value(Yr)] Y
xcProof?vsr(S)
Let s?--Hs<yJE>
8'			a(S.ncxt(vslue(e),S))
- ?r(S.next(value(?r).S)) for reresources(s)
Now 6' is an accept?ble local computation for process Tk which
finishes			S			anJ x(s')--x[value(8')] V x Proof-var(S)			(To check
that 8' is an acceptable local coaputatlon it is only necessary to
verify 2a-c of Jefinition 6.27 for the new element (5.next(value(8),S))
in the sequence.)
For all reresources(S) ` ?r' is an acceptable resource co=pJ'ts
tion which finishes 5 arA baa x!s,)?(vslue(Yr?)] V ?tProof-var(S)
(To check this. it is only necessary to verify 3s-c of uefinition 6.29
for the new eleaent of the sequence.)
8ut this implies poat(S)[s')?true . givin pre(S)[s) ?
y
post(S)[s<y?L>) or pre(S) -` post(S)
7. 5 is with r0 when B do ?l . S in process TIt
a. Assume a is a program state with (pre(s) A 3 A r(r&)(s1.trao -
179
variable L?time but if 5 is a withwhcn statement, the `time" for
5 is Cl?max(L?time?r?tiae)) which will be assigned to Lktine as
soon as the first statemcnt of the critical section is executed.
6.3S.Definition: Let a2 be a sequence of statements obtained by
terging the statements of BB?, in a way which preserves the
.th
order of atate=ents within a single 8k and puts the I occurrence
o+th
of 5 fro:: Tk before the ?			occurrence of 5' from T			if
timeCS,i.B?) < time(S'`?`0m? CSince time is nondecresaing within
o+ these two requirements do not conflict.)
We `must show e - a1Sa2 satisfies b and c from (.) . The
following lemma is the basis of the proof.
6.36.Ler=a: a - a1Sa2 is a computation for T-			with
x!value(s0.e)]?x!value(6?)) V xvsrCT?)			l<k<N
x(value(a0.m)]-x(value(??)] V xcr?
Proof: Nero we sketch the proof; a formal proof is given In Section
6.2.S. Basically. a vields the same?values as Bk for the appro-
priate variables because a2 executes statements from process Tk
in the sa:se order and with the same variable values as ?k a2 also
executes state,enta for resource r. in the same order and with the
same variable values as Y1
rt is clear from the definition of a2 that it executes statements
from T, in the same order as . To see that a2 executes
180
statC?Cnta for resource r in to same order as y. let L be a
3			3
statement with r. wh?n 8 do 5 in process T? Once L starts
3 --H 1
execution the way in which it executes is determined by the variables
in var(s1) . since these are the only variables which can be used in
The auxiliary variables L history x xvar(S1) record these
values each tino L begins execution. Because
L history x(value(??)]?L history x[s]?L history x[value(??)]
L is executed the same way in 8k and ynis is true for each
withwhen statement for r3 so a? which is derived from the 8's
contains the same statements as ?. `i.oreover. they have the sate
order in a2 sa in ?. because "tiwe" increases throughout and
statements in a2 are ordered by "tine
To see that the final values or a2 are those given in the ic=?a.
let			be an initial se?ment of a2			Let a?' and ??` b4 the
eorrespondin? initial seenents of Ik and l<k<N lJ<?<M
Then by induction on the length of a2
xtvalue(so.aiTom2,)1?x[value(8?')] v xcvar(T?)
x[valueCa0.a1T0e2,)]-x[value(Y3.')] V xtr?
If 02' is empty. valuo(so.eiToa2?)?valuecBi,)?valueCs?')?valuc(?i')
since all the 8's and T'? start with the initial state given by
L0initial x[a) . If a2 e2? where 5 is fror.process Tk
177
Next let 5' be thc prograe statc whose control part is c?pty and
variable part has x(si?x[s'] ? x			Let			lJ<?M			Then Yj 15
an acceptable resource conput?t1on tor r. (y ha initial state a'
3			3
and no stateeant'. executed) with control of value(%) empty and
x(a]?x[value(Y?)J ? x			Tha gives l(r.)[s]?true			lj<?<?			So
pre(T0)			(pre(T1) A?..A pre(T?) A 1(r1) A...A
b. We must show
(post(T1) A...A poat(TN) A 1(r1) A...A I(r?)) ?post(T0)
Suptoac a is a program state with
(post(T1) A...A postCTN) A 1(r1) A..?A l(r>))(s)?true
Then fro			post(Sk)(s]			l<k<N			2 an acceptable local computation
which finishes 5k and has x[s]=x[value(??)i V xcProof?var(T?)
Fro			I(r.)[s]			lJ<?<H			a an acceptable resource corputation
with the control of valuecy.) empty and x[s]?x[value(y.)] V
3			3
XProof.var(r?)
To prove postCT0)(s] we need a0.m such that
(.) b. a is a computation for T- which finishes T0
a0 and a can be derived froa
First. to find a0, let ?l be the initial state of the local
coaputation al (any ?k l<?<.? would do). Since B1 is
178
?cceptab1c. pre(T0)(s1l?truc i.e., ?s0,a1 such that P[s0I,?true
and al is a compJ'tation for T. with T0 current after a1 and
x(s1]a(v?lu?Cs0,a1)) V x
This yields 5o which satisfies a) above. For a tale e -
a1T0a2, where a2 is &?tained by trereing the staterents or
a1,....i . Bccause of the auxiliary variables in T' it is possible
to define a2 so that the aJbsequcnce of a1 consisting of statenents
fror.' process Tk cont?ins tr.e same stste?nents ?? ?k' while the
subsequence of a2 consisting of components of withwhen statezents
for resource r contains the 559e statements as `Y . This is done
3 3
by defining a2 by merging the staterents ofa,, in a way
which is consistent with the "time" at which statements were executed.
More for?a1ly:
a.??.Dcfini'sun: Let 6 be a computation (stan?srd, resource, or
local) and S a statement from process Tk of T.
If			s			occurs less than			i			times in			6 , tir.e?.i,6) - 0
If			S			occurs at least			i			times in			6 , let a be the progr?? state in
th
6 just after the I occurrence of S . Than
time(S,i,6)			, if S is not a withwhen statezent
if S is with
--H 3
L?timu[a]
Cl'max!Lktir?rjtimC))[s]
when a do S1.
Thus, timeCS,i.6) represents the "time" at which S was executed
for the ?th tima in 6 In most cases time is given by the
lS3
of addition, r?ltipliCation, ad Concatenation. In this section, we
Cnerali:e t?ia reault to prograns with any of the usual data t!o:nains
and then Jiscuss the significance of relative conpleteness for proofs
of proeran correctness.
Let us consider a procrain T in a language with data t??e(s)
which include a set of values A and operations (o0n? This
langLage ?ay differ from the one of Theorem 6.10 both by failin? to
include the natural nu?bers with ?<?-???".II) and by Containing
additional data values and operations.
First, auppose the lancuage does not contain all of the natural
nu:bers and (<,-, -II) . This is a Co?on caae, as most real prorram
ning languages have only a finite subset of the natural numbers and
do not include our kind of Concatenation. The power of the natural
nunbera was required in the partial correetness proof for the statements
which ?anipulste the "tine" and "history' auxiliary variables. So we
will air?ly expand the Programaing language to data types A' with
operations fo0n? by adding ?<,?.+?,,?II.o,l,,..) , with the
restriction that new operations and data values can only be used In
Statements for auxiliary variables.
If A' and (o
0m? Contain data types and operations which
were not in the prograrring language of Theorca 6.10 there are two
areas of Concern. The first is the auxiliary variable L history x
which ?ust be able to encode a sequence of values of x . l?e have
shown how to encode a sequence of natural numbers, and the technique5
can be applied to encodo any sequence of values from an enumerable
184
doaain. if A is an cnur.er?blo Set, let e:A??', be an en?eration
of the elerenta of A'			A sequence a			a, of Values froo A'
can be represented by
(... ((011e(al))1Je(a?))???)I1e(a?)
So by ad,!ine the operation e() to `?` Cagain to be used only with
auxiliary voriables), we can represent the auxiliary Variables
L ?istory x
The second problem is that it must be possible to e?tresa the
assertions prc(S) , post(s) and 1(r) as first.order foruisa oVer
t.?e donain of the prof-ran?aing lanausse. This was possible when the
lanpuage contained (<`????`,if,o,l,,.,) , because L%en t.',e assertions
represented recurai?ely enurnerable predicate5, Now if A' is an
enuffierable set, and the operations (0j?...`0m? are recursive, the
assertions for a pro?raa usin A' and (oom) are also -
recuraiwely enumerable, and pre, post, and I can be expressed as
firat?order foraulas.
This discussion leals to the following t,?eorea,
6.3sTheoren.: The proof?rul?5 AO-As are relatiVely conplete for
programs in any Version of RPL which has an enuterable do:ain and
recursive operations
Proof: The domain ?ay be extended by addina the natural nutbers,
II and e , Let D' be a complete proof system for this
iSI
because
adding 5 to has the same effect as ajding it to a
the variables on which 5 opcrates are the same in both eases.
?e observed when local and resource comnutationa were def?ned
that it is not slws?s possible to find a program computation which
is compatible with a given local or resource computation- The fact
that we can find a2 which is cor.patible with all th? eta and ?`s
is due to the auxiliary variables of T.
Given this lerma, b) and c) of (?) follow easily. b) is
satisfied because a is a computation for T. which finiahes 5
(since each finishes 5k? c) is satisfied because all the
variables of T belong to some var(T?,) or r? (see the RPL syntax
rules, Definition 4.3). If xcvar(T?) x[vslue(s0,e)]-x[valueC5?))
x[si If xtr. x(valuc(s0,e))?x[value(??)]-x[s) . So
x(value(s0,e)]-x(s] for all x in T This establishes that 5o
and a satisfy a,b.c so postu0)[s]'true . Thus
(post(T1) A...A post(Tw) A 1(r1) A...A l(r?)) post(T0)
This finishes the proof of Theorem 6.33. We next show that pre.
post, and I are assertion functions.
6.37.Corollsrv: Let D be the proof system consisting of AO?A?,
and n' a complete proof system or the natural numbers. Then pre.
post, and I of Definition 6.32 are assertion functions for (P) T' (q)
y
l.?2
Prnof: e must show tha:: pr?. post, and I satisfy pefinition 4.15.
`.?st of the criteria are easily verified, since fdr each condition
I ? `2 in the ?efinition, P P2 is true Uheorer. 6.33) so that
P e?n be proved from PI using D' . Requircoent Sc restricts the
free varibles in pre(s) and post(S) to elenents of Proof-var(S)
and this is satisfied by Definition 6.32. Similarly, Sd restricts
the free variables of 1(r) to thoic in Proof-var(r) and this
requirement is also satisfied by Definition 6.32.
6.19.Theoren(?elativeCor.nletenessofRPL): If fP) T ?Q) is true
in the interpreter, where T is a progran in a version of P?L whose
dsta domain is the natural numbers with <,-,?,-, and then
(P) T (Q) can be proved using AD?A5 and a complete proof systen D'
for the nstural nunbers.
Proof: Given T first construct a progra? T- by adding auxiliary
variables to T ma done in Definition 6.22. Then by Corollary 6.24,
(P) T" (Q) is also true for the interpreter. By Corollary 6.37,
pro, post, and I of Definition o.a? are assertion functions jor
(P) T. (Q) using the deductive syste.? 1)' . Then by Theoren. 4.16,
thcre is a proof of (P) T' (Q) using D' , and by repeated applica-
tions of AS the auxiliary variables can be reroved to give a proof
of (P) T (Q)
6.2.4. smolseationa or tne .?e.'ative ?oT.?iet?n??5 Thevre.?.
Theorem 6.19 states that the RPL proof r?lea AO-AS are relatively'
completo for pro:raaa which use the natural nuobera and the operations
187
resource ra the L history x variables rccord the value of x?rm
when L starts execution. Since L history xProofvar(T?) (1
Proof-var(r1) CL history x is chsn?cd only within L a withwhen
statement for r.)
L history x[value(a?)J?L history x[s]-L history x(vslue(?.)]
and 8? and obtain the same values for xcrm when they start L'
Thua, 6k and execute statesent L the sare nunber of times.
and esch time they start with the same variable values; this implies
that they execute L identically.
6.41.Lerna: The statements in a2 for resource r? arc in the
sane order as the statements in
Proef: The statements of e2 come from the 8k?5 l<k<? . Each
L-. with r??en B do in Tk is executed the same way in
and . So a2 contains the same statements for r3. as does.
They are in the same orler because a2 is ordered by ?time'?. Recall
that
- ?1 2			?
... v
where each ? is a subse?uence w?ich executes a withwhon statement
th
or			r. ?.ow if			5 and 5' occur in v			with the			i			occurrenco
of			5 tefore the			?th occurrence of 5.			either 5			and			5' are
a
in the same v			or time(S.i,v.) < time(S' ,k.v-)			because			r.timo is
1 3			3
updated at the end of each va . 8y Lenma 6.40. ttmeC5.i.??) <
183
tiw.e(S'			inplies that ti?c(S?i?Dm) < tine(S `1?n?			aecsuse
the ocr??ng of stateents fron S which yields a, preserves both
the order of statements from a single process and the tire order. the
th
1th occurrence of 5 precedes the j			occurrence of S			in e2
6.42.Looms: Let ?2			be an initial segnent of a2			and
lj<'<'.1 be the corresponding initial segments of . Then
1.			a			- a1T0e2 is a computation for			T
2.			a.			x(value(so.a')]=x[value(??.?)) V			xcvar(T?)
b.			if 5 is current after			S			is current after a
3.			x[value(a0.e?)i'-x(value(Y?')] V xcr.			lJ<<'.1
Proof: By induction on the lenath of 02'
If a,' is empty:
1. a' - a1T0 is a corputation for T because a1 is defined?as a
computation for T with T0 current after al
2.5. By the definition cf a1 x(value(s0.a1)]?x!vslueCS1)) V x
flow ak l?k<N is an acceptable local co=putation. so its initial-
????? 5k satisfies preCT0) This ceans that the tioe and history
variables have the value 0 in 5k and V xcvar(T) x(sk)
L0 initial x(sk] Cthe auxiliary variables receive these values ?uat
befora L0 begi,.s). Since L0 initial XcProofvar(T?)
L0 initial x[vslue(B?)]?Lo initial x(s)
l?5
extended dosin. Then the proof of Theorem 6.19 (with the op?rationa
on L history aodified as sungested abovc) becomes a proof of 6.38.
Since anY, irr.plenentable prograr?ing lsog?,?o rust op?rate over
an en?erable data dorain with recursive operations, Theorem 6.3?
ir?lies the relative coapleteness of RPL for any reasonabic choice of
data types. This seens to indicate that A0-A8 are `.0 adequ.?te set
of proof-rules in the sense that the?, capture all the information
about progran. staten.?nts that ia relevant for partial correctness. Since
AO-AS are not complete in the absolute sense, tbcre .?re programa for
which valid partial correctnest fornulas cannot be proved. Our main
interest. however. is in proving the partial correetness of proerams
%Titten by progra=ers who understand thca and why they work. In
such a case the progra?=er knows how to prove the necessary facts
about the program domain. The relative coapleteness of AC-AS implies
that in this case it is possible to prove the program's partial
correctoess.
6.2.5.ProofofLemr,a6.31.
In Section 6.2.3 we eave an informal proof of Lemma 6.31. We now
give a rore detailed proof using four subsidiary lemmas. Recall that a
is a progras state with post(T&(s]?true ?? is an acceptable
local coaputation for process Tk . with x[va1ue(B?)]?x(s] V xvsr(T?)
___ is an acceptable resource conputation for r? with the
control of vslueCY?) empty and x[value(y?))-x[a) V xcvar(y.) 50,e1
3 3
are defined in such a way that pre(T0)[value(a0.o1))-true and the
1a6
initial stazc o? a			i			va			a2 is a see?en?e of state?ents
lue(s0,o1)
obzaine(I by rr.or3ing the statcments of the ?? in a way ?hich preserves
th o+?tine' at which the atatene.?ts were execijted.
6.39.l.er?n.a: The atatement% in ?2 for process Tk are in the same
ord?r as the stateeents of
-k
r?roof: Obvious froa the definition of a1
6.40Leos: If L: ?ith r			wbcn t do S			is a statetnent in process
3--H			--H			I
Tk			L is executed in the sare way in			as in ?.			i?e.. the
subacquences of statements froi. L in			and			are identical.
?oreever, if 1k			is an in?tial seginent of			which has S			a c?ponent
of ?1 current, and y3' is the corresponding initial seleent of
o+ then
x[valueCB?o+)]?x?value(Y3.')] V xcvar(S)
Proof: .`?te that
L history x[vslue(??))?L history x(s]?L .?istory x!vai'e(y?)i
V xcvar(S1) , because L history xeProof?varCT?) fl Proof-var(r.)
This neans that 1. is executed the saTe nuaber of ti.?es in a ??
y3 and that each tino the initial variable values are the sa?e in
both computations. If L does not properly contain any withwhen
statements, this implies that L is e?ecuted in exactly the sar? way
in and , since the only variables accessible inside L are
those in var(S1) . If L does contain a withwhtn stater.ent Lo+ for
191
xfralue(s0.a")) -			? xcvar(S)			(provd in 2 aboyc)
- x(va1ue(?")] V xcvar(S) (Lenrr..3 6.40)
So S has ho sane efr?ct on variabics in a2 and yielding 3.
7)1.
CiIAPTL.? 7
CONtLUSIO.? k?D CO'.?iE.?TS
In this thesis we have presented a method for verification of
parallel programs. Our techniques are based on jIoare?a axionatic approach
r?r proving partial correctnesa. ?e first provided axior.s and inference
rules for two p?'rallel languages: a General Parallel Languaae and a
P?estricted Parallel Lan?uage. CPL is not a realistic progra?ing
language: it is introduced because it is powerful enough to represent
most of the standard synchronizing operations. Thus. the deduct?ve
system for GPL can be used to establish the correetness of a pro?raa
which uses semaphores. events, or any of the other corson synchroni:ing
tools. lJnfortunately, these proofs tray be quite cooplex because the
verification of the interference-free property requires that each
assertion be tested for invariance over each assignment state?ent fros
another process.
RPL avoids thiscomplexity by restricting the use of shared var?ables
to critical aections. so that only one process at a tine has access to
a particular variable. This gives RPL prograaa a structure which
makes them casy to understand and to verify. In proving the correctness
of an RPL program ona oust first define the invariant for each resource
(possibly adding auxiliary variables to do so). The rest of the verifi-
cation process requires only sequential reasoning, and is much siapler
than a GPL proof.
192
159
So all 6k'5 start with the sawe initial state, i.c.,
x[Yalue(8?'))?x(s?J=x!si)?x[value(s0.e?)) V x
2.b. The only staterent current after 8k' is Tk (see Definition
6.27). and Tk is also current after a'
3.			The initial state of each			lfl<'I is also identical to
value(s0,a') the proof is the sane as for 2a.
Induction step: If a2			a2'S			assume the lewsna is satisfied for 0,"
and the corresponding 8k" and y," . Let 5 belon,", to process
1 a' - a1T0a2,,S is a computation iff 5 is ready to execute after
a" --H a1T0e; . This requires two conditions to be satisfied.
a. 5 Is current after a" . Since 5 is the next statement
after 8k" in			5			is current after			Ik" (see
Definition			6.27).			By 2a			of the induction hypotheais this
joplies that 5 is current after a
b.			If 5 is with			r			when			B do ?l' r5			is not busy in a2,,
and B!value(a0.a"))-true . Since ?. finiahes one ??ithwhen
statenent hefore it starts another, and a, executes state
nents for r,			in the sane order as Yj ,			r is not busy in
3			5
a," . To see that B(value(s0,a"))?true , note that
B[value(5?')]?true by part 2b of Definition 6.2?.			?ow
x(value(soa2")]?x(value(??)] V xcvar(S) (proved			in 2 below)
"X?value(??')] V xtvar(5) since			5 does not
change any variable values.
193
xcr. (induction)
-x[valua(? o+)] ? xr. since 5 does not
J 1
chan?e any variable values
x[va1ue(a?')] V xtr, (Le?a 6.40)
So x(value(so.o2')J?x[value(8??)] V xcvar(S1) , and
B[value(?0,a2?)]?true
2.a and b. 5 has L?e sara effect in a2' as in if all the
variables in var(S) have the same values in both computations. ?ow
var(S)			vsr(T?) ? (			u
rcresources(5)
?y induction x[vslue(so.a'?)]--x(value(a??)1 V xtvar(T?) -
?or r. ? resources(S)
x[vsluo(s0.a')) "x(vaiua(y.")i			x?r.			(induction)
1 1
o+x[value(a?")] V xtr.			(Len.?a 6.40)
3. If 5 is not a component of a withwhen statement for r? 3 is
satisfied by induction, since 5 does not affect the ?ariablcs of r
If 5 is L: with r when I do ?i' 5 does not change any
variabloswhonadded to a' and a" so again 3 is satisfied by
induction.
If 5 is a proper coapanent of L: with r when 3 do
195
Finailvo+ the rcsuits of this thesis should be very applic?ble to
sutonatic P?0??51 verification. %`e visuilize an approach in which the
prQ?'rar?er ?orks ?ith an intcr3ctive Syster. ii the one d?scribcd
by GooJ, et al. [CoTS]. jo first gives his pro?ran. possibly with
a?'xi?iary ?ariables, and defines resorce and loop invariants. The
verification systeo is then left with the nechanical problco of
checling whether the invariants an input anJ output conditions are
corsiatent. It ?av respond that they. are consistent, thus establishing
the correctness of the program; that they are inconsistent, imply?ng
an error in either the program or the invarianta; or that there?is
insufficient infornation to decide. In the last case the programmer
can provide r?re infornation by adding auxiliary variables or
strengthening the invarianta.
;/ffl?
196
LIIlLIOCRAPiP'
(Aa7lj Ashcroft, E.A. and `. `inns. Forralization of Prcperties of
PafaIltI Pro?,rans. `-I:,zhi.?eIntellirence 6. pp. 17-41,
?Iniversity of Edinburgh Press, 1971. -
(As73] Asr,croft, E.A. Provin? Assertions about Parallel Prograns.
Technical Peport CS-73-Ol. Depsrtncnt of Applied Analysis and
Computer Scicncc, University of 1?'aterloo, 1973.
(?r72a] Irinch I!an?n, P. A Comparison of Two Synchronizin? Concepts.
ActsInfornatica 1. pp. 190-199, 1972.
(Br72bi Structured `!ultiprogramming. CACM 15:7, pp. S74-57?, 1972.
[?r73]Concurrent Programming Concepts. ConnutingS?'r,'evs 5:,,,
pp. 223-245, 1973.
[Br74] Co-.?current Pascal: A Prorra=?ing Languare for Operatins
5ystc?..s Ocaign. Inrorostion Sciences Technical Report 10,
California Institute of Technology. 1974.
(Cs73] Cadiou, J.M, and J.J. Ldvy. Y.ecnani-sble Proofs about PsrsIiei
Processes. Proc.l'thAnnualIFEESvmnosiuonSwitchinz
andAutor?taThco-rv, pp. 34-45, 1973.
(Co7lJ Courtois, P.J. R. leyrans, and D.L. Parnas. Cencurrent
Control with "?eaders" and "?riters", CAC' 14:10, pp. 667-668,
1971.
[Co7S? Cook, S.A. Axiomatic and Interpretive Senantics for an Alrol
Fragmcnt. Tcc?nica1 Peport 79, Department of Conputer Science,
University of Toronto, 1975.
(Di6Sal Di)kstrs, E.I'. Co-operating Sequential Processes, in F. Genuys,
cd. Pro?rss?in'Lannua"eaNATOA&JsncedStudyInstitute,
pp. 43-112, Acadc?ic Press, 1968.
[Di6lib]The Structure of the TIlE .`Iultiprogram?lng System. CAC4
11:5, pp. 341-347, 1rJ68,
!Di7O]Notes on Structured Prograr,?ing. Technical University
of Eindhoven Report Eh?249. indhoven, Netherlands, 1970.
(Di7l]hierarchical Orderin,, of Sequential Processes, in
liosre and Perrott, ed. OperatimpSystemsTechnioums, Acadeoic
Press, 1972.
193
The dejuctive systems for kPL an CPL ar. pria?L-ily int?ndc'I ?or
partial correctness proofs. `.e?ever a nuaber of ot?er propertics are
i.?port3nt for parallel prograa.'. and the inforw?tion obtaine from a
partial cerreetness proof can often be applied to vcrify that other
?roperties also hold. In Chapter 5 we showed how the pre, post. and
resource invariant assertions from a partial correctncss proof can be
used to establish mutual e:<clusion, freedom from deadlock. and ?ro?ram
termination.
Finally. we evaluated the axioms and inference rules by defining
interpreters for the languages RPL and GPL; the interpreters model
the effect of executin: programs on a real computer. The R?L and GPL
deductive systems were shown to be consistent with the interpreters.
i.e. they accurately describe the effects of program exeeutio:?. For
RPL we also showed that the deduetive system was relatively complete
with respect to the interpreter, i.e. given ade?uato knowledge about
the data donain of the program. any true partial eorrectness formula
can be proved. Thus. the axioms and inference rules do not omit any
crucial information about program e,ecution.
Our results suggest several directions for future work. One
i?portant task is the extension of the deductive system to a more
powerful programming lanuage. A major weakness of RPL and CPL is that
both are limited to' programs with a fixed degree of parallelism. Parallel
execution is initiated by the eobeein statement, which starts a fixed
m?ber of parallel processes. The addition of recursive procedures
would overcome th?s limitation. since a recursive procedure which
contained a cobe?in statement could create an arbitrary number of parallel
94
procesees. `?e con3ecture that recursi?e procedures would increase the
conplexity of part?al c?rrcctness proofs only as ruch as in the
seq?ential case, i.e., a new rule describing recursion rr.jst be added,
but no chan?e in the existing axions is necessary. However, r?tual
excl'jsion anA deadloc pree techniques ray require .?orc significant
modification.
`tore icncrslly, it is clear that neither RPL nor ?PL is a perfect
language for parallel progracnint. GPL is too powerful to be feasible
for inpler.entation, and it does not provide enough structure to aid
the programmer in organiiing his program. Although RPL is an i=prove=ent
in both these areas, the conditional critical section is still somewhat
incfficicnt as a synchrcnizing operation. Moreover, there are some
problems which do not fit reasonably into the RPL framework for
example the readers and writers problem discussed in Chapter t. There
is a need for new languae constructions which can be implemented
efficiently and which provide a basis fer organizing programs in?a clear
and easily verified manner.
Another area in which further wo?x is needed is the ?crification
of properties other than partial correetneas. Althmu'h techniqJes were
presented in Chapter 5 for pro?'ing ao:te of these properties, there are
many more to conaidey. e.g., priority scheduling and pro?ress for eath
process. Not all of these properties will be anciable to the axieratic
approach Caee the discussion at the end of Chapter 5), but the range
of properties which can be verified using this and other techniques can
certainly be extended.
197
(Di73]
Pijkstra. E.W. A Sir)1e Axiomatic ?asis for Prn'raming
Language Constructs. Lecture notes fron the International
Su??er School on Structured Programming and Prograrne? Structures,
`tunich. Germany. 1973.
(e167) Floyd. R?W. Assigning `eaning to Prograna. in Sch?artz, J.T..
ed. `atheraticalAspectsofComputerScience Proc.Syr'i'osiain
Anlieduather?tics 1.0 pp l??3 ,`n?r. `lath. Soc. 1967.
(Go7S] Good. I. R.L. London. and 11.1'. tledane. An Interactive
Protram Verification System. IF,L.TransactionsonSoft?
l1ntineerin? 1:1, pp. 59-67, 1975.
?Ia72) liabermann. A.N. Synchronitation of Comnunicating Processes.
CAC'! 15:3. pp. 171-176. 1972.
(11069] Ijoare, C.A.R. An Axionatic ?asis for Computer Programming.
CAC' 12:10. pp. 576-580. 1969.
[11o72]Towards a Theory of Parallel Programming. in bare
and Perrott. ed. Operatin?Svste?..sTechniljes. Academic Press,
1972.
(l1o74a]"onitors: An Operatin' System Structuring Concept.
CAC' 17:10. pp. 548-557. 1974.
(?o74b] loare. C.A.R. and P.E. Loner Consistent and Complementary
For--H..a1 Theories of the Semantics of Programming Languages.
ActaInformatica 3. pp. 131-153, 1974.
(La711 Laner, P.E. Consistent Formal Theories of the Sensntics of
Pregramzning Languages. 111.' Labroatory Vienna TR 25.121. 1971.
[Ls73] Lauer. 11.C. Correctness in Operating Systems. Ph.D. thesis.
Carnegie-lellon Uniersity. 1973.
[Li74a] Lipton. R.J. On Synchroni:ation Primitive Systems. P?.D. thesis,
Carnegie-lielIon University, 1974.
(Li74b]Reduction: A New l!thmd for Proving Properties of
Systens of Processes. Yale Computer Science Research Report
30, 1974.
, (`.?74] Mamma, . and A. Pnueli. Axiomatic Approach to Total Correctness
of Progra1a. ActsInfornatica 3. pp. 243-263, 1974.
(`(.172] `lilner, R. and R.W. Weyrauch. Proving Compiler Correctnesa
in a ?`.ecbani:ed Logic. yachineintellisenco 7. pp. 51-70,
Edinburgh University Proas. 1972.
198
[??74] :??t??, c. ?rovir.r, Propertics 0 Interacti?g Proccsscs.
Co.?putcr Scionce Tcchn?ca1 kcport 74-9. Univcrsity cf ?as.?ington.
1974.
(?o74) f<oacr B.K. Corrc<tncss of Parallel PrograT.?: The Churc,-
Rosaer Approaca. l.? o+?esearc.? rep3rt RCSln7. T'.:o.?as J. ?atson
?esearen' Center. Yorktown feigats. .?ew Yo?i.. 1974.
(Si7S] Sinr:off . and A. van Lar.sweer?e. Constrjcting Correct and
Effiejeit Concurrent Progra?s. Proc. Ar'.-!PEEInternational
Con?erenceonRclta?leSo?tware 197S.