Copyright
B. D Lubachevsky.

Verification of several parallel coordination programs based on descriptions of their reachability sets online

. (page 1 of 3)
Online LibraryB. D LubachevskyVerification of several parallel coordination programs based on descriptions of their reachability sets → online text (page 1 of 3)
Font size
QR-code for this ebook


Computer Science Department



TECHNICAL REPORT



VERIFICATION OF SEVERAL PARALLEL
COORDINATION PROGRAMS BASED ON
DESCRIPTIONS OF THEIR REACHABILITY SETS



by



B.D. Lubachevsky
JULY 1981
REPORT NO. 036



NEW YORK UNIVERSITY







Department of Computer Science
Courant Institute of Mathematical Sciences

251 MERCER STREET, NEW YORK, NY. 10012



mz^



Ultracomputer Note #33



VERIFICATION OF SEVERAL PARALLEL
COORDINATION PROGRAMS BASED ON
DESCRIPTIONS OF THEIR REACHABILITY SETS

by

B.D. Lubachevsky

JULY 1981

REPORT NO. 036



This work was supported in part by the Applied Mathematical Sciences
Program of the U.S. Department of Energy under Contract No.
DE-AC02-76ER03077 , and in part by the National Science Foundation
under Grant No. NSF-KCS79-21258 .



Ultracomputer Note #33 July 1981



VERIFICATION OF SEVERAL PARALLEL COORDINATION PROGRAMS
BASED ON DESCRIPTIONS OF THEIR REACHABILITY SETS



by

B .D .Lubachevsky



Abstract - A method for verifying parallel programs is applied to
several examples (PV-semaphore, "busy-wait" synchronization, "cessation
of activity" synchronization, "readers-writers"). The graph of all
program states and state transitions is represented in a special
compact form independent of the number N of processing elements. This
representation aids in verifying certain correctness properties that
can not be easily expressed in the form "predicate(state)" . In each of
the above mentioned examples a special "reachability tree" is developed
whose nodes are some subsets of the set of all reachable states. The
root is the initial state and moving down the tree corresponds to some
processors advancing their execution. In the presented examples the
size of this tree is independent of N. The notion of compact program is
introduced: roughly speaking a parallel program is compact if there
exists a boundary, independent of N, on time required to reach any
state. Examples of non-compact programs are represented.

Index Terms - correctness proof, program verification, concurrent
processes, synchronization, semaphore, liveness property, mutual
exclusion, deadlock.



This work was supported in part by the Applied Mathematical Sciences
Program of the U.S. Department of Energy under Contract No.
DE-AC02-76ER03077 , and in part by the National Science Foundation under
Grant No. NSF-MCS79-21258.



-2-
1. Introduction.

This paper considers verification problems typified by following
(incorrect) implementation of Dijkstra's PV-semaphore.

COMMENT P-section

PI: p 0) then go to P3

P2: REPADD (sem.l)
go to PI

COMMENT critical section, protected by sem

P3: {...}

COMMENT V-section

REPADD (sem,l)
go to PI

This code is supposed to be executed by all the processing elements
(PEs) of a parallel computer. In this code, sem is a public variable
accessible by each PE; initially sem = 1 ; p is a private variable, i.e.
each PE maintains its own copy of p; all PEs begin at PI; expression
REPADD( sem, constant) is used for the function-with-side-ef f ect that
replaces sem by (sem + constant) and returns the new value of sem. The
REPADD operation is indivisible in the sense that the result of
concurently executed REPADD operations is the same as if the operations
were executed in some unspecified serial order (see [5]).

It was shown in [A] (see also [5]) that after the first execution
of the critical section P3, the following unacceptable race condition
can occur: All the PEs are infinitely executing the loop between the
statements PI and P2, and sem < 0, which prevents any PE from entering
the critical section. Note that such "parallel bugs" are particulary
hard to discover so a mechanical method for exposing them would be very
helpful. Consider the following table that lists all states reachable
when a 2-processor parallel computer executes the above program. In
this table we characterize states by giving the values of sem and the
number of PEs beginning execution of each statement PI, P2, P3. (We do



-3-

not consider states in which a PE has executed part, but not all, of a
statement). For each state we also indicate the states resulting from
a PE completing execution of its current statement and moving to
another.

s^ (initial state) [PI: 2 PEs, P2: no PEs, P3: no PEs; sem = 1]
move of 1 PE from PI to P3 leads to So

52 [PI: 1 PE, P2: no PEs, P3: 1 PE; sem = 0]

move of 1 PE from Pi to P2 leads to So
move of 1 PE from P3 to PI leads to s,

53 [PI: no PEs, P2: 1 PE, P3: 1 PE; sem = -1]

move of 1 PE from P2 to PI leads to S2
move of 1 PE from P3 to PI leads to s,

s^ [PI: 1 PE, P2: 1 PE, P3: no PEs; sem = 0]
move of 1 PE from PI to P2 leads to Sc
move of 1 PE from P2 to PI leads to Si

S5 [PI: no PEs, P2: 2 PEs, P3: no PEs; sem = -1]
move of 1 PE from P2 to PI leads to s^

Table 1.1



This type of table can be produced mechanically. In fact, a formal
procedure exists and has been programmed by the author that can analyse
programs like the one given above for any fixed number of PEs. We do
not present a detailed description of this procedure in the present
paper and only briefly outline it here. This procedure, first, creates
the table of all reachable states (like table 1.1 above). Then the
procedure analyses the directed graph representing all reachable states
of the program and all possible transitions. For our example the nodes
of the graph are s-^, S2, S3, s^, S5, and the arcs are (s-^,S2), (s2,S3),
(S2,S]^), (S3,S2), (S3,S4), (s4,S5), isi^,s^), (s5,s^). Each of the arcs
corresponds to one move listed in the above table. The race condition
mentioned above appear as a strongly connected component s^->Sc->s^ of
the subgraph generated by the predicate "there are no PEs at P3" in
this graph. We will see that the well-known "finite delay property"
(discussed below) also must be satisfied by the strongly connected
component in order to generate a race condition.



-4-

We now show that the veri f icational approach started by Floyd for
sequential programs and extended ([2], [7]) to concurrent programs
would not expose the described above race condition. We can rewrite
our REPADDs as "WITH-WHEN"^ cf [7]:

p t such that some PE is in the
critical section at time t'.

While analysing this (relatively simple) program we will introduce
several techniques and notions used in subsequent examples.

First, we are to represent the concrete program as an abstract
program of section 2. The critical section "P5: {...}" and the other
section denoted (•••} do not effect the analysis. Thus we can consider
the following abbreviated abstract program.



-11-

Pl: if (sem < 0) then go to *

P2: if (REPADD (sem,-l) > 0) then go to P4

P3: REPADD (sem,l)
go to PI

P4: REPADD (sem,l)
go to PI

Note that statements PI, P2, P3, P4 in this code are of the form
(13), (17), (16), and (16), respectively.



We next show that R(sq) 3 SI U...U S5, where Si, i=l,...,5 are
the following sets (all n^ are supposed to be nonnegative integers):



51 =

52 =

53 =

54 =

55 =



q} = {s ; n^ = N, sem = 1 }
s ; n, + no = N, sem = 1 }

n, + n2 = N-1 , n^ = 1 , sem = 0;

^1 "*" ^2 "^ "3 ~ ^~^ > ^4 ~ 1 > sem = -no }

ni + no + no = N, ni > 1 , no > 1, sem = 1 - no}



Clearly, R 3 SI.

Consider the only state Sq = {n,0,0,0; l} in SI, i.e. the state in
which all PEs are at PI and the public variable sem = 1. Looking at
the code we see that in state Sq from 1 to N PEs can move from PI to
P2; such moves generate the set

S2' = js ; nj^ + n2 = N, n2 > 1, sem = l}

Note that S2 = S2' U SI and therefore all states in S2 are reachable,
i.e. rJ3 S2.



Consider those states s in S2 from which PEs can move along the
arc P2 -> P4, i.e. those states satisfying the condition n2 > 1 • Note
that in these states at least one PE is at P2 and sem = 1. Looking at



-12-

the code we see that at most 1 PE can move from P2 to P4; such moves
generate S3 and therefore all states in S3 are reachable, i.e. R 3
S3.

Consider those states s in S3 from which PEs can move along the
arc P2 -> P3, i.e. those states satisfying the condition n2 > 1 . Note
that in these states at least one PE is at P2 and sem < 0. Looking at
the code we see that from 1 to n2 PEs can move from P2 to P3; such
moves generate the set

54' = {s ; ni + no + n^ = N-1 , n / = 1 , no > 1 , sem = -no}

Note that S4 = S4' U S3 and therefore all states in S4 are reachable,
i.e. R D S4.

Consider those states s in S4 that have at least 1 PE at P3, i.e.
those states satisfying the condition n-, > 1 . Looking at the code we
see that 1 PE can move from P4 to PI; such moves generate the set 85
and therefore all states from S5 are reachable, i.e. R Z) S5.

This implies that each Si contains only reachable states, i.e.

5
(1) R D U Si

1=1

The above arguments may be abbreviated as in table 3.1.



-13-
REACHABILITY TREE

51 n-^ = N, sem = 1

moves from PI to P2 lead to S2

52 n, + no = N, sem = 1

moves from P2 to P4 lead to S3

53 n, + n2 = N-1 , n^ = 1. , sem =

moves from P2 to P3 lead to S4

SA rij^ + n2 + n2 = N-1, n^ = 1 , sem = -n2

moves from P4 to PI lead to S5, if no > 1

S5 n-^ + n2 + n2.= N, nj^ > 1 , no > 1, sem = l-n-j

Table 3.1

We will use the REACHABILITY TREE in future examples without
explicitly noting that all states represented in the table are
reachable.

The word "tree" in the name of the table is due to the fact that
the table can be viewed as a directed graph, which is in fact a
directed tree. The nodes of this graph are the Si in the table and the
arcs are pairs (Si,Sj) such that some move starting at Si "leads to Sj"
according to the table. For the semaphore example the nodes are
{S1,S2,S3,SA,S5} and the arcs are {(SI ,S2) , (S2,S3) , (S3,SA) , (SA,S5) } , so
that the tree is simply a sequence S1->S2->S3->SA->S5. For subsequent
examples the REACHABILITY TREE can be. more complex.

Recall the restriction n^ > 1 in moves from SA to S5. Let us call
this kind of restriction a branching condition . In the above example
n-j, the only variable appearing in a branching condition, does not
change in value during the move controlled by the branching condition;
but sometimes a branching condition involves several variables some of
which change in value during the move. In such a case the predicate
must be true for the states obtained after the move.

When the number of nodes in the REACHABILITY TREE is small (as is
the case for the simple semaphore program) , the REACHABILITY TREE can
be used directly as an instrument to observe the behavior of the
program. In other examples the REACHABILITY TREE is large and



-lA-

reductions are helpful. Let us demonstrate one such a reduction for
our simple example.

Consider the set of sets "i = {S2,S4,S5}. * has the property that
it is a minimal subset "of the set * = {Sl ,S2,S3,S4,S5 } such that for
any element Si of * there exists an element Sj from "i such that Si CT
Sj. In fact we have the following inclusions:

INCLUSIONS

SI C S2; S3 C S4

Moreover none of the elements from "i* is a subset of any of the other 2
elements of f. Thus we can omit SI and S3 without losing any states.

In the REACHABILITY TREE above, for each set Si that is an element
of * we only listed some of the possible moves. The following
REACHABILITY SET DESCRIPTION (RSD) is the final product of the
technique. It lists, for each Si in t, all possible moves.

REACHABILITY SET DESCRIPTION

S2 n, + n2 = N, sem = 1

moves from PI to P2 lead to *
moves from P2 to P4 lead to 84

54 n^^ + n2 + n^ = N-1, n^ = 1 , sem = -no

moves from PI to PI lead to *

moves from P2 to P3 lead to *

moves from P3 to PI lead to *

moves from P4 to PI lead to S5, if n^ > 1

or lead to S2, if n^ =

55 n^ + n2 + n-j = N, n-^ > 1 , n2 > 1, sem = l-n^

moves from PI to PI lead to *

moves from P2 to P3 lead to *

moves from P3 to PI lead to *, if n, > 1

or lead to S2, if n^ =

Table 3.2



-15-

The phrases listed under the formulas for each Si are called
directing phrases . Each directing phrase represents a class of moves
"from Pi to Pj". We say that these noves are carried by the arc Pi ->
Pj (of the graph G) or that this arc carries these moves.

The RSD is closed in the sense that all moves are to sets given in
the description; moreover, all possible moves are represented and the
initial state belongs to S2. Thus we have

(2) R C S2 U S4 U S5.

Properties (1) and (2) together give

R = S2 U S4 U S5

In subsequent examples a similar argument shows that R is the union of
the sets presented in the RSD.

The above analysis has actually involved a hidden assumption that
N is sufficiently large. For example when we considered those states s
in S3 such that n2 > 0, we tacitly assumed that N > 1 (or else no such
s exists). For each example in this paper it is easy to see that there
exists an Nq such that for all N > Ng all the required states do exist.
In particular, for the semaphore example just discussed, one may choose
Nq = 2. However, the REACHABILITY TREE and the RSD tables are actually
valid for all N > 1 if interpreted correctly. Although for small N
some sets Si are empty and some branching conditions are unsatisf iable,
no contradiction arises. This may be easily checked on a case-by-case
basis.

Before analysing the semaphore program using the above RSD let us
make the following general remarks.

Note that the RSD can be viewed as a directed graph T that differs
from both the graph A and the REACHABILITY TREE. Namely nodes of T are
those sets Si appearing in the RSD and arcs of T correspond to the



-16-

directing phrases associated with each Si. In the semaphore example T
has 3 nodes corresponding to the 3 sets S2,SA,S5 and has 11 arcs,
corresponding to the 11 directed phrases in the RSD. For example, the
r contains arcs (S2,S2), (85^55), and (S5,S2) since the phrases

moves from PI to P2 lead to *

moves from P3 to PI lead to * , if n^ > 1
or lead to S2, if no =

are written under the formulas for S2 and S5.

For the reader's convenience we summarize the graphs defined thus
far in table 3.3.





Graph




Node set




Elements of node set




G




Pl,...,Pk




program positions




A




R




reachable states




r


{Si,


[» •• • »Si^ of


RSD


subsets of R



Table 3.3



Let p(s) be some predicate over the set R of nodes of A , i.e. a
predicate over states of the program and S be a subset of R. By S»p we
denote the intersection of S with {s;p( s) = true } . By A«p we denote the
subgraph of A induced by the predicate p, i.e. the subgraph whose node
set is R»p and whose arcs are those of A connecting these nodes. The
following is a general problem when analysing our programs. Given a



^A strongly connected component c in a directed graph g is a maximal
subgraph of g such that for any two (not necessarily different) nodes
of c there exists a directed path in g from the first node to the
second .



-17-

predicate p find all strongly connected components (SCCs) in A»p. To
find these SCCs one executes the following procedure called FIND SCC.


1 3

Online LibraryB. D LubachevskyVerification of several parallel coordination programs based on descriptions of their reachability sets → online text (page 1 of 3)