Peng-analysis Of Comm

Analysis of Communicating Processes for Non-progress Wuxu Peng and S. Purushothaman Department of Computer Science The Pennsylvania State University University Park, PA 16802

Abstract Let P and Q be two processes (specified as finite state machines) communicating asynchronously with each other using send and receive commands over a set of message types E. We consider the problem of testing P and Q for two forms of non-progress: deadlock and unspecified reception. Since the nonprogress problem is undecidable, we use a dataflow approach to obtain sufficientconditions under which the two processes are free of deadlock and unspecified reception. Our approximation analysis is based on weakening the receive operation, and we present polynomial time algorithms to perform the analysis. This problem arises in the context of dataflow

of messages.

Let P and Q be two processes specified as finite state machines (possibly nondeterministic), which send and receive messages asynchronously over unbounded buffers. The events of the two machines are send and receive commands specifying a particular message type g E E. A send event s(g) in P, appends a message of type g to the end of Q’s buffer. A receive event r ( g ) in P succeeds if there is a message of type g at the front of P ’ s buffer; it causes the front of P’s buffer to be deleted. We assume interleaving execution of the two processes. A pair of processes P and Q reach deadlock provided both can only attempt to receive and both of the buffers are empty. A process P reaches an unspecified reception state provided it reaches a state where it can only receive messages of particular types, and the message at the front of the queue is not one of acceptable types. Both deadlock and unspecified reception contribute towards non-progress of the processes and hence should be avoided. The problem of checking two processes for absence of deadlock and unspecified reception is undecidable [3]. In this paper we will take a dataflow approach to these problems. We will weaken the model by using receive commands that do not depend on the type of the message received. Under these assumptions we will present polynomial space and time algorithms to check statically whether two processes P and Q are free of deadlock and unspecified receptions. We develop the algorithms is such a fashion that the proof of “semantic soundness” theorems falls through easily. Our algorithm for checking two processes for absence of deadlocks solves the problem left open by Gouda and Yu in (111. On the other hand, the problem of checking for unspecified receptions has not been considered in the literature before. Our analysis for unspecified reception is set up in such a fashion that it is applicable when there are more than two participating processes.

analysis of processes that communicate by message passing and in the context of showing correctness of protocol specifications.

1

Introduction: Problem statement and background

One of the important characteristics of parallel programs is indeterminacy. Two different runs of a program with the same initial input might produce different traces. Thus it becomes difficult to debug them. Consequently, the burden of showing/proving that a parallel program is free of runtime errors such as deadlock rests with the programmer. We believe that in order for parallel programming languages to be widely accepted, their compilers should help users in detecting and exposing errors like deadlock. Our motivation is similar in spirit to type checking that is traditionally performed in the semantic analysis phase of a compiler for languages such as PASCAL. In fact, our approach is similar to polymorphic type-checking [2] of programs. In this paper we consider the problem of statically analyzing communicating processes for deadlock and unspecified reception

280

CH2706-0/89/0000/02&?0$01.00 0 1989 IEEE

Our motivation for considering finite state machines as representations of processes is two fold. First, in order to perform dataflow analysis of communicating processes we will have to forget the results of tests and assignment statements, which would lead us to communicating finite state machines [9]. Our specific model of asynchronous communication with blocking receives and non-blocking sends arise in programming the Intel hypercube and the systolic Warp machine [6].Our second motivation is the use of such machines in the literature for specifying and validating network protocols [I]. Moreover, a calculus for communicating processes [i’] widely used for giving semantics to parallel constructs is based on the notion of finite state machines as processes.

context of synchronous communication. They consider the non-progress problem when the interconnection among the processes is restricted to a tree and when restricted to acyclic processes in the general interconnections case. The work of Taylor [IO] discusses the importance of performing static analysis and presents a simulator for checking deadlocks whose termination is not guaranteed. The work of Holzman [4] discusses an algebra for expressing protocols and presents a simulator to detect deadlock. As in the work of Taylor, the simulator is not guarenteed to terminate.

3

In Section 2 we report on previous work, in Section 3 we provide necessary definitions, in Section 4 we show how deadlock analysis can be done, in Section 5 we consider the unspecified reception problem and we conclude in section 6.

2

Communicating finite state machines

A communicating finite state machine (CFSM) is a labeled directed graph with a distinguished initial state, and wherein each edge is labeled by an event. The events of a CFSM are send and receive commands over a set of message types E. The communication between CFSMs is assumed to be asynchronous (i.e., non-blocking sends and blocking receives). Consequently, we assume the availability of an infinite buffer for each process. Furthermore, interleaving semantics is assumed.

Previous work

Formally, let C be a set of message types, then a CFSM

P can be specified as a four-tuple (S,A,T,po), where

Previous work on this problem appear by Reif [9],by Gouda et al [11,3],and by Kanelakkis [5]. Reif considers the problem of reachability in a set of processes with multiple ports and a single message type. With static communication which corresponds to our assumptions here, he shows that reachability requires at least exponential space, infinitely often. On the other hand, his approximate algorithm for reachability analysis is more tractable. Unfortunately, his work does not handle loops well. Furthermore, the emphasis in the approximate analysis is on checking for the presence of deadlocks rather than on absence of deadlocks.

(1) S is the set of local states, ( 2 ) A = { r ( g ) , s ( g ) 1 g E C} is the set of events, s ( g ) denotes sending a message of type g and T(g) denotes receiving a message of type g, (3) T is a partial mapping, T : S x A 4 2’. T(p1,a) is the set of new states that the machine can possibly enter after performing event a in state p l , (4) po is the initial state.

Let N = ( P , Q ) be a network of two communicating finite state machines (NCFSM), where both P and Q are CFSMs. We will assume from now on that P and Q communicate over the same set C of message types. When N starts execution, the message buffers for both P and Q are assumed to be empty. A global state of N can be denoted by a 4-tuple [p, q, z, y], where process P is in state p , process Q is in state q , z is the string of messages in P’s buffer and y is the string Q’s. The initial state of the network is [Po, 40, E , E ] , where po is the initial state of P and qo is the initial state of Q.

The work of Gouda is more directly related to our work in that our models are the same. They provide an O(m3n3) algorithm that checks for freedom from deadlock when the two machines do not have any mixed nodes - that is there are no vertices whose outgoing arcs include both sending and receiving events. We present an O(m4n4) algorithm that works even in the presence of mixed nodes, where m and n are the number of states in the two processes. They did not consider the problem of checking for unspecified reception.

A node p in either P or Q is said to be a sending (or receiving) node iff all of its outgoing edges are sending (re-

Kanelakkis and Smolka considered the problem in the

28 1

spective buffers are empty. Since we are assuming that the receive commands do not depend on the type of messages, the type of messages being is not significant. Consequently, we will consider two machines P and Q that communicate by sending and receiving messages of a single type. Let m (or n) be the number of nodes in machine P(or Q). We will refer to the event of sending a message by 1 and the event of receiving a message by T. Since the type of the messages is not significant, the global state of the two machines can be captured by the 4-tuple [p, q, z, y ] , where p is a state in P , q is a state in Q, z and y denote the number of pending messages in the buffers of P and Q respectively.

ceiving) edges. A node p in P or Q is said to be a mixed node iff it has outgoing sending and receiving edges. These definitions have obvious generalizations to global states. Let e be an outgoing edge of node p (in P ) or q (in Q), and let label(e) = a. Let juxtaposition of two strings denote concatenation. A global state [p’, q‘, z’, y’] is onestep-reachable from [p, q, I,y ] , denoted M [p, q, I , y ] % [p’,q’, I‘, y’], if (1) e is a sending edge labeled by s ( g ) from p to p‘ in P , q‘ = q, z’ = z and y.g = y’, or (2) e is a sending edge labeled by s ( g ) from q to q’ in Q,p’ = p , 5.9 = z’ and y’ = y , or (3) e is a receiving edge labeled by r ( g ) from p to p’ in P , q = q’, g.z‘ = z and y‘ = y, or (4) e is a receiving edge labeled by ‘ ( 9 ) from q to q’ in Q,p = p’, I = 2‘ and g.y‘ = y . Define reachability as the reflexive and transitive closure of one-step-reachability. Define reachability set to be the set of states reachable from the initial state [Po, 90,E , E ] . We use the notation [p, q , I , y ) A [ p ’ ,q’, z‘, y’] if [p’,q‘, z‘, y‘] is reachable from [p,q,z,y]. Of course, [ ~ O , Q ~ , E , E ] -L [p, q , z, y ] denotes that [p, q , I, y ] is a reachable global state. A reachable state [p, q , I, y ] is a deadlock state iff I =

A reachable global state [p, q , 2,y ] is fair if z is equal to y . That is, the number of messages in the buffers for both P and Q are the same at all times. More formally, we define the fair reachable graph (FRG) for a pair of machines P and Q exchanging messages of a single type as follows, which captures the set of all fair states of the network ( P ,Q). Definition 4.1 Let N = ( P , Q ) be an NCFSM which ezchanges messages of a single type. The FRG[P,Q]= (V,E ) is a directed labelled graph defined as ( 1 ) bo,qo] E V , where po (qo) is the dart state for P ( Q ) .

Let [p,q] E V . -

( 2 ) I f p-&’

y = E and both p and q are receiving nodes.

E.

A reachable state [p, q , z, y ] is an unspecified reception state iff

E

( 9 ) I f p L p ’ E P , and q A q ’ E Q, then [p, q ] Z [ p ’ , q’] E

( 4 ) Ifp-%’

E P , and q L q ‘ E Q , then [p, q ] i [ p ’ ,q‘] E

(5) I f p A p ‘

E P , and &q‘

E.

2. q is a receiving node and none of the outgoing edges of q is labeled by the message at the front of y .

E.

When the type of the messages is not important, we will notate all receive commands (irrespective of the message type expected) by i. The Dyck set over the left brackets a l , a z , . . . ,a, and corresponding right brackets bl, b,.. . ,b, will be notated as DYCK(al,az,...,a,; b l , b , . . . , b , ) and the set of all prefixes over a Dyck set will be notated as PDYCK(a1, a2,. .. ,a,; b l , &, . . . , b,). Note that both of these are context-free languages. For example the grammar S ::= S(S)S I E specifies the dyck set over ”(” and

E

Q, then [p, q ] A [ p ’ , q‘] E

0

Intuitively, the edge label 1 denotes an increase in the number of messages, i denotes a decrease in the number of messages, and 0 denotes that no change has taken place in the number of messages in both the buffers.

A path r in FRG[P,Q] is legal iff any prefix of r has at least as many 1-labeled edges as T-labeled edges. The length of a path r (notated as Zen(r)) in FRG[P,Q]is the number of 1-labeled edges minus the number of 7-labeled edges in r.

1’’.

4

Q , then [ p , q ] A [ p ’ , q’]

E.

1. p is a receiving node and none of the outgoing edges of p is labeled by the message at the front of z, or

”

E P , and q L q ‘ E

The fair reachable graphs are important in that they capture only a subset of the entire reachable set of states. We state below that all fair reachable states are captured in the fair reachable graph. Our proof is based on a corresponding theorem appearing in [Ill, and is given in the Appendix A. Formally, we have

Deadlock Analysis

In this section we will discuss the problem of checking for freedom from deadlock. Note that processes P and Q reach deadlock iff they are both in receiving states and their re-

282

Lemma 4.1 Assume that we are given a n N C F S M N = ( P , Q ) and that its fair reachable graph is F R G [ P , Q ] = (V,E). [p,q, k , k ] is a reachable state in N iff there ezists at least a legal path r from node [po,qo] to node [p,q] in F R G [ P ,Q ] such that Zen(r) = k . I n particular, [p, q, O,O] is a reachable deadlock state in N iff there ezists at least a legal path r of length zero from node [Po, qo] to node [p, q] in FRG[P,Q].

Theorem 4.2 Let N be an N C F S M over multiple message types. Consider N’ obtained from N by identifying all message types to be a single message type. If N’ is free of deadlocks then N is also free of deadlocks. 0

Given a fair reachable graph, we have to search for receiving nodes such that the buffers can be empty when execution reaches them. We do so by capturing the set of execution sequences as context free language over the alphabet C1 = { l , i } .

5

Proof: Since N‘ has all the execution sequences of N (and of course some extra ones), if N’ is free of deadlocks then N is free of deadlocks too. 0

Analysis of unspecified reception

To recapitulate, a state p(or q ) in process P ( o r in Q) is an unspecified reception state if and only if [p, q, I, y ] is a reachable state, p(or q ) is a receiving node and none of the outgoing edges of p(or q ) is labeled by message type at the front of z(or y ) . As the existence of unspecified reception states in P solely depends on how messages are added to and deleted from P’s buffer, we wish to consider only the actions on P’s buffer (independent of Q s buffer) when analyzing P. This would form a modular approach allowing us to concentrate on one process at a time. Moreover, such an approach would allow us to generalize the technique for two machines to multiple machines. But, the messages that are added to P‘s buffer are the effect of send events in Q and vice versa. Consequently, we will first construct the set of all interleavings of the two processes and then project out the actions pertaining to P’s or Q’s buffer. The set of all interleavings can be obtained by a shuffle-product of the two machines. To maintain the indentity of events we will use a tuple (a,E ) to denote event a of process P and ( E , p) to denote event ,B of process Q .

Definition 4.2 Let F R G [ P ,Q]= (V,E ) be the fair reachable graph f O T a n NCFSM N = ( P , Q ) . The fair reachable automaton ( F R A ) corresponding to F R G [ P ,Q ] is a finite state machine M = (V,C,, 6, F , s), where (1) If v L w E E, then VLW E 6.

-

(2) If v L w E E, then V ~ E 6. W (3) If v L w E E, then v&w E 6. ( 4 ) The starting state s of M is the node [po,q~]in V . ( 5 ) F is the set of all receiving nodes in V . D In order to check for absence of deadlocks, we merely need to check that the language accepted by M (i.e., L ( M ) ) does not intersect the Dyck language over C1. More formally, we have the following: Theorem 4.1 Let N = ( P , Q ) an N C F S M over a single message type. Let M be the fair reachable automaton of N . N is free of deadlocks iff L ( M ) n D Y C K ( l ; i ) = 0. 0

Definition 5.1 Let an F S A (S,,,A,T,,po) be the specification of process P and a n F S A (Sq,A, Tp,qo) be the spec$cation of process Q. The shufle-product P @ Q is specified

Proof: Based on lemma 4.1 and the fact that a word w e D Y C K ( 1 ; T ) has equal number of 1s and 1 s and that any prefix of w has at least as many I s as is. 0 The entire process of checking for deadlock can be performed in O(m4n4) time, where m and n are the number of states in the two machines. The intersection of an FRA M(which has at most mn states) and a PDA for D Y C K ( 1 ; T ) (with a single state and two stack symbols) yields agrammar with at most m4n4productions, which has to be tested for emptiness. Since emptiness of a contextfree grammar can be carried out in time proportional to the number of productions in it, the entire process of checking for deadlock takes O(m4n4)time. The following semantic soundness theorem ( [ I l l ) helps us relate deadlock in a communicating machines with multiple types of messages to those that communicate using a single message type.

by the F S A (S,A’,T‘,s), where (1) s = [po,qol E s. (2) If [p,q] E S and p%p’

[p, q

E P , then the transition

[p’,q] E A‘. (3) If [p,q] E S and q L q ‘ E Q , then the transition [p, q]%[p, q f ] E T and the state [p, q‘] E A’. 0 ] ~ [ p ’q ], E T and the state

The global state of the composed process P @ Q can be depicted as a 2-tuple [[p, q], (2, y ) ] where [p, q] is a state of the composed process and (I, y ) is the tuple of message buffers. The state [[p, q ] , (I, y ) ] corresponds directly to the global state [p, q, I, y ] of the NCFSM N = ( P , Q ) . Consequently, the definition of reachability carries over with some minor changes.

283

Given a shuffle-product the relative ordering of the operations that affect P’s buffer can be obtained by ignoring the operations that affect Q‘s buffer. We will refer to this operation as projection and denote the projection of machine P (or Q) over the shuffle-product P @ Q by ( P @ Q ) Ip (or ( P@ Q) Formally we have

state [[p, q ] ,z ] in ( P @ Q )( p is an unspecified reception state if none of the outgoing receiving edges of [p, q] is labeled by the message type in front of the queue z. Let e be the edge from state [p1,q1] to state [p2,q2]. We say that e is the cause of an unspecified reception at state [p, q ] if there is an execution path in which a message of type g sent as a result of executing edge e results in g being in front of queue at [p, q ] , and g is not acceptable at state [p, q]. As the receive commands do not respect the type of a message, e can be the cause of an unspecified reception if there are k messages in the buffer when execution reaches state [PI,q1) and there are k receive commands in a path from [p1,q2] to the state b,q]. To formalize this intuition, we need the following definitions in the context of projection ( P @ Q )Ip.

IQ).

Definition 5.2 Let P @ Q = (S,A’,T,s) be the shufleproduct of N = ( P ,Q ) . T h e projection of P @ Q over P is a ( P 8 Q ) IP= (sp, Ap,Tp,sP) defined as: ( 1 ) sp= s. (2) sp = s. (3) T h e alphabet Ap contains all the send event3 of Q and a special letter T which denotes the receiving action of

P , viz., Ap = { g I ( E , s ( s ) )E A} U {T}. ( 4 ) The transition function Tp is a (sort of) restriction of the transition function of the composition P @ Q to the events in Ap. Corresponding t o transitions in A’ that affect Q’s buffer we use .z transitions in ( P 8 Q ) Ip, and corresponding to every transition that affects P’s buffer we will use a transition labeled by a n appropriate event f r o m Ap. Formally, Tp i s defineed as: I f [p, q ] ( E ’ S ( d ) h q ’ l E T , then ( p , q ] ~ [ p , q ’E ] Tp.

-

If [p,qfr*)[p’,q]

Definition 5.3 T h e spectra of a state [p,q] (notated as spectra([p,q ] ) ) is the set of all natural numbers k, such that [[p, q ] , z ] is a reachable state and length of z is k. T h e chops of two states [p, q] and [p’,q’] (notated chops( [p, q ] , [p’, q’])) is the set of all natural numbers k such that there are k receive commands o n some path f r o m [p, q] to [p’,q’]. 0 We are now in a position to state formally the condition under which a node, and consequently a shuffle-product is free of unspecified receptions. T h e o r e m 5.1 Let P‘ be the projection ( P @ Q )Ip. Let p be a receiving node in P . Let C be the set of all message types sent in P’ and C, be the set of all message types labelling all outgoing edges of p . Let e be a sending edge f r o m [PI, q1] t o [pz,qz] labeled by g E E.

E T , then [ p , q ] L [ p ’ , q ]E Tp.

The projection over P is a single finite state machine, and thus we can define the notion of reachability with the aid of a single queue. Note that the transitions are labeled by either E which has no effect on the queue, send events ( 9 E E) which cause a message of type g to be appended at which remove the end of the queue and receive events (i) messages from the front of the queue.

( 1 ) A state [p, q] E P’ is free of unspecified reception due to e i f f 9 E E-% is empty. . _

* spectra([p~,qll)n c h o ~ s ( [ p z , q ~ l , [ p , q l )

( 2 ) A state [p, q] E P‘ is free of unspecified reception due to a message type g i f it is free of unspecified reception due to e f o r every edge e labeled by E pt.

In the construction given above, the second process and its queue is being completely ignored. This should lead to some approximation, but an approximation on the safe side. Consequently, we have

(3) A state [p,q] E P‘ is free of unspecified reception if it is free of unspecified reception due to every message type g in the set C of P’. ( 4 ) The state p E P i3 free of unspecified receptions in the interaction between processes P and Q, if every state of

IQ

Lemma 5.1 Let ( P 8 Q ) Ip and (P@ Q ) be projections of P @ Q over P and Q respectively. I f [ [ p , q ] , ( z , y ) ]is a reachable state in the shufle-product, then [[p,q],z]is a reachable state in ( P 8 Q ) ( p and ((p,q],y]is a reachable state in ( P @ Q ) ( 8 . 0

the f o r m

b,q ] E P‘

is free of unspecified reception.

( 5 ) If every receive state in P and Q is free of unspecified

reception, then the N C F S M N = ( P , Q ) is free of unspecified reception. 0

A receiving node p in P is distributed in ( P @ Q ) Ip as a number of states of the form [p, q ] . Consequently, we can say that p is free of unspecified receptions if all states [p, q] in ( P Q ) Ip are free of unspecified receptions. A reachable

Proof: Follows directly from the definition of the relations spectra and chops. 0

284

Consider two edges, one is labeled by 1 and the other labeled by T in 91(R')2 lying on a path p as follows:

The use of projections in the above development allows us to easily extend this technique to certifying freedom from unspecified reception in the case of more than two processes; we merely need to compute the shuffle-product of all the machines and then consider the projection on each of the machines. Now we are left with tasks of computing the spectra of a node, computing the chops of two nodes and finding the intersection between them.

p : 5'

- L S 2 L S 3

1 .

'

L s n - li s ,

Let k be the number of messages in the queue when execution reaches the node s]. If this path is taken, then the number of messages in the queue when execution reaches the node s, will be IC and for nodes s2, ..., sn-l will be IC 1. Consequently, by adding an €-labeled edge from si to s, we will not be changing the spectra of any node. Assume that we have added an E-edge from SI to s, for all paths p as described above. Note that there can be at most O(m2n2) such additions. Since the addition of each of such E edge does not change the spectra of any node, we can drop all the receiving edges without changing the spectra relation! We will refer to this new machine as the normalized machine. The construction of the normalized machine R from a machine R' can be carried out in time O(m6n5)when R' has O(mn)states. The algorithm to perform this transformation is given in the Appendix B3. The correctness of this algorithm can be established by induction on the number of edges of paths in the graph. Now, we have the following

+

Let P' denote the projection (PBQ)( p = (Sp,AprTp,sp). Let s l , s2 and sg be states in P' for which we wish to test if spectra(sl)~chop~(s2,s3) is empty. Define R' to be a FSA with s1 as the final state, i.e., R' = (S,Ap,TP,sp, {SI}). Define R" as the FSA P' with s2 as the start state and s3 as the final state, i.e. R" = (S,ApTp,s2, ( ~ 3 ) ) . Now L(R') is a language characterizing all the paths in P' from the start state sp to sl, and L(R") is the set of paths in P' from state s2 to state s3 in P'. Note that every legal execution sequence from sp to SI has the property that any prefix of it has at least as many sends as receives. Consequently, the set of all legal execution sequences can be obtained by intersecting L(R') with PDYCK(gl,...,gn;1,...,i), where C = {gl,...,gn}. As we are interested in the number of messages in the buffer at state sl, i.e., the excess number of sends over receives in any legal execution sequence

spectra(sl)nchops(sz,s3) is empty iff L ( R )n L(iP2(R"))is

empty.

from start state sp to state sl, define L = G1(L(R'))n P D Y C K ( 1; 7)where 91 is a homomorphism specified by 91(g E E) = 1. Let be a Parikh's mapping [8]'. Thus,

Since each of the steps involved in computing the intersection can be performed in polynomial space and time, the test for unspecified reception can be carried out in polynomial space and time.

spectra(s1) = { z 1 = #I - #i, , where [#I, #i] E " ( L ) } . Similarly chops(s2,s3) = { z 1 z E 9(92(L(R"))},where G2 is specified as 92(g E E) = E and 02(i)= 1. Instead of computing the Parikh's mapping for the two sets and then intersecting them, we will use a more direct approach. The direct approach that we will look at in the following is possible due to a special property of CFLs (Parikh's theorem), which states that every CFL is letter-equivalent to a regular language. More formally, if C is a CFL then there exists a regular language R, such that *(C)= * ( R ) . Consequently, in the following instead of explicitly constructing the spectra we will compute the regular language over the single letter 1 which has the Parikh's mapping that we are interested in.

6

Discussion

We have shown how two communicating finite state processes can be tested for freedom from deadlock and unspecified reception in polynomial time. Our analysis for deadlock settles the problem left open in [ll].On the other hand, our analysis for unspecified reception is novel and has not been considered in the literature before. Moreover, our solution to the unspecified reception problem is scalable to networks of more than two processes. In figures 1 and 2 we show some networks that can be certified to be free of unspecified receptions using our algorithms. The problem of testing for deadlock in more than two processes still remains open.

'Parikh's mapping may be defined as follows. Let C = {al, ...,a,,} be the alphabet of a language C . Let #a(w) be number of times a E C appears in the word w E C . Now, U(C) = {n I D = [#,,,(w), ...,#..(tu)] and w E C }

*It can be obtained by replacing every event in g by 1. The language L(CP,(R'))is the same as CPI(L(R')). 3This algorithm does not depend on the final state of R'. Thus it computes the spectra of every node in a projection at the same time

285

Acknowledgements: We would like to thank Piotr Berman for his suggestions and encouragement. Initial node I

References

Initial node l

Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines. JACM, 30(2):323-342,1983. Luca Cardelli and Peter Wegner. Data types and Data abstraction ACM Computing Surveys, 1985. M. Gouda, E. Manning, and Y. T. Yu. On the progress of communication between two finite state machines. Information and Control, 63(3):308-320, 1984.

s (b)

r (a)

(a) Machine

G. J. Holzman. A theory of protocol validation. IEEE Transactions on Computers, C-31(8),1982.

Paris Kanelakkis and Scott Smolka. On the analysis of

(b) Machine Ql

Figure 1. An NCFSM N1

=

(Pl, Q1)

cooperation and antangonism in networks of communicating processes. In IV ACM Symposium on Principles of Distributed Computing, 1985. Initial

Monica Lam. Compiler Optimizations for Asynchronous Systolic Array Programs. In X V ACM

Symposium on Principles of Programming Languages, 1988. Robin Milner. Calculus for communcating systems. LNCS, Springer-Verlag, 1979. (a) Machine P2

Rohit Parikh. On Context-Free Languages. JACM, 570-581, 1966. Initial

John Reif. Dataflow analysis of communicating processes. In VI ACM Symposium on Principles of PTOgramming Languages, 1979. R. Taylor. A general-purpose algorithm for analyzing concurrent systems. Communications of A CM, 26(5):362-376, 1983. Y. T . Yu and M. G. Gouda. Deadlock detection for a class of communicating finite state machines. IEEE Transaction on Communications, 32514-2519. Dec 1982.

(b) Machine Q2 Figure 2. An NCFSM N2

286

r (a)

=

(P2, Q2)

Appendix A

Note that ECL and IECL can be computed in time O(m3n3). Now we are ready for the algorithm.

Proof of lemma 4.1

Algorithm Remove Purpose: Eliminate all T labelled edges from a projection graph a1(P‘)to obtain a normalized graph G.

If part: By the construction of the fair reachable graph, given a legal path r : [PO,q o ] L [ P , q] in FRG[P,Q ] , where

Input: A projection graph Ql(P’),whose node set is V and edge set is E.

l e n ( r ) = k, it is easy to recover the corresponding communication path in N leading to [P, q, k, IC]. Only if part: Let r : e l , e z , ...ek be a path in the network N leading from [Po,qo] to a fair state [ P , q , k , k ] . Among these k edges, let #s(P) be the number of sending edges of P, #s(Q) be the number of sending edges of Q, #r(P) be the number of sending edges of P, and #r(Q) be the number of sending edges of Q. As #s(P) = #r(Q)+k and #s(Q) = #r(P)+k, the path e l , ez, ...ek has the same number of edges from P and Q. Let a l , az, ...ai be the edges of P appearing in e l , ez, ...ek, and let b l , bz, ...bl be the edges of Q appearing in the same order as in e l , e z , ...ek. Now a path can be constructed in the FRG[P, Q], by considering the edges a, and bi in pairs. By induction on k, it can be easily shown that l e n ( r ) = k. 0

B

U,

(* Q is a queue which holds edges that have to be tested *) 0. Q := 4;

Q := Q U { v ~ w } ; 2. while Q # 4 do begin -

and there is

E

path from

U

Select any edge v-!+w in Q;

Q := Q - { v ~ w } ; for each node U on ISEL(V) do if (w $ ECL(u)) then begin Add U ~ to W E; for each node U‘ in IECL(u) do

6. 7. 8.

-

ECL(v‘) := ECL(v’) U ECL(w); for each node w‘ in ECL(w) do IECL(w’) := IECL(w’) U IECL(u); for each node U’ in ECL(w) do ff ISEL(u) - ISEL(v’) # then begin

9. 10.

11.

Definition B.l For each node v E ( P C 3 Q ) Ip ( 0 7 in (PC3 Q ) IQ) define the inverse sending edge list (ISEL) for v as follows: U,

3. 4.

5.

For an effecient computation of the normalized machine we have to maintain relations ISEL, ECL and IECL which are defined as follows:

--t

-

1. for each edge v A w E V do

An algorithm to compute spectra of all nodes in a projection

ISEL(v)= {w 1 w - 1

Output: A normalized graph G, such that for any node spectra(v) in @l(P’)= spectra(v) in G.

-

12.

for each edge v ’ L w ’ do if

13.

to

15.

VI.

end

The ISEL for each node in a projection can be computed in time O ( m z n z ) .

end

Definition B.2 For each node U , the E closure list (ECL) is set of nodes for which there is an €-path from U , i.e., ECL(v)={w I there ezists a path labelled by E from v t o w}. Definition B.3 For each node v, the inverse (IECL) can be defined as

E

closure list

IECL(v) = { w 1 there exists an E-path from w to v}.

287

v‘Lw‘ $ Q then -

Q := Q U { v’Aw’}; ISEL(v’) := ISEL(v‘) U ISEL(u). end

14.