B. D Lubachevsky. # Verification of several parallel coordination programs based on descriptions of their reachability sets online

. **(page 1 of 3)**

Online Library → B. D Lubachevsky → Verification of several parallel coordination programs based on descriptions of their reachability sets → online text (page 1 of 3)

Font size

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.

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.

Online Library → B. D Lubachevsky → Verification of several parallel coordination programs based on descriptions of their reachability sets → online text (page 1 of 3)