Detection of Weak Unstable Predicates in Distributed Programs.
This paper discusses detection of global predicates in a distributed program. Earlieralgorithms for detection of global predicates proposed by Chandy and Lamport (1985)work only for stable predicates. A predicate is stable if it does not turn false once itbecomes true. Our algorithms detect even unstable predicates, without excessiveoverhead. In the past, such predicates have been regarded as too difficult to detect.The predicates are specified by using a logic described formally in this paper. We discussdetection of weak conjunctive predicates that are formed by conjunction of predicateslocal to processes in the system. Our detection methods will detect whether such apredicate is true for any interleaving of events in the system, regardless of whether thepredicate is stable. Also, any predicate that can be reduced to a set of weak conjunctivepredicates is detectable. This class of predicates captures many global predicates thatare of interest to a programmer. The message complexity of our algorithm is bounded bythe number of messages used by the program. The main applications of our results are indebugging and testing of distributed programs. Our algorithms have been incorporated ina distributed debugger that runs on a network of Sun workstations in UNIX.
Introduction
A distributed program is one that runs on multiple processors
connected by a communication network. The state
of such a program is distributed across the network and
no process has access to the global state at any instant.
Detection of a global predicate, i.e. a condition that depends
on the state of multiple processes, is a fundamental
problem in distributed computing. This problem arises in
many contexts such as designing, testing and debugging of
distributed programs.
A global predicate may be either stable or unstable. A
stable predicate is one which never turns false once it becomes
true. Some examples of stable predicates are dead-lock
and termination. Once a system has terminated it
will stay terminated. An unstable predicate is one without
such a property. Its value may alternate between true
and false. Chandy and Lamport [3] have given an elegant
algorithm to detect stable predicates. Their algorithm is
based on taking a consistent global snapshot of the system
and checking if the snapshot satisfies the global predicate.
If the snapshot satisfies the stable predicate, then it can
be inferred that the stable predicate is true at the end of
This work was supported in part by the NSF Grant CCR 9110605, the
Navy Grant N00039-91-C-0082, a TRW faculty assistantship award, and
IBM Agreement 153.
V.K. Garg is with the Electrical and Computer Engineering
Dept, University of Texas at Austin, Austin,
jay@pine.ece.utexas.edu B. Waldecker is with Austin System Center of
Schlumberger Well Services, Austin,
the snapshot algorithm. Similarly, if the predicate is false
for the snapshot, then it was also false at the beginning of
the snapshot algorithm. By taking such snapshots periodically
a stable property can be detected. Bouge [2] , and
Spezialetti and Kearns [22] have extended this method for
repeated snapshots. This approach does not work for unstable
predicate which may be true only between two snap-shots
and not at the time when the snapshot is taken. An
entirely different approach is required for such predicates.
In this paper, we present an approach which detects a
large class of unstable predicates. We begin by defining
a logic that is used for specification of global predicates.
Formulas in this logic are interpreted over a single run of a
distributed program. A run of a distributed program generates
a partial order of events, and there are many total
orders consistent with this partial order. We call a formula
strong if it is true for all total orders, and weak if there exists
a total order for which it is true. We consider a special
class of predicates defined in this logic in which a global
state formula is either a disjunction, or a conjunction of local
predicates. Since disjunctive predicates can simply be
detected by incorporating a local predicate detection mechanism
at each process, we focus on conjunctive predicates.
In this paper, we describe algorithms for detection of weak
types of these predicates. Detection of strong predicates is
discussed in [10] .
Many of our detection algorithms use timestamp vectors
as proposed by Fidge [6] and Mattern [17]. Each process
detects its local predicate and records the timestamp associated
with the event. These timestamps are sent to
a checker process which uses these timestamps to decide
if the global predicate became true. We show that our
method uses the optimal number of comparisons by providing
an adversary argument. We also show that the checking
process can be decentralized, making our algorithms useful
even for large networks.
The algorithms presented in this paper have many appli-
cations. In debugging a distributed program, a programmer
may specify a breakpoint on a condition using our logic
and then detect if the condition became true. Our algorithms
can also be used for testing distributed programs.
Any condition that must be true in a valid run of a distributed
program may be specified and then its occurrence
can be verified. An important property of our algorithms
is that they detect even those errors which may not manifest
themselves in a particular execution, but may do so
with different processing speeds. As an example, consider
a distributed mutual exclusion algorithm. In some run, it
may be possible that two processes do not access critical
region even if they both had permission to enter the critical
region. Our algorithms will detect such a scenario under
certain conditions described in the paper.
Cooper and Marzullo [5], and Haban and Weigel [11] also
describe predicate detection, but they deal with general
predicates. Detection of such predicates is intractable since
it involves a combinatorial explosion of the state space. For
example, the algorithm proposed by Cooper and Marzullo
[5] has complexity O(k n ) where k is the maximum number
of events a monitored process has executed and n is the
number of processes. The fundamental difference between
our algorithm and their algorithm is that their algorithm
explicitly checks all possible global states, whereas our algorithm
does not. Miller and Choi [19] discuss mainly
linked predicates. They do not discuss detection of conjunctive
predicates (in our sense) which are most useful
in distributed programs. Moreover, they do not make distinction
between program messages and messages used by
the detection algorithm. As a result, the linked predicate
detected by Miller and Choi's algorithm may be true
when the debugger is present but may become false when
it is removed. Our algorithms avoid this problem. Hurfin,
Plouzeau and Raynal [12] also discuss methods for detecting
atomic sequences of predicates in distributed computa-
tions. Spezialetti and Kearns [23] discuss methods for recognizing
event occurrences without taking snapshots. How-
ever, their approach is suitable only for monotonic events
which are similar to stable properties. An overview of these
and some other approaches can be found in [20].
This paper is organized as follows: Section II presents
our logic for describing unstable predicates in a distributed
program. It describes the notion of a distributed run, a
global sequence and the logic for specification of global
predicates. Section III discusses a necessary and sufficient
condition for detection of weak conjunctive predicates. It
also shows that detection of weak conjunctive predicates
is sufficient to detect any global predicate on a finite state
program, or any global predicate that can be written as a
boolean expression of local conditions. Section IV presents
an algorithm for detection of a weak conjunctive predicate.
Section V describes a technique to decentralize our algo-
rithm. Section VI gives some details of an implementation
of our algorithms in a distributed debugger. Finally, section
VII gives conclusions of this paper.
II. Our Model
A. Distributed Run
We assume a loosely-coupled message-passing system without
any shared memory or a global clock. A distributed
program consists of a set of n processes denoted by
communicating solely via asynchronous mes-
sages. In this paper, we will be concerned with a single
run r of a distributed program. Each process P i in that
run generates a single execution trace r[i] which is a finite
sequence of states and actions which alternate beginning
with an initial state. The state of a process is defined
by the value of all its variables including its program
counter. For example, the process P i generates the trace
s i;0 a i;0 s i;1 a are the local states
and a i 's are the local actions in the process P i . There are
three kinds of actions - internal, send and receive. A send
action denoted by send(! means the sending of a
message OE from the process P i to the process P j . A receive
action denoted by receive(! means the receiving
of a message OE from the process P i by the process P j . We
assume in this paper that no messages are lost, altered or
spuriously introduced. We do not make any assumptions
about FIFO nature of the channels. A run r is a vector of
traces with r[i] as the trace of the process P i . From the
reliability of messages we obtain
receive(!
We also define a happened-before relation (denoted by !)
between states similar to that of Lamport's happened-before
relation between events .
1 The state s in the trace r[i] happened-before
(!) the state t in the trace r[j] if and only if one of the
following holds:
1. occurs before t in r[i].
2. The action following s is the send of a message and the
action before t is the reception of that message.
3. There exists a state u in one of the traces such that
t.
The relation ! is a partial order on the states of the processes
in the system. As a result of rules 2 and 3 in the
above definition, we say that there is a message path from
state s to state t if s ! t and they are in different processes.
A run can be visualized as a valid error-free process time
diagram [16].
Example 2 Consider the following distributed program:
Process
var x:integer initially 7; var y,z:integer initially (0,0);
begin begin
possible values of
program counters. A distributed run r is given by:
Another run r 0 can be constructed when two messages sent
by the process P 1 are received in the reverse order.
B. Global Sequence
A run defines a partial order (!) on the set of actions
and states. For simplicity, we ignore actions from a run
and focus just on states in traces. Thus, r[i] denotes the
sequence of states of P i . In general, there are many total
orders that are consistent with (or linearizations of) this
partial order. A global sequence corresponds to a view of
the run which could be obtained given the existence of a
global clock. Thus, a global sequence is a sequence of global
states where a global state is a vector of local states. This
definition of a global state is different from that of Chandy
and Lamport which includes states of the channels. In our
model, a channel is just a set of all those messages that
have been sent but not received yet. Since this set can be
deduced from all the local states, we do not require the
state of channels to be explicitly included in the global
state. We denote the set of global sequences consistent
with a run r as linear(r). A global sequence g is a finite
sequence of global states denoted as l , where
k is a global state for 0 - k - l. Its suffix starting with
l ) is denoted by g k . Clearly, if the
observer restricts his attention to a single process P i , then
he would observe r[i] or a stutter of r[i]. A stutter of r[i] is
a finite sequence where each state in r[i] may be repeated a
finite number of times. The stutter arises because we have
purposely avoided any reference to physical time. Let skt
mean that s 6! t - t 6! s. Then, a global sequence of a run
is defined as:
Definition 3 g is a global sequence of a run r (denoted by
only if the following constraints hold:
restricted to P (or a stutter of r[i])
[i] is the state of P i in the
global state g k
Example 4 Some global sequences consistent with the run
r in Example 2 are given below:
(l
(l
Our model of a distributed run and global sequences does
not assume that the system computation can always be
specified as some interleaving of local actions. The next
global state of a global sequence may result from multiple
independent local actions.
C. Logic Operators
There are three syntactic categories in our logic - bool,
lin and form. The syntax of our logic is as follows:
form ::= A: lin j E: lin
lin
lin - lin j :lin j bool
bool ::= a predicate over a global system state
A bool is a boolean expression defined on a single global
state of the system. Its value can be determined if the
global state is known. For example, if the global state has
then the bool (x - y) is true. Here x
and y could be variables in different processes. A lin is
a temporal formula defined over a global sequence. 3 lin
means that there exists a suffix of the global sequence such
that lin is true for the suffix [21]. We also use 2 as the dual
of 3. We have also introduced a binary operator (,!) to
capture sequencing directly. p ,! q means that there exists
suffixes g i and g j of the global sequence such that p is true
of the suffix g i , q is true of the suffix g j , and i ! j. A form
is defined over a set of global sequences and it is simply a
lin qualified with the universal (A:) or the existential (E:)
quantifier. Thus, the semantics of our logic is as follows:
lin
lin
A, and E quantify over the set of global sequences that
a distributed run may exhibit given the trace for each pro-
cess. A:p means that the predicate p holds for all global
sequences and E:p means that the predicate p holds for
some global sequence. We call formulas starting with A:
as strong formulas and formulas starting with E: as weak
formulas. The intuition behind the term strong is that a
strong formula is true no matter how fast or slow the individual
processes in the system execute. That is, it holds
for all execution speeds which generate the same trace for
an individual process. A weak formula is true if and only
if there exists one global sequence in which it is true. In
other words, the predicate can be made true by choosing
appropriate execution speeds of various processors.
The difficulty of checking truthness of a global predicate
arises from two sources. First, if there are n processes in
the system, the total number of global sequences (in which
a global state is not repeated) is exponential in n and the
size of the traces. Secondly, the global state is distributed
across the network during an actual run. Thus, detection
of any general predicate in the above logic is not feasible
in a distributed program. To avoid the problem of combinatorial
explosion, we focus on detection of predicates
belonging to a class that we believe captures a large sub-set
of predicates interesting to a programmer. We use the
word local to refer to a predicate or condition that involves
the state of a single process in the system. Such a condition
can be easily checked by the process itself. We detect
predicates that are boolean expressions of local predicates.
Following are examples of the formulas detectable by our
algorithms:
1. Suppose we are developing a mutual exclusion algo-
rithm. Let CS i represent the local predicate that the process
P i is in critical section. Then, the following formula
detects any possibility of violation of mutual exclusion for
a particular run:
2. In the example 4, we can check if
Note that
is not true for the global sequence g, but it is true for the
global sequence h. Our algorithm will detect the above
predicate to be true for the run r even though the global
sequence executed may be g.
3. Assume that in a database application, serializability is
enforced using a two phase locking scheme [15]. Further
assume that there are two types of locks: read and write.
Then, the following formula may be useful to identify an
error in implementation:
III. Weak Conjunctive Predicates
A weak conjunctive predicate (WCP) is true for a given
run if and only if there exists a global sequence consistent
with that run in which all conjuncts are true in some global
state. Practically speaking, this type of predicate is most
useful for bad or undesirable predicates (i.e. predicates that
should never become true). In such cases, the programmer
would like to know whenever it is possible that the bad
predicate may become true. As an example, consider the
classical mutual exclusion situation. We may use a WCP
to check if the correctness criterion of never having two or
more processes in their critical sections at the same time is
met. We would want to detect the predicate "process x is in
its critical section and process y is in its critical section". It
is important to observe that our algorithms will report the
possibility of mutual exclusion violation even if it was not
violated in the execution that happened. The detection
will occur if and only if there exists a consistent cut in
which all local predicates are true. Thus, our techniques
detect errors that may be hidden in some run due to race
conditions.
A. Importance of Weak Conjunctive Predicates
Conjunctive predicates form the most interesting class of
predicates because their detection is sufficient for detection
of any global predicate which can be written as a boolean
expression of local predicates. This observation is shown
below:
Lemma 5 Let p be any predicate constructed from local
predicates using boolean connectives. can be
detected using an algorithm that can detect
is a pure conjunction of local predicates.
Proof: We first write p in its disjunctive normal form.
Thus, E: 3
a pure conjunction of local predicates. Next, we observe
that
f semantics of E and 3 g
f semantics of -g
f semantics of E and 3 g
Thus, the problem of detecting is reduced to solving
l problems of detecting is a pure conjunction
of local predicates.
Our approach is most useful when the global predicate
can be written as a boolean expression of local predicates.
As an example, consider a distributed program in which
y and z are in three different processes. Then,
can be rewritten as
where each part is a weak conjunctive predicate.
We note that even if the global predicate is not a boolean
expression of local predicates, but it is satisfied by only a
finite number of possible global states, then it can again be
rewritten as a disjunction of weak conjunctive predicates.
For example, consider the predicate
x and y are in different processes. is not a local
predicate as it depends on both processes. However, if we
know that x and y can only take values f0; 1g, then the
above expression can be rewritten as
This is equivalent to
Each of the disjunct in this expression is a weak conjunctive
predicate.
We observe that predicates of the form A : 2bool can
also be easily detected as they are simply duals of
which can be detected as shown in Section .
In this paper, we have emphasized conjunctive predicates
and not disjunctive predicates. The reason is that
disjunctive predicates are quite simple to detect. To detect
a disjunctive predicate E:3LP 1 - LP 2 - LPm , it
is sufficient for the process P i to monitor LP i . If any of
the process finds its local predicate true, the disjunctive
predicate is true.
B. Conditions for Weak Conjunctive Predicates
We use LP i to denote a local predicate in the process P i ,
and LP i (s) to denote that the predicate LP i is true in the
state s. We say that occurs in the sequence
r[i].
Our aim is to detect whether E: 3(LP 1 -LP
holds for a given r. We can assume m - n because LP i -
LP j is just another local predicate if LP i and LP j belong
to the same process. We now present a theorem which
states the necessary and sufficient conditions for a weak
conjunctive predicate to hold.
Theorem 6 E: 3(LP 1 -LP true for a run
r iff for all 1 - such that LP i is true in
state s i , and s i and s j are incomparable for i 6= j. That is,
r
ks
Proof: First assume that E: 3(LP 1 - LP
true for the run r. By definition, there is a global sequence
2 linear(r) which has a global state, g   where all local
predicates are true. We define s
r[i]). Now consider any two distinct
indices i and j between 1 and m. Since s i and s j correspond
to the same global state, s i and s j must be incomparable
by (S2). Therefore, 9s
ks
We prove the other direction (() for 2. The proof
for the general case is similar. Assume that there exist
states such that states s 1 and s 2 are
incomparable, and LP 1 This implies that
there is no message path from s 1 to s 2 or vice-versa. Thus,
any message received in or before s 2 could not have been
sent after s 1 and any message received in or before s 1 could
not have been sent after s 2 . Fig. 1. illustrates this. Thus
1. 1.
2.
2. P1 freezes at s1 and
P2 executes until s2.
2.
step 1. P1 and P2 execute until
P1 at s1 and P2 before s2
Fig. 1. Incomparable States Producing A Single Global
State
it is possible to construct the following execution (global
1. Let both processes execute consistent with the run r
until either P 1 is at s 1 and P 2 is before s 2 , or P 2 is at s 2
and P 1 is before s 1 . Assume without loss of generality
that the former case holds.
2. Freeze P 1 at s 1 and let P 2 execute until it is at s 2 .
This is possible because there is no message sent after
received before s 2 .
We now have a global state g
are true in g   .
IV. Detection of Weak Conjunctive Predicates2
[1,0,0]
[1,1,0]
Fig. 2. Examples of lcmvectors
Theorem 6 shows that it is necessary and sufficient to
find a set of incomparable states in which local predicates
are true to detect a weak conjunctive predicate. In this
section, we present a centralized algorithm to do so. Later,
we will see how the algorithm can be decentralized. In
this algorithm, one process serves as a checker. All other
processes involved in WCP are referred to as non-checker
processes. These processes, shown in Fig. 3, check for local
predicates.
Each non-checker process keeps its own local lcmvector
(last causal message vector) of timestamps. These timestamp
vectors are slight a modification of the virtual time
vectors proposed by [6,17]. For the process P j , lcmvec-
tor[i] (i 6= j) is the message id of the most recent message
from P i (to anybody) which has a causal relationship to
for the process P j is the next message id
that P j will use. To maintain the lcmvector information,
we require every process to include its lcmvector in each
program message it sends. Whenever a process receives a
program message, it updates its own lcmvector by taking
the component-wise maximum of its lcmvector and the one
contained in the message. Fig. 2 illustrates this by showing
lcmvector in each interval. Whenever the local
predicate of a process becomes true for the first time since
the most recently sent message (or the beginning of the
trace), it generates a debug message containing its local
timestamp vector and sends it to the checker process.
One of the reasons that the above algorithm is practical
is that a process is not required to send its lcmvector every
time the local predicate is detected. A simple observation
tells us that the lcmvector need not be sent if there has
been no message activity since the last time the lcmvector
was sent. This is because the lcmvector can change its
value only when a message is sent or received. We now
show that it is sufficient to send the lcmvector once after
each message is sent irrespective of the number of messages
received.
Let local(s) denote that the local predicate is true in
state s. We define the predicate first(s) to be true iff
the local predicate is true for the first time since the most
recently sent message (or the beginning of the trace). We
var
lcmvector: array [1.n] of integer;
last causal msg rcvd from process 1 to n*/
firstflag: boolean init true;
local pred: Boolean Expression;
/*the local pred. to be tested by this process*/
2 For sending do
send (prog,
Upon receive (prog, msg
Upon (local pred = true)- firstflag do
firstflag := false;
send (dbg, lcmvector) to the checker process;
Fig. 3. Algorithm for weak conjunctive predicates -
nonchecker process P id
say are the states
in different processes making the wcp true (as in Theorem
6).
Theorem 7 9s
Proof: (() is trivially true. We show ()). By symmetry
it is sufficient to prove the existence of s 0
1 such that
1 as the first
state in the trace of P 1 since the most recently sent message
or the beginning of the trace such that local(s 0
true. As s 1 exists, we know that s 0
exists. By our
choice of s 0
1 ) is true. Our proof obligation is to
show that wcp(s 0
It is sufficient to show that
ks m. For any s j , s 1 6! s j and there is
no message sent after s 0
Also s j 6! s 0
imply
that contradiction. Therefore, we conclude that
ks j for any 2 - j - m.
We now analyze the complexity of non-checker processes.
The space complexity is given by the array lcmvector and
is O(n). The main time complexity is involved in detecting
the local predicates which is the same as for a sequential
debugger. Additional time is required to maintain time
vectors. This is O(n) for every receive of a message. In
the worst case, one debug message is generated for each
program message sent, so the worst case message complexity
is O(m s s is the number of program messages
sent. In addition, program messages have to include time
vectors.
We now give the algorithm for the checker process which
detects the WCP using the debug messages sent by other
processes. The checker process has a separate queue for
each process involved in the WCP. Incoming debug messages
from processes are enqueued in the appropriate queue.
We assume that the checker process gets its message from
any process in FIFO order. Note that we do not require
FIFO for the underlying computation. Only the detection
algorithm needs to implement FIFO property for efficiency
purposes. If the underlying communication is not
FIFO, the checker process can ensure that it receives messages
from non-checker processes in FIFO by using sequence
numbers in messages.
The checker process applies the following definition to
determine the order between two lcmvectors. For any two
lcmvectors, u and v,
Furthermore, if we know the
processes the vectors came from, the comparison between
two lcmvectors can be made in constant time. Let P roc :
ng map a lcmvector to the process it belongs
to. Then, the required computation to check if the
lcmvector u is less than the lcmvector v is
Lemma 8 Let s and t be states in processes P i and P j with
lcmvectors u and v, respectively. Then,
t, then there is a message path from s to t. There-
fore, since P j updates its lcmvector upon receipt of a message
and this update is done by taking the component-wise
maximum, we know the following holds:
Furthermore, since v[j] is the next message id to be used
by could not have seen this value as t 6! s. We
thereby know that v[j] ? u[j]. Hence, the following holds:
We now show that :(s ! t)
by the first
part of this theorem. If (skt)) then there is no message
path from the state s to the state t or vice-versa. Hence,
when P i is at s and P j is at t,
Therefore,
Thus, the task of the checker process is reduced to checking
ordering between lcmvectors to determine the ordering
between states. The following observation is critical for reducing
the number of comparisons in the checker process:
Lemma 9 If the lcmvector at the head of one queue is
less than the lcmvector at the head of any other queue,
then the smaller lcmvector may be eliminated from further
consideration in checking to see if the WCP is satisfied.
Proof: In order for the WCP to be satisfied, we must find
a set of lcmvectors, one from each queue, such that each is
incomparable with all the others in the set. If the lcmvector
at the head of one queue (q i ) is less than that at the head of
another queue (q j ), we know it will be less than any other
lcmvectors in q j because the queues are in increasing order
from head to tail. Also any later arrivals into q j must be
greater than that at the head of q i . Hence, no entry in q j
will ever be incomparable with that at the head of q i so the
head of q i may be eliminated from further consideration in
checking to see if the WCP is satisfied.
The algorithm given in Fig. 4 is initiated whenever any
new lcmvector is received. If the corresponding queue is
non-empty, then it is simply inserted in the queue; other-
wise, there exists a possibility that the conjunctive predicate
may have become true. The algorithm checks for
var
changed, newchanged: set of f1,2,.,mg
Upon recv(elem) from P k do
changed
while (changed 6= OE) begin
newchanged := fg;
for i in changed, and j in f1,2,.,m gdo
begin
newchanged:=newchanged [ fig;
newchanged:=newchanged [ fjg;
changed := newchanged;
for i in changed do deletehead(q i );
end;/* while */
Fig. 4. Algorithm for weak conjunctive predicates - the
checker process
incomparable lcmvectors by comparing only the heads of
queues. Moreover, it compares only those heads of the
queues which have not been compared earlier. For this
purpose, it uses the variable changed which is the set of
indices for which the head of the queues have been up-
dated. The while loop maintains the invariant:
This is done by finding all those elements which are lower
than some other elements and including them in changed.
This means that there can not be two comparable elements
in f1; 2; :::; mg \Gamma changed. The loop terminates when
changed is empty. At that point, if all queues are non-
empty, then by the invariant I, we can deduce that all the
heads are incomparable. Let there be m queues with at
most p elements in any queue. The next theorem deals
with the complexity of the above algorithm.
Theorem 10 The above algorithm requires at most O(m 2 p)
comparisons.
Proof: Let comp(k) denote the number of comparisons required
in the k th iteration of the while loop. Let t denote
the total number of iterations of the while loop. Then, the
total number of comparisons equals
represent the value of changed at the k th it-
eration. jchanged(k)j for k - 2 represents the number
of elements deleted in the iteration of the while
loop. From the structure of the for-loops we get that
Therefore, the total number
of comparisons required are
The following theorem proves that the complexity of the
above problem is at
thus showing that our
algorithm is optimal [8].
Theorem 11 Any algorithm which determines whether there
exists a set of incomparable vectors of size m in m chains
of size at most p, makes at least pm(m \Gamma 1)=2 comparisons.
Proof: We first show it for the case when the size of each
queue is exactly one, i.e. 1. The adversary will give to
the algorithm a set in which either zero or exactly one pair
of elements are comparable. The adversary also chooses
to answer "incomparable" to first m(m \Gamma
tions. Thus, the algorithm cannot determine if the set has
a comparable pair unless it asks about all the pairs.
We now show the result for a general p. Let q i [k] denote
the k th element in the queue q i . The adversary will give
the algorithm q i 's with the following characteristic:
Thus, the above problem reduces to p instances of the problem
which checks if any of the m elements is incompara-
ble. If the algorithm does not completely solve one instance
then the adversary chooses that instance to show m queues
consistent with all the its answers but different in the final
outcome.
V. Decentralization of the Detection Algorithm
We now show techniques for decentralizing the above
algorithm. From the property (P1), we can deduce that if
a set of vectors S forms an anti-chain (that is all pairs of
vectors are incomparable), then the following holds:
8 distinct s; t
We denote this condition by the predicate inc(S). The following
theorem shows that the process of checking inc(S)
can be decomposed into that of checking it for smaller sets.
Theorem 12 Let U be sets of lcmvectors, such
that
by taking componentwise maximum of all vectors in the set
X. Then,
inc(S) iff inc(T
inc(T ) and inc(U ) are clearly true because
We show that
The other conjunct is proved in a similar fashion.
From (P 2), we deduce that 8 distinct s; t
s[P roc(t)]. This means that max T [P
by the definition of max T . From (P 2), we also deduce
that 8 u This means that
by the definition of maxU .
From the above two assertions we conclude that
We will show that (P 2) holds for S, i.e.
8 distinct s; t
If both s and t belong either to T and U , then the above
is true from inc(T ) and inc(U ). Let us assume without
loss of generality that t 2 T and u 2 U . We need to show
that t[P roc(t)] ? u[P roc(t)] (the other part is proved sim-
ilarly). From inc(T ) we conclude that,
t[P roc(t)]. And now from max T [P roc(t)] ? maxU [P roc(t)]
we conclude that t[P roc(t)] ? u[P roc(t)].
Using the above theorem and the notions of a hierar-
chy, the algorithm for checking WCP can be decentralized
as follows. We may divide the set of processes into two
groups. The group checker process checks for WCP within
its group. On finding one, it sends the maximum of all
lcmvectors to a higher process in the hierarchy. This process
checks the last two conjuncts of the above theorem.
Clearly, the above argument can be generalized to a hierarchy
of any depth.
Example 13 Consider a distributed program with four
processes. Let the lcmvectors corresponding to these processes
be
Now instead of checking whether the entire set consists of
incomparable vectors, we divide it into two subsets
We check that each one of them is incomparable. This computation
can be done by group checker processes. Group
to the higher-level process. This process can check that
strictly greater than maxU in the first two components
and maxU is strictly greater than max T in the last
two components. Hence, by Theorem 12, all vectors in the
set S are pairwise incomparable.
VI. Implementation: UTDDB
The main application of our results are in debugging
and testing of distributed programs. We have incorporated
our algorithms in the distributed debugger called UTDDB
(University of Texas Distributed Debugger) [14]. The on-line
debugger is able to detect global states or sequences of
global states in a distributed computation. UTDDB consists
of two types of processes - coordinator and monitor
type. There exists only one coordinator process, but the
number of monitor processes is the same as the number of
application processes in the underlying distributed computation

The coordinator process serves as the checker process
for WCP as well as the user-interface of UTDDB to the
programmer. It accepts input from the programmer such
as distributed predicates to be detected. It also reports to
the programmer if the predicate is detected.
Monitor process are hidden from the programmer. Each
of the monitor processes, detects local predicates defined
within the domain of the application process it is monitor-
ing. This is done by single stepping the program. After
each step, the monitor examines the address space of the
application process to check if any of the simple predicates
in its list are true. It is also responsible to implement algorithms
described as a non-checker process in Section . In
particular, it maintains the vector clock mechanism.
In a distributed debugger, the delays between occurrence
of a predicate, its detection and halting of the program may
be substantial. Thus, when the program is finally halted,
it may no longer be in a state the programmer is interested
in. Therefore, for the weak conjunctive predicate, UT-
DDB gives the programmer the option of rolling back the
distributed computation to a consistent global state where
the predicate is true. The coordinator uses the set of timestamps
that detected the WCP predicate to calculate this
global state which it then sends to all the monitors. As the
application processes execute, they record incoming events
to a file. So, when a monitor receives a message telling it to
roll back an application process, the monitor restarts the
application process and replays the recorded events until
the process reaches a local state that is part of the global
state where the weak conjunctive predicate is true. Such
a restart assumes that the only non-determinism in the
program is due to reordering of messages.
Our algorithms are also used in a trace analyzer (another
part of UTDDB) for distributed programs [4]. Our analyzer
monitors a distributed program and gathers enough
information to form a distributed run as described in Section
II. This approach reduces the probe effect that the
distributed program may experience if the detection was
carried out while the program was in execution. The user
can then ask UTDDB whether any predicate expressed in a
subset of the logic described in this paper ever became true.
We are currently extending these algorithms for detection
of sequences of global predicates [1,9,25], and relational
global predicates [24].
VII. Conclusions
We have discussed detection of global predicates in a
distributed program. Earlier algorithms for detection of
global predicates proposed by Chandy and Lamport work
only for stable predicates. Our algorithms detect even unstable
predicates with reasonable time, space and message
complexity.
Our experience with these algorithms has been extremely
encouraging. In the current implementation, the main
overhead is in the local monitor process for checking local
predicates. By providing special hardware support even
this overhead can be reduced. For example, most architectures
provide special hardware support such as break-point
traps if certain location is accessed. This feature can
be used to make detection of local predicates of the form
(program at line x) very efficient.
We believe that algorithms presented in this paper should
be part of every distributed debugger because they incur
low overhead, and are quite useful in identifying errors in
the program.

Acknowledgements

We would like to thank Bryan Chin, Mohamed Gouda,
Greg Hoagland, Jay Misra, William Myre, Don Pazel, and
Alex Tomlinson for their comments and observations which
have enabled us to strengthen this work. We would also
like to thank Bryan Chin for implementing offline versions
of our algorithms and Greg Hoagland for incorporating our
algorithms in UTDDB. We would also like to thank anonymous
referees for their meticulous review of an earlier version
of the paper.



--R

"Distributed Debugging Tools for Heterogeneous Distributed Systems"
"Repeated Snapshots in Distributed Systems with Synchronous Communication and Their Implementation in CSP"
"Distributed Snapshots: Determining Global States of Distributed Systems"
"An Offline Debugger for Distributed Programs"
"Consistent Detection of Global Predicates"
"Partial Orders for Parallel Debugging"
"Causal Distributed Break- points"
"Some Optimal Algorithms for Decomposed Partially Ordered Sets,"
"Concurrent Regular Expressions and their Relationship to Petri Net Languages,"
"Detection of Unstable Predicate in Distributed Programs,"
"Global events and global breakpoints in distributed systems"
"Detecting Atomic Sequences of Predicates in Distributed Computations,"
"Computing Particular Snapshots in Distributed Systems"
"A Debugger for Distributed Programs"
Database System Concepts
"Time, Clocks, and the Ordering of Events in a Distributed System"
"Virtual time and global states of distributed sys- tems"
"Debugging Concurrent Programs"
"Breakpoints and Halting in Distributed Programs"
"Detecting Causal Relationships in Distributed Computations: In Search of the Holy Grail"
"The Complexity of Propositional Linear Temporal Logic"
"Efficient Distributed Snapshots"
"A General Approach to Recognizing Event Occurrences in Distributed Computations"
"Detecting Relational Global Predicates in Distributed Systems,"
"Detection of Unstable Predicates in Debugging Distributed Programs"
--TR
The complexity of propositional linear temporal logics
Database system concepts
Repeated snapshots in distributed systems with synchronous communications and their implementation in CSP
Global events and global breakpoints in distributed systems
Partial orders for parallel debugging
Debugging concurrent programs
Consistent detection of global predicates
Detection of unstable predicates in debugging distributed programs
Concurrent regular expressions and their relationship to Petri nets
Some optimal algorithms for decomposed partially ordered sets
Detecting relational global predicates in distributed systems
Detecting atomic sequences of predicates in distributed computations
Distributed snapshots
Time, clocks, and the ordering of events in a distributed system
Detection of Unstable Predicates in Distributed Programs

--CTR
Vijay K. Garg, Methods for Observing Global Properties in Distributed Systems, IEEE Parallel & Distributed Technology: Systems & Technology, v.5 n.4, p.69-77, October 1997
Sujatha Kashyap , Vijay K. Garg, Intractability results in predicate detection, Information Processing Letters, v.94 n.6, p.277-282,
Hsien-Kuang Chiou , Willard Korfhage, Enhancing Distributed Event Predicate Detection Algorithms, IEEE Transactions on Parallel and Distributed Systems, v.7 n.7, p.673-676, July 1996
Loon-Been Chen , I-Chen Wu, An Efficient Distributed Online Algorithm to Detect Strong Conjunctive Predicates, IEEE Transactions on Software Engineering, v.28 n.11, p.1077-1084, November 2002
Punit Chandra , Ajay D. Kshemkalyani, Distributed algorithm to detect strong conjunctive predicates, Information Processing Letters, v.87 n.5, p.243-249, 15 September
Karun N. Biyani , Sandeep S. Kulkarni, Testing Dynamic Adaptation in Distributed Systems, Proceedings of the Second International Workshop on Automation of Software Test, p.10, May 20-26, 2007
Ajay D. Kshemkalyani, A Fine-Grained Modality Classification for Global Predicates, IEEE Transactions on Parallel and Distributed Systems, v.14 n.8, p.807-816, August
Michel Hurfin , Masaaki Mizuno , Mukesh Singhal , Michel Raynal, Efficient Distributed Detection of Conjunctions of Local Predicates, IEEE Transactions on Software Engineering, v.24 n.8, p.664-677, August 1998
Sujatha Kashyap , Vijay K. Garg, Exploiting predicate structure for efficient reachability detection, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA
Guy Dumais , Hon F. Li, Distributed Predicate Detection in Series-Parallel Systems, IEEE Transactions on Parallel and Distributed Systems, v.13 n.4, p.373-387, April 2002
Craig M. Chase , Vijay K. Garg, Detection of global predicates: techniques and their limitations, Distributed Computing, v.11 n.4, p.191-201, October 1998
Vijay K. Garg , Brian Waldecker, Detection of Strong Unstable Predicates in Distributed Programs, IEEE Transactions on Parallel and Distributed Systems, v.7 n.12, p.1323-1333, December 1996
Scott D. Stoller, Detecting global predicates in distributed systems with clocks, Distributed Computing, v.13 n.2, p.85-98, April 2000
Punit Chandra , Ajay D. Kshemkalyani, Causality-Based Predicate Detection across Space and Time, IEEE Transactions on Computers, v.54 n.11, p.1438-1453, November 2005
Anish Arora , Sandeep S. Kulkarni , Murat Demirbas, Resettable vector clocks, Journal of Parallel and Distributed Computing, v.66 n.2, p.221-237, February 2006
Anirban Majumdar , Clark Thomborson, Manufacturing opaque predicates in distributed systems for code obfuscation, Proceedings of the 29th Australasian Computer Science Conference, p.187-196, January 16-19, 2006, Hobart, Australia
Felix C. Grtner, Fundamentals of fault-tolerant distributed computing in asynchronous environments, ACM Computing Surveys (CSUR), v.31 n.1, p.1-26, March 1999
weak unstable predicates;distributed memory systems;distributed programs;programtesting;global predicates;sun workstations;testing;UNIX;program debugging;debugging;distributed algorithms;distributed debugger;weakconjunctive predicates;message complexity;index termscommunication complexity