A Prover for Parallel Processes

1. INTRODUCTION

The need for proofs of properties of parallel program is very greater. A number of research results for parallel program have been given. [1],(2],[3],[4],[5],[8],[9],[10] In parallel processes, several processes which communicate each other run on several processors~ So para­ llel processes cause complicated states. How­ ever, as shown in [8], we can consider them the compositions of indivisible operations. So, by decomposition of parallel programs, we can analyze their movement s and effects on states. Syntactic analyses of this type are powerful for those of properties of parallel programs. Our prover processes these analyses.

Since the formal system given in [8] includes infinitely long expressions such as F* (the

abbreviation of F0VFlvF~ ... ), we mechanize its subsystem which contains decomposition of F* with respect to 'interruption (2.3.4)' but does not contain the rules of inference which decom-

pose G(F*) into G(F 0 ),G{F), ... ,G(Fn), .... (cf. [8] 3.1 {i) *-left and *-right) We implement it by the KLISP[6] system with about 12K free cells on PDPll/55 computer in a similar way to [7].

We roughly explain our basic idea in the simpl­ est cases . In our system, we introduce the operator F;G (G is executed after F), but we do not introduce the 'clock'. Let f, g and h be indivisible operations. f and g , sometimes, run in parallel on different processors (denoted by f//g), but f//g causes the same result as f;g or g;f (denoted by (f;g~(g;f)). For example, (f;g)//h or (f;g)*//h causes the same result as (h;f;g)\1( f;h;g)V{f;g;h) or ( f;g)*;h; ( f;g)*V

A Prover for Parallel Processes

Toshio Nishimura Department of Mathematics University of Tsukuba Sakura-mura Niihari-gun

Ibaraki-ken 300-31, JAPAN

for verifying logical properties of parallel processes. The prover system given in [8]. We mechanize it so that a proof-tree is The prover reduces a parallel program into possible serial ones by 'interruption' etc .. This paper includes some examples processed

(f;g)*;f;h;g;(f;g)*, respectively. The general form of a rule of inference will be given in 2.3.4 below. In such a way, we could reduce parallel processes into possible serial ones.

In our system, we prove the equivalence of para­ llel programs in the form of sequent. In order to show the equivalence between two programs F and G, our prover proves two sequents F~ and �~F. For example, let a process be able to enter the critical section C if it satisfies the condition Q. It can not enter C eternally , if it satisfies 'not Q' (denoted by~Q) eternally (denoted by (7Q)·). So, in order to show that a parallel program P is deadlock free, it is sufficient to show that P i s equivalent to a program E, where E does not contain infinite loop such as x·. And, a parallel pror,ram P which contains two critical sections CSl and CS2 are mutually exclusive, if P is equivalent Lo a program E, where E does not contain any parallel run of CSl and CS2 such as CS1//CS2 .

2. IMPLEMENTED FORMAL SYSTEM ---

2.1. An expression and an indivi sible expres ­ sion.

The symbols used in the propositional calculus have the usual meanings for lor,ical formulas (e.g. y, f\,-::J, :=- or 7 represent s 'or', 'and', 'implies', 'equivalent' or 'not' respectively). And we introduce symbols of expression-constants Especially, the expression-constant "I" plays the role of the identity function and means the truth value "true" for a formula. And ".1"" represent s "impossible", and the truth value "false" for a formula. A formula in the propo­ sitional calculus, extended by adding the clause

"if A and Bare formulas, so are A;B and A//B", is an expression. An expression-constant is an expression. A figure of the form x:=E is an express ion, called an assignment statement to x, where x is a variable and E is a term in the predicate calculus . IfF and G are expressions, so ar e F//G, FVb and F;G. IfF is an expres-

sion , so are ~, F.., and F*, where m is a vari­ able for integers. If F is an expression, then [F] is an indivisible expression. An indivisi­ ble expression is an expression. Only those obtained in the above are expressions.

We briefly explain the intuitive meaning of the above definition. An expression means an instruction, a decision, a series of them or a formula in the propositional calculus . And a decision is denoted by a formula. F;G means that G is executed after the execution of F. F//G represents that F and G are executed in parallel. IfF and G are formulas, F;G, F//G and FAG have the same meaning as "F and G" in the propositional calculus. An expression FVC represents that at least one of F or G is exe­ cuted . If F and G are formulas, FVG has the same meaning as "For G". An expres sion F* means that F will be executed n-times for an arbitrary n. F~ represents the infinite loop of F.

Generally , an expression F is of the form F 1 ;F 2 ; ... ;Fn' where every Fi is an indivisible express i on , an expression-constant or an expres­ sion of the form 7H, HVK, H//K, ~. H* or H .... Titis i s called the canonical form of F.

In the prover, F;G, F/\G,. FVG, F/ /G, F.JG, F:G,

~. Fn, F*, F" or [F] i s denoted by (CONC F G), (*AND F G), (*OR F G), (PAR F G), (*IMPLIES F G) , ( *EQUIV F G) , (*NOT F) , (LABEL F n) , ( * F) , (INF F) or (IND F), respectively.

2 . 2 ~ seguent, an axiom and !:!:_ proof

A fi gure of the form

form wh1eh satisfies the following conditions.

1. The uppermost sequent is an arbitrary sequent.
2. Every lowermost sequent is an axiom.
3. The upper sequent and the lower sequents are connected by a rule of inference given in the paragraph 2.3 below.

Let S be a sequent. Then a proof-tree, which has S as the uppermost sequent, is called the proof-tree to S. If we have a proof-tree to S, we say that S is provable.

(*ARROW (E) (E 1 En)).

2.3 Rules of Inference

Rules of inference of the subsystem are divided into the following parts.

2.3.1 Rules of inference for the propositional calculus.

We omit those here. (cf. [7])

2.3.2 Rules of inference with respect to \1

Let F(e) be an arbitrary expression which con­ tains the indicated expression-variable e in at most one place in F(e) except for the inside of any subexpression of the form K*, K" or7L. V-left Given a sequent F(EVC)~~. we can give two sequents F(B}-+lland F(C)~L). V-right Given a sequentr~~.F(BVC) , we can give the sequentr--t>.LI,F(B) ,F(C)

2.3.3 Replacement of expression

(i) Replacement by assumption

Let F(e) be an arbitrary expression. Here the indicated e may be contained in several parts of F(e). Let a sequent F(A)--+G(A), be given, where A is a formula. Then, according that the set of assumptions contains A or7A, we can give the sequent F(I)~�(I), or F(!)-+�(~), , respectively.

(ii) Inherent replacement

In our system, the followings are built in as schemes of assumptions.

G 0 =I,7i=I, :I*=I, I*=I, I//G=G, G//I=G, I;G=G, G;I=G,i:VG=G, �vi:=�,i 10 =~, J';G=!., ~//�=S, G//£=.i ,7I=:£'

if G does not contain an expression of the form

K·, G;£ =~,

K·;H=K , (K"'//G);H=K"'//G, (G//K 00 );H=G//Keo,

(G*)QI=(G*;I 00 )VG 10 and Gm;GrA=G 04 ·

Given a sequent, every figure of the same form as the left-hand side of '=' in the sequent is replaced by the right-hand side by matching.

We roughly explain the meanings of some of them. Let the following parallel program be given: perbegin Pl: begin Ll: if Q then goto Ll; S end; P2: begin G end

parend.

In Pl, one of the following (i) and (ii) occurs: (i) Q is satisfied finite times and after that "]Q is satisfied and then S is executed (denoted by Q*;7Q;S) and (ii) Q is satisfied eternally (denoted by QrA). So in Pl//P2, either (Q*;7Q;S) //G or Q~//� is executed. If (Q*;7Q;S)//G is

executed, Q is satisfied finite times (i.e.:! 0 or I*), the value of Q finally becomes 1: . So

the value of .! 0 or I* is I. And then the infi­ nite loop Q 111 (i.e. ¥) is impossible, i.e. the value of ~s :I. Since ( i) is executed, tht execution of Q 10 //G is impossible, i.e. the value of~ /G is!. If Q·/ /G is executed, then the value of 7Q is.! and the execution of Q* ;7Q;S is impossible, i.e. the value of I*;~;S (= ~;S) is i . Since K 00 is the infinite loop of K, every­ thing after K"' is unable to be executed. So the value of K-;H is K·. In K"'//G, G may eternally wait for the completion of K 10 after its com­ pletion. Then the value of (K"'//G);H is K"//G.

2.3.4 Interruption

In order to describe the rule of inference for interruption, we define two ordered sets comp(E) and lete(E) for an arbitrary expression E, which does not contain//, as follows. If F is an indivisible expression or an expres­

sion-constant, then

comp(F) = (I,F) and lete (F) = (F,I). Let F and G be arbitrary expressions, where comp(F)=(F 10 , ··. ,F 1 m)' lete(F)=(F 20 , ··· ,F2m)' comp(G)=(G 10 , ··· ,G 1 n) and lete(G)=(G 20 , ··· ,G 2 n).

'I'hen

Let F//G or G//F be a subexpression in a sequent, where G does not contain //. Let an expression F 1 ;F 2 ; ·.· ;Fm be the canonical form of F. Let Fi be the leftmost indivisible expres­ sion. Denoting F 1 ; ·.. ;F. 1 or F. 1 ; ... ;F by H 1 11+ m or H 2 respectively, F is of the form H 1 ;Fi;H 2 . When comp(G)=(G 10 , ·.. ,Glm) and lete(G)=(G 20 , .. , G2m), the indicated F//G is replaced by (Hl//Gl0);Fi;(H2//G20)V(Hl//Gl2);Fi;(H2/ /G22)\/ ... V(H 1 //Glm);Fi;(H 2 //G2m). The case of G//F is similar. In the actual programming, the sets comp(G) and lete(G) are not constructed, but it is processed in procedural way. (cf. 3.(6), (8))

2.3.5 Execution

(i) Execution of assignment statement

By G' we denote the result obtained by executine x:=E for G. Then G' is obtained as follows: Let G 1 ;G 2 ; ... ;Gm be the canonical form of an expression G, and Gj the leftmost expression which contains an assignment statement to x. Then G1,G2·····Gj_ 1 are the results obtained by replacing E for x in G 1 ,G 2 , ... ,Gj-l respectively If Gj is of the form x:=K, then Gj is x:=K', where K' is the result obtained by replacing E for x inK. If K does not contain x, then Gj' is Gj.

Let F be an arbitrary expression and F 1 ;F 2 ; ·.. ; F its canonical form. And let F. be the leftm 1 most assignment statement of the form x:=E where E does not contain x, and let Fj (i(j) be the next leftmost expression which contains an assignment statement to x. Then the result obtained by execution of Fi i s F 1 ; .·. ;Fi;Fi+l; ... ;FJ;Fj+l'"""'Fm.

(ii) Elimination of assignment statement

Let F and F 1 ;F 2 ; ... ;Fm be the same as the previous one. And let Fi be the leftmost assignment statement to x. If we have Fj such that Fj is an assignment statement to x and Fi+l; .·· ;Fj-l does not contain the variable x, then F is r eplaced by F 1 ; ... ;Fi_ 1 ;Fi+l; ·.. ;FJ; ... ;Fm.

3 . ALGORITHM

Given an arbi trary sequent E ~ E 1 , . . . , Em and a set of assumptions , the prover constructs the proof-tree to the sequent in the following order.

• (1 ) Whether the given sequent i s an axiom or not , is checked . If the lef t-hand s ide of the sequent is ~ , i t is an axiom. If an expression in the left- hand s ide occurs in the r i ght-hand side , it is al so an axi om. When we have no re­ maining sequent, the proof i s complet ed, and the obtained proof -tree is printed out. If we have a r emaining sequent, the prover has the last one of t hem as the given one, and goes to (1). If it is not an axiom, then the prover goes to (2).
• (2 ) The prover executes assignment statements contained in E, E 1 , ... ,Em' if any, from left to rlght and the control goes to (1). Otherwise 1t 1~oe s to (3) .
• If a r ule of inference 'inherent replace­ ment (2.3 . 3 ( i i) )' is applicable to t he given sequent , t hen t he prover executes i t , and the control goes to ( 1 ). Otherwi se , i t goes to ( 4).
• (I,) If a rule or infer ence 'replacement by assumption (2 . 3. 3 (i ) )' ·i s applicable to the r,ivcn sequent , t hen t he prover executes it, and the control 1~oes to ( 1). Ot herwise, it goes to (5) .
• ( 5) If a rule of inference ' V -left' i s appli­ cable to the given sequent, then t he prover exe­ cutes it . Let t he given one be F(BVC)~J1, where the i ndi cat ed FNC i s not in any inside of 7, * or..,. 'Then for the next st ep, F(B)----t.Liis the "lvcn nequent nnd F(C)~.LJ i:J the last rf'llllll.ll .l. llf' one. And the control v,oes to ( 1). Othcrwbc , lt goes to (6).
• (6 ) I f' a r ule of inference ' i nterr uption' is applicable to t he l eft-hand side of the given sequent , t hen t he prover executes i t. Let the given one be F(�//H)~, where t he i ndicated G/ / H is not i n any inside of7, *or~. And let the result be F(A 1 V ·.. VAn )---+.LJ. Then the

prover constructs t he following n sequents:

F(A 1 )~J1(the given sequent for the next step),

F(A 2 )~Ll(the last remaining sequent),

F(A 3 )~.LJ, ..· , F(An)~Lf,

and the control goes to (1). If an interrupt­ ion is not applicable to the left-hand side, then the control goes to (7).

• ( 7) If a rule of inference 'V -right' is appli­ cable to the sequent, then the prover executes it. And the control goes to (1). Otherwise goes to (8).
• If a rule of inference 'interruption' is applicable to the right-hand side of the given sequent, then prover executes it. Let the given
• one ber---+LJ 1 , F(G/ /H), ..1 2 , where the indicated G/ /H is not in any inside of 7, * or " . And let the result be ['~ 1 , F ( A 1 V .·· VAn) .t] 2 · Then the prover constructs the sequent

r~LJ 1 ,F(A 1 ), ... ,F(An),11 2 , and the control goes to (1). If an interruption is not applicable to the right-hand side, then it goes to (9).

• {9) We fail the proof. Then we can select one of the following two modes. One, we stop the prover and print out the proof-tree obtained so far. Two, we return the control to the last r emaining sequent, and continue to construct the proof -tree. If we have no remaining sequent, the proof-tree obtained so far is print out.

In our prover, we can change the order of (2), ·.· ,(8) by presenting the table of the order of execution in advance.

4. EXAMPLES

4.1 An example of mutually exclusive but deadlocked program

E.W.Dijkstra gave an example of a program which satisfies the mutual exclusion but causes the "deadlock"[l]. His program is the following: begin in~eger c 1 , c 2 ; c 1 :=1; c 2 :=1;

parbeg1n

process 1: begin A 1 : C 1 :=0;

L 1 : if c 2 =0 then goto 1 1 ; critical section 1; c 1 :=1; remainder of cycle 1; goto A 1

end; process 2: begin A 2 : c 2 :=0;

1 2 : if c 1 =o then goto 1 2 ; critical section 2; c 2 :=1;

remainder of cycle 2; goto A 2 end

I~t P 1 or P 2 be c 1 :=0;(C 2 #0V(C 2 =o)~);CS 1 ;c 1 :=1 or c 2 :=0;(cloV(c 1 =o) 00 );CS 2 ;c 2 :=1, respectively. Then the program except for the last "goto A 1 " or "goto A 2 " can be expressed by the following:

provided that the program does not halt. By ~ , we denote the following:

Then the sequent which we want to prove is c 1 :=l;C 2 :=l;(P 1 //P 2 J---tL1,

with assumptions 0=0, 1=1, 1#0, O#l. Because it is not an axiom and the replacement of assumptions can not be applied, the prover applies V-left, and we have

The prover applies interruption to the left-hand side of (3) for c 1 :=0, so we have

Applyinf, to (4) elimination of assignment(C 1 :=1) and replacement by assumption(G//I=G and G;I=G), we have

By the application of interruption to the left­ hand side of (5) for c 2 #o, we have

... '

Applying to (6) replacement by assumption(G//I=G and G;I=G), execution of assignment((C#O)=(l#O)) and replacement by assumptions((l#O)=I and G; I=G), we have

Applying interruption to the left-hand side of (7) for C :=1, we have

Applying execution and elimination of assign­ ment, replacement of assumption to (8), we have (10) cs 1 ;c 1 :=l;CS 2 ;c 2 :=1---+~.

This is an axiom. Then the prover stores the sequents (8) and (10) in the disk storage and returns to ( 9). Repeating these operations, at length, the control returns to the decomposition of the sequent (which is one of the result s of V-left to (2))

Applying replacement by assumptions(K~;H=K~)

(11) becomes

By interruption for c 1 :=0, we have

c 1 :=l;C 2 :=l;(I//I);C 1 :=0;

( (c 2 =0) 10 / /(C 2 :=0; (C 1 =or) )~~.

Applying execution and elimination of assign­ ment and replace by assumption, to (]3), we have (16) C2:=0;Cl :=0; (I 10 I I I 00 )--4Ll.

This is an axiom and represents the deadlock. From (14), we have the same sequent as (16). Applying execution of assignment to (15), we have

~replacement of assumptions, we have

which is an axiom.

In this problem, the number of leaves of the proof-tree is 38. And the time for proving is 112 seconds.

4.2 Dijkstra's solution for two processes

E.W.Dijkstra gave the famous solution [2) p.58. In order to prove the correctness of the solu­ tion, it is sufficient to show the following sequent in our system. In the following, h=l or h=2.

In this proof, the number of leaves was 690 and it took 3074 seconds long in which 2976 garbage collections were included.

5. CONCLUSION

Our prover is very useful for verifying logical properties such as the mutual exclusion or deadlock free problem. But at the present, this prover is basic and the construction of a proof­ tree is staightforward. So it has many branches and leaves. In the next step, we intend to supply it with the following facilities: (1) analyses of syntactic patterns, for example, application of rules of inference with attention to a fixed variable, (2) restricted mathematical induction (cf. [7]) for processing infinitely long expression F*, and (3) man-machine inter­ action.