Constraint-based structuring of network protocols.
The complexity of designing protocols has led to compositional techniques for designing and verifying protocols. We propose a technique based on the notion of parallel composition of protocols. We view a composite protocol as an interleaved execution of the component protocols subject to a set of constraints. Using the constraints as building blocks, we define several constraint-based structures with each structure combining the properties of the component protocols in a different way. For instance, the component protocols of a multifunction protocol can be structured so that the composite protocol performs all the individual functions concurrently or performs only one of them depending on the order of initiation of the component protocols. We provide inference rules to infer safety and liveness properties of the composite protocol. Some properties are derived from those of the component protocols while others are derived from the structuring mechanism (the set of constraints) used to combine the component protocols.
Introduction
Distributed protocols are typically complex and perform several functions. The modules
performing the various functions may interact with one another in a complex
manner which makes the design and verification of protocols a difficult task. Several
formalisms for specifying protocols have been proposed [9, 2, 14] which provide basic
operators for process synchronization. For modular design of protocols, several
structuring techniques for protocols specified in these formalisms have been pro-
posed. These structuring techniques follow the "separation of concerns" paradigm
in which the functionality of a protocol is first decomposed into subfunctions, protocols
for the various subfunctions are designed separately, and then combined using
a fixed set of rules to obtain a protocol for the entire problem. An advantage of
such a technique is that it allows the designer to focus on one aspect (subfunction)
at a time. In addition, in certain cases, properties of the composite protocol can be
inferred from those of the component protocols.
Sequential composition is one such structuring technique which allows design of
protocols performing multiple functions in sequence [8, 7, 6, 16, 13, 15]. Let
be two protocols. If P performs the first subtask
and Q performs the second subtask then the sequential composition of P and Q
requires P i to execute before Q i at each site i. For example, if P performs connection
establishment and Q is a data transfer protocol then P ; Q denotes the protocol which
first establishes a connection and then transfers the data. Sufficient conditions can
be derived to infer properties of the combined protocol. For example, showed
that if the component protocols are deadlock free and properly terminating then the
composite protocol is also deadlock-free and properly terminating.
In many multifunction protocols, several activities may have to be performed
concurrently. In such cases, we have to combine the component protocols so that
they can execute in an interleaved manner and interact with one another. We refer
to this as parallel composition of protocols wherein the component protocols can
execute concurrently. Several formalisms based on parallel composition have been
proposed. [3] proposed a notion of superimposition which is a parallel composition of
a basic computation, P , with some control protocol Q. In this case, Q i observes the
events of P i and constrains its execution. For example, a deadlock avoidance protocol
can be superimposed on a basic computation (which controls the basic computation
to prevent deadlocks). In the methodology proposed in [12], operational constraints
(which are in the form of propositions) are added to guards of the send statements
of P i and Q i to constrain their execution (constraints of P i may include variables
of Q i ). The union construct proposed in [5] also allows an interleaved execution of
the component protocols without any constraints.
We propose a technique for parallel composition of protocols. We model the
parallel composition as an interleaved execution of the component protocols P and
Q subject to a set of constraints. The constraints are local in nature and describe
the interactions between P i and Q i for each i. In this paper, we study two types
of constraints, synchronizing and inhibiting, to describe the interactions. Using
these constraints as building blocks, we define several constraint-based structures to
combine a set of component protocols with each structure combining the properties
of the component protocols in a different way. Using these structures, we show that
several existing protocols can be redesigned in a modular fashion.
The synchronizing constraint requires certain actions of P i and Q i to be synchro-
nized. This constraint can be used to combine P and Q to produce a multifunction
protocol which performs the functions of P and Q concurrently. For example, the
problem of N-process mutual exclusion can be decomposed into the subproblems of
enforcing mutual exclusion between each pair of processes. Using the synchronizing
constraint, we combine the two-process mutual exclusion protocols, one for each pair
of processes, to obtain the N-process protocol. By combining a protocol for data
transfer and a protocol for flow control, we also design a protocol to transfer data
with flow control.
The inhibiting constraint is specified between processes and may require that Q i
be inhibited on the initiation of P i (Q i ). This constraint can be used to inhibit
the execution of one protocol (which may already be executing) on the initiation
of another protocol. The inhibiting constraint is useful, for example, to design
multifunction protocols which can potentially perform the functions specified by
any of the component protocols but must perform only one of them. For example,
we design a leader election protocol which can elect any site as the leader but must
elect only one of them.
We give a set of rules to infer safety and liveness properties of the composite
protocol. Some safety and liveness properties of the composite protocol are inferred
from those of the component protocols whereas some are inferred from the structure
imposed by the constraints. The proof system is closely related to the one in [10],
where a projection method to verify a protocol was proposed. In the projection
technique, an already designed protocol is decomposed for the purpose of analysis.
Our technique can be viewed as an inverse of the projection method. For example,
if P and Q are composed to obtain R, then projection of R on to variables and
messages of P gives a protocol that is identical to P except that some guards may
have additional boolean conjuncts.
We show that different protocols can be obtained by imposing different constraints
on the same set of component protocols. As mentioned above, sequential
composition allows construction of multifunction protocols which perform the functions
in sequence. In [15], we modeled sequential composition using ordering constraints
between P i and Q i for each i. The technique proposed in this paper also
views the composition in terms of a set of constraints, and allows construction of
multifunction protocols which either perform all the component functions concurrently
or performs only one of them. Together with the ordering constraint, the
proposed technique can be used to design complex protocols. We also advocate the
use of our technique in conjunction with the step-wise refinement techniques [11, 17].
First, a simple protocol (maybe an inefficient one, but correct) can be derived using
our technique, which can then be refined in a step-manner to optimize it.
This paper is organized as follows. In the next section, we present a formalism
to specify protocols and Section 3 discusses some examples. In Section 4, we present
our composition principle and Section 5 describes the properties of the composite
protocols. Finally, we conclude in Section 6.
Model
A protocol, P , is a set of processes We model the communication
channel from P i to P j as a sequence ch i;j of messages. A message is of the
form M(para list), where M is the type of the message and para list is a list of
parameters. The statement 'j ! M(arg list)' executed by P i causes M(arg list) to
be appended to the end of ch i;j . The statement 'i ? M(para list)' executed by P j
removes the message at the head of ch i;j (if there exists a message of type M at
the head of the channel) and stores the contents of the message in para list. The
execution of 'i ? M(para list)' is blocked until there exists a message of type M at
the head of the channel. Each P i is in the following normal form [1]:
s init
l=1 a l :: en(a l
s init is the initialization action used to specify initial values of the variables
and therefore, we assume that it can only contain local computation. "a l ::
guarded action in which a l is the label, en(a l ) is the
guard and s l is the computation associated with the action. The guard, en(a l ),
is of the form bool l ; Rec l , where bool l is a boolean expression and Rec l is a
receive statement (both parts are optional). bool l ; Rec l evaluates to true if
bool l is true and the message indicated in Rec l can be received (that is, it
is at the head of the channel). The computation s l may contain send statements
and some local computation. The execution of the alternative statement
l=1 a l :: en(a l ) \Gamma! s l ] involves evaluating the guards of each action and executing
s action a x with en(a x ) as true. The statement  [S ] involves a
repetitive execution of statement S.

Figure

1 gives a two-process mutual exclusion protocol, MUT (i; j), for processes
i and j. In this protocol, a single token in circulated between the processes and the
process holding the token can enter the critical section. The variable hold i;j is true
if i holds the token. The variable ext i is set to true if i wants to enter the critical
section. If i holds the token, it checks whether there is a pending request. If one
exists, then i enters the critical section (by setting in i to true). After this check has
been made, check i;j is set to true. On exiting the critical section, it sets in i to false.
If check i;j is true, i holds the token and i is not in the critical section, then i sends
the token to j. The protocol at site j is similar (except that in the initialization
section, hold i is set to false).
denote the set of variables which appear in P i and var(P
denote the set of messages sent or received
by P i and mess(P ). The state of P i is defined by
the values of variables in var(P i ). We will use predicate init(P i ) to characterize
the initial state of P i (this predicate reflects the assignments made in s init ). The
state of a channel from P i to P j is the value of ch i;j . The state of the system is
a tuple (s states of the processes and
represent the states of the channels. The initial state of the system is a state
in which all channels are empty and init(P 1 Each event
is associated with an action and an event occurs when the computation associated
with its action is executed. We use a i to denote the event which corresponds to the
in i
true
*[ Rtoken i;j
:: j? token \Gamma! hold i;j
trueEnter i;j :: :check i;j
hold i;j
\Gamma! check i;j := true;
if ext i
then in i
:: in i
\Gamma! in i
check i;j
\Gamma! j! token; check i;j
hold i;j
falseRequest i;j
\Gamma! ext i
true

Figure

1: Protocol MUT (i; j) at site i
th execution of action a. We assume that the execution of each event is atomic with
respect to other events.
An execution of a protocol is a maximal sequence,
0 is the initial state, and for all l, event e l is enabled in state g l and the execution
of the computation associated with e l transforms state g l to g l+1 . We say that
is reachable from g 0 if there exists a sequence
em
that e l transforms the state g l to g l+1 , 1 - l - m.
We define the proposition initiate(P i ) as follows: initiate(P i ) is initially false.
It becomes true when any action from the loop statement of P i has been executed.
Informally, whether P at site i has been initiated (since init
is used to specify initial values only, P i is not considered initiated until it executes
an action from its loop statement). We also define initiate
initiate Pn and active P
initiate Pn . We say that P i is an initiator
of P if there exists an execution of P in which P i sends a message before receiving
a message. Informally, an initiator of a protocol is a process which can start the
protocol by sending messages to other processes without first receiving a message.
A protocol can have more than one initiator.
An assertion I is an invariant of P if I is true in the initial state of P and in all
states reachable from the initial state. We define the relation ; as follows: ff ; fi
in an execution
of P iff the following holds: For all x, if ff is
true in g x , then there exists a state g y , y - x, such that fi holds in g y . ff ; fi in
all executions of P . Informally, ff ; fi implies that if ff becomes
true then fi will become true in the future. For example, ext i ; in i in MUT (i;
implies if i wants to enter the critical section, it will eventually do so. To prove
the ; properties, we assume the following strong fairness condition: If an action is
enabled infinitely often then its execution cannot be delayed indefinitely.
3 A Compositional Approach
Let P and Q be two component protocols. A composite protocol R in our framework
is structured as a set of interacting component protocols. The interactions between
the protocols are specified by a set of constraints. The constraints are local in nature
i:e:; they are specified between processes at the same site and therefore, R i derived
only from processes at site i (with P and Q as component protocols, R
constraints). We will introduce the constraints using examples.
3.1 Synchronizing Constraint
A synchronizing constraint between actions a p and a q requires that their execution
be synchronized i:e:; the system treats a p and a q as a single action which is enabled
when both en(a p ) and en(a q ) are true. The synchronizing constraint is useful
in designing protocols performing multiple functions concurrently. Each function
may impose different restrictions on the common actions and the synchronizing
constraints can ensure that restrictions of all the component protocols are satisfied.
Our first set of example protocols which use synchronizing constraints involves
problems which can be decomposed into subproblems, where each subproblem is
the same as the original problem but of a smaller size. For example, a mutual
exclusion problem between three sites 1, 2 and 3 can be decomposed into three
subproblems, each involving mutual exclusion between a pair of sites. Figure 1 shows
a two-process mutual exclusion protocol M(i; j) for a pair (i; j) of sites. The three-process
protocol, MUT(1; 2; 3), can be obtained by combining M(1; 2), M(1;
M(2; as follows: In MUT(1; 2; 3), we want to ensure (in 1
Protocol M(1; 2) maintains in 1 ) :in 2 by requiring that Enter 1;2 (which sets in 1 to
true) be executed on receiving permission from 2 (in the form of a token). MUT(1;
ensures in 1 ) :in 3 in a similar way. By imposing a synchronizing constraint
on Enter 1;2 and Enter 1;3 , we ensure that in MUT(1; 2; 3), both en(Enter 1;2 ) and
en(Enter 1;3 ) are true before in 1 is assigned the value true (which maintains both
invariants). Similar constraints need to be enforced at other sites. This protocol
can be extended to an N-process mutual exclusion protocol.
As another example, consider a protocol in which a sender sends the same set
of data items to a number of receivers in a synchronized manner (sender sends a
data item to all receivers, receives acknowledgements from all receivers and then
sends the next data item). Consider the corresponding protocol Data(s; ri) with
sender s and a single receiver ri. This is an iterative protocol where in each
iteration, the sender sends the next data item, waits for an acknowledgement
and then increments next. The original protocol can be obtained by combining
by synchronizing the action of incrementing
next (which is a shared variable). This ensures that the next data item is sent
after acknowledgements have been received from all receivers.
Another class of multifunction protocols that can be designed using synchronizing
constraints consists of protocols that involve distinct types of subproblems.
Consider the protocols Data and F low shown in Figure 2. Protocol Data performs
the function of sending a sequence of data items in the array Sdata[1::1]
from a sender s to receiver r which stores them in Rdata[1::1]. In Data s , a data
item can be sent and variable used incremented (action Send) only after the data
item is ready for transmission (we assume that a higher layer protocol is producing
these data items and sets ready[x] to true after it has placed the data item x in
Sdata[x]). Protocol F low performs the function of flow control. In this protocol,
s sends a REQ message to r for some credit (whenever it has no more credit left).
On receiving the REQ message, r sends some credit. s can spend by incrementing
used (action Spend) whenever credit is available. A protocol, Data&F low, which
performs data transfer with flow control can be obtained by executing Data and
F low in an interleaved manner with a synchronizing constraint on actions Spend
and Send (each action imposes a different constraint on when the variable used can
be incremented; as discussed later, used is incremented only once when both Spend
and Send are executed). As a result, a data item is sent only after it is ready for
transmission and when credit is available.
We can further add properties to Data&F low in a incremental fashion. For
F low s ::
avail := 0; used := 0
used ! avail \Gamma!
used := used
Data s
used := 0;
ready[used
used used
low r ::
grant := 0;
Grant:: s?REQ(x) \Gamma!
grant
Data r
next := 0;
Recr:: s?data(y) \Gamma!
next

Figure

2: Data and Flow control Protocols
instance, if the channels may reorder messages, then Data&F low does not guarantee
Sdata[i]). We can guarantee ordered delivery by composing
low with a protocol, Seq, which ensures ordered delivery of messages by
imposing restrictions on when the array Rdata can be updated at the receiver site.
The notion of superimposition [3] is a composition mechanism which can be
modeled using the synchronizing constraint. Superimposition requires that if P is
superimposed on Q then for each message of type M of Q, the action of send-
ing(receiving) M in Q must be synchronized with the action of sending(receiving)
in P . Since the superimposition framework was designed to reason about control
protocols, synchronization is allowed on sending/receiving actions only.
3.2 Inhibiting constraint
An inhibiting constraint is specified as a pair (P indicates that on the
initiation of P i , the execution of Q i must be inhibited. We use this constraint to
describe an interaction wherein one protocol may have to inhibit the execution of
another protocol. This constraint is useful in deriving several types of multifunction
protocols as shown in the following examples.
In certain multifunction protocols, we may require one component protocol to
explicitly terminate another component protocol. For example, a connection management
protocol typically performs the following two functions: connection establishment
and disconnection. The disconnection protocol can be initiated at any
time, and on the initiation of this protocol, the execution of the data transfer phase
is inhibited. In this case, at each site (both the sender and the receiver), initiation
of the process belonging to the disconnection protocol terminates the process
belonging to the connection protocol. We specify this interaction as the disconnection
protocol terminating the connection establishment protocol. We implement P
terminates Q by specifying that P i inhibits Q
The terminates relation is an asymmetric one. In general, we may allow both P
and Q to inhibit one another. This relationship is useful in designing a multifunction
protocol which perform only one of its possible multiple functions at a time.
Consider the case in which each component protocol has a single initiator. If P and
Q have the same initiator site i, then we define a conf lict relation between them by
specifying that both P i and Q i inhibit each other. In this case, the initiation of one
of them will inhibit the initiation of the other. If P and Q have initiators at different
sites then both can be initiated concurrently. In this case, we have to specify a
priority relationship. We say that P has priority over Q if Q is inhibited when both
are initiated concurrently. We implement this by specifying that P i inhibits Q i for
each i and if P j is the initiator of P then Q inhibits P j . Thus, only if Q is initiated
first and it leads to initiation of Q be selected for execution.

Figure

3 gives a three-process traversal protocol, Traverse(1), with 1 as the initiator
for a network of three sites with identities 1, 2 and 3. In this protocol, node
1 sends a message containing its identity to 2 and 3, then sets leader 1 to true after
receiving an ack message from both 2 and 3. This protocol performs the function
of electing 1 as the leader. We can obtain a leader-election protocol by combining
Traverse(1), Traverse(2) and Traverse(3) and specifying the constraint that
Traverse(i) has priority over Traverse(j), where i ? j. This constraint implements
the rule that if when a traversal initiated by a node with a larger identity encounters
a traversal with a smaller identity, the traversal with a smaller identity is inhibited.
As another example, consider a simple connection establishment protocol
sent 1
\Gamma! 2! capture(id 1
sent 1
trueElect 1
::win 1;2
\Gamma! leader 1
true
recd 2;1
recd 3;1

Figure

3: A 3-process traversal algorithm
in which the initiator site i establishes a connection from i to j. Consider
the composition of Connect(1; 2) and Connect(2; 1). A full-duplex protocol in
which connections are allowed in both directions concurrently can be designed by
combining Connect(1; 2) and Connect(2; 1) with no constraints. However, if connection
in only one direction is allowed then we can specify that Connect(1; 2) has
priority over Connect(2; 1) (or vice-versa) as both have initiators at different sites.
In this case, if both initiate connection establishment at the same time, then the
connection from 1 to 2 is established 1 . Now consider the protocols Connect(1; 2)
and Connect(1; 3). If 1 is allowed to establish connection with only one site at a
time (for instance, if 1 is the server, 2 and 3 are clients then the server may be
allowed to connect to one client at a time) then we can achieve this by specifying
Using sequential composition, we can combine the resulting protocol with itself to get an
iterative protocol in which after the connection is established and then disconnected, the protocol
returns to the initial state in which a choice again is available to establish a connection in either
direction.
that Connect(1; 2) and Connect(1; are conflicting protocols (as initiators are at
the same site). Using a combination of these constraints, many complex protocols
can be designed.
As illustrated in this section, a set of component protocols can be structured in
different ways using different set of constraints. Although the protocols discussed
above have been designed before, the use of our technique makes the design modular
(and helps in understanding the overall structure of the protocol). Our aim is
to make a disciplined use of the constraints to combine protocols in well-defined
structures (discussed above) in order to ensure that their properties can be combined
using some inference rules. In the next section, we develop a framework which
formalizes the restrictions on the constraints.
4 The Composition Principle
In this section, we give a formal definition of our composition technique and discuss
an algorithm for obtaining a composite protocol. We will consider composition of
two component protocols only. Let be the
two component protocols. We assume that P and Q do not share messages (but P i
and Q i may share variables). A composite protocol, R, is obtained from P and Q
by specifying at most one type of constraints: synchronizing constraints, inhibiting
constraints or no constraints. Given P , Q, and the constraints, the composite protocol
involves an interleaved execution of P and Q subject to the specified constraints.
In the following section, we discuss composition using synchronzing constraints and
inhibiting constraints.
4.1 Composition using synchronizing constraint
The synchronizing constraints are specified using a set synch(P; Q). A pair (a; b)
belonging to synch(P; Q) specifies that actions a and b are subject to the synchronizing
constraint, where a and b are actions belonging to P i and Q i respectively,
for some i. In this section, we give first give an algorithm to obtain the composite
protocol, R, from P , Q and the constraints, and then discuss some rules to infer
of R from those of P and Q. Before presenting this algorithm, we will define certain
restrictions on the constraints which ensure that properties of the component
protocols can be combined using well-defined rules. We first define the notion of
matching actions. Actions ap and aq of P i and Q i respectively are matching actions
do not update any variable in
actions Enter 1;2 and Enter 1;3 with computations:
check 1;2 := true; if ext 1 then in 1 := true; ext 1 := false
check 1;3 := true; if ext 1 then in 1 := true; ext 1 := false
are matching, where
denote the set of actions in P and Q that update a variable in
example,
fEnter Request 1;2 ; Request 1;3 g.
We say that P and Q are matching protocols if for each action a in shared(P; Q)
which belongs to P (Q), there exists a distinct matching action in Q (P )
(the matching function is one-to-one). For example, protocols MUT(1; 2)
and MUT(1; are matching since fEnter 1;2 ; Enter 1;3 g, fExit 1;2 ; Exit 1;3 g and
fRequest Request 1;3 g are matching pairs of actions. We say that action a of
P belongs to synch(P; Q) if (a; b) 2 synch(P; Q) for some action b of Q. We require
the following restriction:
must be matching and every matching pair of actions must belong
to synch(P; Q).
If a belongs to synch(P; Q) then en(a) does not involve receiving a message 2 .
Note that in addition to the actions required to be present by restriction S1,
additional pairs of actions also. The restrictions given
above have been defined to match the inference rules given in the folowing. It is
possible to define other ways of using the constraints with associated inference rules.
Less restrictions will, in general, imply more complex inference rules. In the extreme
case, we can allow arbitrary constraints to be specified and provide no inference rules
(this would require analysis of the composite protocol directly).
2 Since the channels are shared, this restriction is required to ensure deadlock freedom. In our
framework. we assume that P and Q do not share messages. We can extend our framework to
allow message sharing and relax S3 to allow action a to receive a shared message (in this case, the
matching action b will also involve receiving the same shared message).
4.1.1 An algorithm for generating composite protocols
This section discusses an algorithm to obtain the composite protocol R from P , Q
and synch(P; Q). The constraints can be implemented in several ways. For instance,
we can create a control process at each node i which is superimposed on both P i
and Q i to enforce the constraints. In the following, we give an implementation of
the constraints which creates a single process R i from P i , Q i and the constraints:
A1. If the initialization action of P i and Q
respectively then the initialization action of R i is
A2. The actions in the loop statement of R i are obtained as follows: For each action
a of P i or Q i ,
ffl If a 62 synch(P; Q) then a:: en(a) \Gamma! s a is in R i .
ffl Let a :: en(a) \Gamma! c 1 ; c; c 2 be an action in shared(P; Q) and b :: en(b) \Gamma!
4 be the matching action. Then ab
in R i , where ab is a new label. In this case, we say that action ab is obtained
by fusing actions a and b.
We will now derive the three process mutual exclusion protocol using the protocol
of

Figure

1. As discussed before, MUT(1; 2) and MUT(1; are matching. Hence,
we can first obtain M 0 by combining MUT(1; 2) and MUT(1; 3) with synch set as:
Protocol M 0 has three processes where M 0
1 is obtained by combining MUT(1;
and MUT(1;
. For protocols M 0 and
MUT(2; 3), we have the following pairs of matching actions:
(Enter
(Req
all of which belong to shared(M are also
matching. We combine these protocols to obtain MUT(1; 2; 3), which is shown in

Figure

4.
4.1.2 Properties of the composite protocol
We now present rules which enable us to infer properties of the composite protocol
from those of the component protocols. Let F (P ) be a set of formulas which only
hold 1;2
:= true; hold 1;3
Rtoken 1;2 :: 2? token \Gamma! hold 1;2 := trueRtoken 1;3
:: 3? token \Gamma! hold 1;3
- :check 1;3
hold 1;2
hold 1;3
\Gamma!
check 1;2
:= true; check 1;3
then in 1
\Gamma! in i
hold 1;2
check 1;2
\Gamma! 2! token; check 1;2
hold 1;2
:= falseStoken 1;3 :: hold 1;3 - check 1;3 - :in 1 \Gamma! 3! token; check 1;3 := false; hold 1;3 := falseRequest 1
\Gamma! ext i
true

Figure

4: Three Process Mutual Exclusion Protocol
refer to variables in var(P ). Let EF (P ) be a set of formulas which only refer to
variables in var(P ) and to propositions of the form m 2 ch i;j , where m is a message.
Set EF (P ) does not allow reference to the number of messages in the channel or
the position of a message in the channel.
Let R be a protocol obtained by combining P , Q and synch(P; Q). The following
lemma allows us to infer invariants of R from those of P and Q. From condition S1,
an update to a shared variable by Q (P ) is made only when P (Q) is ready to make
the same update. Hence, all updates to shared variables are made in a consistent
manner.
Lemma 4.1 If I 2 EF (P ) is an invariant of P then I is an invariant of R.
We know that (in i is an invariant of MUT (i; j). Then,
from the corresponding invariants of MUT(1; 2), MUT(2; using
Lemma 4.1, we can infer that 8i;
is an invariant of MUT(1; 2; 3). Through the use of shared variables, invariants
relating variables in P and Q can also be inferred. For example, for the protocol
low, grant - next (which implies that the receiver never receives a data
item for which it has not granted permission) can be inferred as an invariant from
grant - used (an invariant of F low) and used - next (an invariant of Data).
Some invariants can be inferred from the constraints imposed. Lemma 4.2 reflects
the nature of the structure imposed by the synchronizing constraint. Let occur(e)
be a proposition that is true if event e has occurred. As defined earlier, a i refers to
the i th execution of action a.
Lemma 4.2 If (a; b) 2 synch(P; Q), ff ) occur(a i ) is an invariant of P and
is an invariant of Q then ff ) fi is an invariant of R.
For example, in MUT(1; 2; 3), let recd(1; 2) and sent(1; 3) be auxiliary variables
indicating the number of times 1 has received token from 2 and the number of times
1 has sent a token to 3. Then, recd(1;
1;2 ) is an invariant
of MUT(1; 2) (since 1 has the token initially) and occur(Enter x
is an invariant of MUT(1; 3). Hence, (recd(1;
an invariant of MUT(1; 2; 3) (which can be used to show that in MUT(1; 2; 3), each
process i sends both tokens before it is ready to send any one of them again). In
addition to invariants, we can design proof rules for more general safety properties.
For example, P satisfies ff unless fi if in each execution
any i, if ff is true in g i , then either ff remains true in all subsequent states or there
exists such that ff is true in g k , is true in g j . If ff unless fi in
P and ff; fi 2 EF (P ) then ff unless fi in R. Informally, this follows from the fact
that in any state g k , belongs to Q then it cannot invalidate ff (if
cannot refer to variables in ff; if (a; e k
then since a does not invalidate ff, e k cannot invalidate ff).
We now discuss liveness properties. We first give a set of proof rules to infer
liveness properties in a protocol. In the following, let fffg a ffig mean that if ff is
true before the execution of a then fi is true after the execution of a. ff ; fi via a
in P if the following holds:
is an invariant of P
(2) fffg a ffig, and
(3) for all actions b, fff - en(b)g b fff - fig.
Further, ff ; fi in P if one of the following is true:
is an invariant
where a is an action in P
S is a set of formulas, 8b 2 is the disjunction
of all formulas in S.
Let first(ch i;j ) denote the message at the head of channel ch i;j . Protocol P is
free from unspecified receptions if there does not exist a reachable state g such that
in state g, for some i and j, first(ch i;j no action in P j which receives
m is enabled in g. If P is free from unspecified receptions then for any message m,
ch i;j communication channels,
we need to ensure that R is free from unspecified receptions. Because of restriction
S3, we have the following lemma:
Lemma 4.3 If P and Q are free from unspecified receptions then R is free from
unspecified receptions.
In the following, we will assume that R is free from unspecified receptions. We will
now give inference rules to derive liveness properties of R.
Lemma 4.4 If ff ; fi via a in P , where ff; fi 2 EF (P ) and a is not in synch(P; Q)
then ff ; fi in R.
We say that is local to P if its derivation does not involve any application
of rule L1 with an action in synch(P; Q). As a corollary to Lemma 4.4, we have:
Corollary 4.1 If ff ; fi is local to P then ff ; fi in R.
In combining MUT(1; 2) and MUT(1; 3), for example, hold 2;1 - check 2;1 - :in
hold 1;2 is local to MUT(1; 2) and therefore, it holds in the composite protocol M 0 .
We now consider the case in which (a; b) belongs to synch(P; Q) and ff ; fi via a in
c be action obtained by fusing a and b. Assume that ff
holds in R in state g. Then, en(a) holds in g. We have to show that c is eventually
executed. For this, en(b) must become true (since Thus, we
have the following lemma:
Lemma 4.5 If (a; b) 2 synch(P; Q), ff ; fi via a in P , and I - en(a) - ff ; en(b)
in R, where I is an invariant of R, then ff ; fi in R.
Consider the flow control protocol shown in Figure 2. We know that (ready[y
in Data. We can infer this property for
low as follows: We can infer that (used is an invariant
from Lemma 4.2 and the following invariants:
(invaraint of F low)
Then, using rule L1, we have (used
(avail ? used) is local to F low, we have used) in the
composite protocol. Then, from rule L4, we have (used
used), from Lemma 4.5, (ready[y
holds in the composite protocol.
Special cases can be identified for checking when c can always be executed (irre-
spective of ff and I). For example, if we can show that for each (a; b) 2 synch(P; Q),
in P implies ff ; fi in R. This, for
instance, can be shown for the following class of compositions: Let
iterative protocols with P 1 executing actions a executing
actions in each iteration (P 2 and Q 2 are similar) and synch(P;
such that for all
example, would satisfy the given restrictions
(the synchronizing constraints must respect the cyclic order). Such a condition
can be generalized for iterative protocols with more than two processes.
4.2 Composition using inhibiting constraint
We now discuss composition using inhibiting constraint. We require The inhibiting
constraints are specified using a set inhibit(P; Q) that consists of pairs
processes. If (P belongs to inhibit(P; Q) then the initiation of P i
inhibits (that is, after initiate(P i ) becomes true, no action of Q i can execute).
We require that inhibit(P; Q) satisfy the following restrictions:
We only use the inhibition constraint to specify the terminate, priority and
conflict relations. We define a relation dominates as follows: (P; Q) belongs
to dominates if P terminates Q or P has priority over Q. We require that the
dominates relation be acyclic.
4.2.1 An algorithm for generating composite protocols
We use the following rules to derive the composite process R i from P i and Q i .
(B1) Let the initialization actions of P i and Q i be s p and s q respectively. We
introduce two new variables enable P i and enable Q i . Then, the initialization
action of R i is s
(B2) The actions in the loop statement of R i are obtained as follows: Let a be an
action of P i . We first apply rule (a) to modify action a, then apply (b) to
further modify it (the same rules are applied to modify the actions of Q
(a) If (P then a is modified to a:: en(a) \Gamma! s
:= false. Else, it is not modified.
(b) If (Q then a is further modified by adding enable P i
as a conjunct to the guard of a. In addition, if a involves the command
then a new action new:: :enable P i
introduced
in R i , where new is a new label.
As an optimization in rule B2, if the first action in the loop statement to be executed
in P i is known, then we need to add enable Q i := false only to this action. In
Section 3, we discussed the derivation of the three-process leader election protocol
by combining the traversal protocols. The protocol constructed by our algorithm
using the constraint discussed in the Section 3.2 is shown in Figure 5.
4.2.2 Properties of the composite protocol
If inhibit(P; Q) is non-empty then no shared variables are allowed. However, in
case a protocol is inhibited, additional actions are added which can modify the
channel contentsm and therefore, invariants referring to channel contents may not
be preserved. Hence, we have the following lemma.
Lemma 4.6 If inhibit(P; Q) is non-empty and I 2 F (P ) is an invariant of P then
I is an invariant of R.
Using Lemma 4.6, we can infer that leader i ) (recd 2;1 - recd 3;1 ) is an invariant of
leader election protocol from the fact that it is an invariant of Traverse 1 . Lemma 4.6
can be refined for special cases. For example, if I 2 EF (P ) is an invariant of P and
terminates Q or P has priority over Q or P and Q conflict then initiate P ) I is
an invariant of R (intuitively, initiate P implies that P will inhibit Q and therefore,
the execution of P will not be impacted by that of Q; hence, its invariants referring
to the channel contents will be preserved).
in 1
\Gamma! sent 1;2
-:sent 1;2
\Gamma! 2! capture(id 1
sent 1;2
-:sent 1;3
\Gamma! 3! capture(id 1
sent 1;3
::win 1;2
\Gamma! leader 1

Figure

5: A three process election algorithm
Recall that initiate P is true when the execution of P is initiated by any of
its initiators and active P is true when all processes of P have been initiated. Let
enable
enable Pn . From the definitions, initiate P and active P
are false in the intial state but are stable predicates (once they become true, they
remain true). On the other hand, enable P is true in the initial state but is not stable
enable P i can be assigned false if (Q
Lemma 4.7
(a) If P terminates Q then initiate P is an invariant of R.
(b) If P has priority over Q then initiate P is an invariant
of R.
(c) If P and Q conflict then initiate P is an invariant of
R.
Corollary 4.2 If ff ) initiate P and fi ) active Q are invariants of P and Q
respectively, where ff 2 F (P ) and fi 2 F (Q), and P has priority over Q or P and
conflict then (ff is an invariant of R.
Consider the leader election protocol discussed earlier. We know that leader 1 )
active T raverse(1) and leader 2 ) initiate T raverse(2) are invariants of Traverse(1) and
Traverse(2) respectively. Since Traverse(2) has priority over Traverse(1), from
is an invariant of the
composite protocol. Similarly, using Corollary 4.2, we can show that in the protocol
obtained by combining Connect(1; 2) and Connect(2; 1), connection is established
in only one direction, and in the protocol obtained by combining Connect(1; 2) and
connection is established with either 2 or 3.
Since P and Q share communication channels, we need to ensure that R is free
from unspecified receptions. Because of the additional transitions added by rule
B2(b), we have the following lemma:
Lemma 4.8 If P and Q are free from unspecified receptions then R is free from
unspecified receptions.
Consider the case in which inhibit(P; Q) is non-empty. Initially, both protocols are
enabled. If there exists a pair (Q in P then it is
possible that after ff becomes true, P i is inhibited and fi never becomes true. There-
fore, in general, we can only state that if there exists a pair (Q
and ff ; fi in P then ff ; (:enable P - fi) in R. This, however, may not be sufficient
to infer interesting liveness properties of R. The following lemma exploits the
properties of the inhibition constraint to infer additional liveness properties.
Lemma 4.9 Let ff ; fi in P , where ff; fi 2 EF (P ). If P terminates Q or P has
priority over Q or P and Q conflict then ff - initiate P ; fi. If Q has priority over
active
Corollary 4.3 If true ; fi p in P , true ; fi q in Q and inhibit(P; Q) is not empty
then true
As an application of Corollary 4.3, consider the composition of Traverse(1) and
Traverse(2). Since true ; leader 2 in Traverse(2) and true ; leader 1 in
Traverse(1). From Corollary 4.3, we can infer true in the
composite protocol. Using Lemma 4.9, we can also show that if true active P
in P , true ; active Q in Q, and P has priority over Q or P and Q conflict then
true active P \Phi active Q in R (this reflects the nature of the composition which
dictates that only one of them becomes active).
5 Conclusion
We have presented a framework to compose protocols using synchronizing and inhibiting
constraints. The synchronizing constraints allow derivation of multifunction
protocols which perform all component functions concurrently. The inhibiting
constraint can be used to design multifunction protocols which perform one of the
component functions. We demonstrated the use of these constraints by designing
several protocols. We presented a set of rules to infer safety and liveness properties
of the composite protocol.
In [15], we modeled sequential composition as a set of protocols executing under
ordering constraints. The proposed formalism views a composite protocol as a concurrent
execution of component protocols subject to a set of constraints. Our future
work will involve development of a unified formalism which allows ordering, synchronizing
and inhibiting constraints. We find that many composite protocols require
a combination of such constraints (for instance, both ordering and synchronizing
constraints between the two protocols).
Several other types of control protocols can be structured using the inhibiting
constraint. For example, consider the snapshot protocol [4] for recording global
states, which is typically initiated whenever a "change" in the network state is
observed by any node. In a dynamic network, if the snapshot protocol is in progress
and a node detects a change again, it may reinitiate the protocol and all nodes
are required to participate in the new initiation. Each initiation of the protocol
can be considered as a new execution which inhibits the old execution. Modeling
this would require extension of the framework to allow message sharing between
protocols interacting using the inhibiting constraints and is part of future work.



--R

Two normal forms theorems for csp programs.
Finite state description of communication protocols.
A compositional approach to superimposition.
Distributed snapshots: Determining global states in distributed systems.
Parallel program design.
A decomposition method for the analysis and design of finite state protocols.
A discipline for constructing multi-phase communicating protocols
Decomposition of distributed programs into communication closed layers.
Communicating sequential processes.


A methodology for constructing communication protocols with multiple concurrent functions.
An improved method for constructing multiphase communications protocols.
Hierarchical correctness proofs of distributed algo- rithms
On the construction of multiphase protocols.
Designing distributed algorithms by means of formal sequentially phased reasoning.
A lattice-structured proof technique applied to a minimum spanning tree algorithm
--TR
Hierarchical correctness proofs for distributed algorithms
A compositional approach to superimposition
A Relational Notation for State Transition Systems
A discipline for constructing multiphase communication protocols
Distributed snapshots
Communicating sequential processes
An Improved Method for Constructing Multiphase Communications Protocols
Designing Distributed Algorithms by Means of Formal Sequentially Phased Reasoning (Extended Abstract)
A decomposition method for the analysis and design of finite state protocols
multifunction protocols;safety and liveness properties;protocol composition;distributed protocols