Efficient Distributed Detection of Conjunctions of Local Predicates.
AbstractGlobal predicate detection is a fundamental problem in distributed systems and finds applications in many domains such as testing and debugging distributed programs. This paper presents an efficient distributed algorithm to detect conjunctive form global predicates in distributed systems. The algorithm detects the first consistent global state that satisfies the predicate even if the predicate is unstable. Unlike previously proposed run-time predicate detection algorithms, our algorithm does not require exchange of control messages during the normal computation. All the necessary information to detect predicates is piggybacked on computation messages of application programs. The algorithm is distributed because the predicate detection efforts as well as the necessary information are equally distributed among the processes. We prove the correctness of the algorithm and compare its performance with respect to message, storage, and computational complexities with that of the previously proposed run-time predicate detection algorithms.
Introduction
Development of distributed applications requires the ability to analyze their behavior
at run time whether to debug or control the execution. In particular, it is sometimes
essential to know if a property is satisfied (or not) by a distributed computation.
Properties of the computation, which specify desired (or undesired) evolutions of the
program's execution state, are described by means of predicates over local variables
of component processes.
A basic predicate refers to the program's execution state at a given time. These
predicates are divided into two classes called local predicates and global predicates.
A local predicate is a general boolean expression defined over the local state of a
single process, whereas a global predicate is a boolean expression involving variables
managed by several processes. Due to the asynchronous nature of a distributed
computation, it is impossible for a process to determine the total order in which
the events occurred in the physical time. Consequently, it is often impossible to determine
the global states through which a distributed computation passed through,
complicating the task of ascertaining if a global predicate became true during a
computation.
Basic predicates are used as building blocks to form more complex class of predicates
such as linked predicates [14], simple sequences [5, 9, 1], interval-constrained
sequences [1], regular patterns [4] or atomic sequences [8, 9]. The above class of properties
are useful in characterizing the evolution of the program's execution state,
and protocols exist for detecting these properties at run time by way of language
recognition techniques [2].
When the property (i.e., a combination of the basic properties) contains no
global predicate, the detection can be done locally without introducing any delays,
without defining a centralized process and without exchanging any control messages.
Control information is just piggybacked to the existing message of the application.
However, if the property refers at least to one global predicate, then all possible
observations of the computation must be considered. In other words, the detection
of the property requires the construction and the traversal of the lattice of consistent
global states representing all observations of the computation. When the property
reduces to one global predicate, the construction of the lattice can be avoided in
some cases. If the property is expressed as a disjunction of local predicates, then
obviously no cooperation between processes is needed in order to detect the property
during a computation. A form of global predicate, namely, the conjunction of local
predicates, has been the focus of research [5, 6, 7, 12, 17] during the recent years. In
such predicates, the number of global states of interest in the lattice is considerably
RR
4 M. Hurfin, M. Mizuno, M. Raynal, M. Singhal
reduced because all global states that includes a local state where the local predicate
is false need not be examined.
Previous Work
The problem of global predicate detection has attracted considerable attention lately
and a number of global predicate detection algorithms have been proposed in the
recent past. In the centralized algorithm of Cooper and Marzullo [3], every process
reports each of its local states to a process, which builds a lattice of the global
computation and checks if a state in the computation satisfies the global predicate.
The power of this algorithm lies in generality of the global predicates it can detect;
however, the algorithm has a very high overhead. If a computation has n processes
and if m is the maximum number of events in any process, then the lattice consists
of O(m n ) states in the worst case. Thus, the worst case time complexity of this
algorithm is O(m n ). The algorithm in [10] has linear space complexity; however, the
worst case time complexity is still linear in the number of states in the lattice.
Since the detection of generalized global predicates by building and searching
the entire state space of a computation is utterly prohibitive, researchers have developed
faster, more efficient global predicate detection algorithms by restricting
themselves to special classes of predicates. For example, a form of global predicate
that is expressed as the conjunction of several local predicates has been the focus of
research [5, 6, 7, 12, 17] recently. Detection of such predicates can be done during
a replay of the computation [12, 17] or during the initial computation [5, 6, 7].This
paper focus on the second kind of solution which allows one to detect the predicate
even before the end of the computation. In the Garg-Waldecker centralized algorithm
to detect such predicates [6], a process gathers information about the local states
of the processes, builds only those global states that satisfy the global predicate,
and checks if a constructed global state is consistent. In the distributed algorithm of
Garg and Chase [7], a token is used that carries information about the latest global
consistent state (cut) such that the local predicates hold at all the respective local
states. The worst case time complexity of both these algorithms is O(mn 2 ) which
is linear in m and is much smaller than the worst case time complexity of the methods
that require searching the entire lattice. However, the price paid is that not
all properties can be expressed as the conjunction of local predicates.
Recently, Stoller and Schneider [16] proposed an algorithm that combines the
Garg-Waldecker approach [6] with any approach that constructs a lattice to detect
Possibly(\Phi). distributed computation satisfies Possibly(\Phi) iff predicate \Phi holds
in a state in the corresponding lattice.) This algorithm has the best features of both
INRIA
Efficient Distributed Detection of Conjunctions of Local Predicates 5
the approaches - it can detect Possibly(\Phi) for any predicate \Phi and it detects a global
predicate expressed as the conjunction of local predicates in time linear in m (the
maximum number of events in any process).
Paper Objectives
This paper presents an efficient distributed algorithm to detect conjunctive form global
predicates in distributed systems. We prove the correctness of the algorithm and
compare its performance with that of the previous algorithms to detect conjunctive
form global predicates.
The rest of the paper is organized as follows: In the next section, we define system
model and introduce necessary definitions and notations. Section 3 presents the
first global predicate detection algorithm and gives a correctness proof. The second
algorithm is presented in Section 4. In Section 5, we compare the performance of
the proposed algorithms with the existing algorithms for detecting conjunctive form
global predicates. Finally, Section 6 contains the concluding remarks.
System Model, Definitions, and Notations
2.1 Distributed Computations
A distributed program consists of n sequential processes denoted by P 1
The concurrent execution of all the processes on a network of processors is called
a distributed computation. The processes do not share a global memory or a global
clock. Message passing is the only way for processes to communicate with one
another. The computation is asynchronous: each process evolves at his own speed
and messages are exchanged through communication channels, whose transmission
delays are finite but arbitrary. We assume that no messages are altered or spuriously
introduced. No assumption is made about the FIFO nature of the channels.
2.2 Events
2.2.1 Definition and Notations
Activity of each process is modeled by a sequence of events (i.e., executed action).
Three kinds of events are considered: internal, send, and receive events. Let e x
the x th event which occurs at process P i . Figure 1 shows an example of distributed
computation involving two processes P 1 and P 2 . In this example, event e 2
1 is a send
event and event e 1
2 is the corresponding receive event. Event e 1
1 is an internal event.
RR
6 M. Hurfin, M. Mizuno, M. Raynal, M. Singhal
Figure

1: A distributed computation
For each process P i , we define an additional internal event denoted as e 0
i that
occurred at process P i at the beginning of the computation. So, during a given
computation, execution of process P i is characterized by a sequence of events:
Furthermore, if the computation terminates, the last action executed at process
(denoted as e m i
by an imaginary internal event denoted as e m i +1
2.2.2 Causal Precedence Relation Between Events
The "happened-before" causal precedence relation of Lamport induces a partial
order on the events of a distributed computation. This transitive relation, denoted
by OE, is defined as follows:
8e x
or
There exists a message m such that
i is a send event (sending of m to P j
e y
j is a receive event (receiving of m from
or
There exists an event e z
such
k and e z
This relation is extended to a reflexive relation denoted .
INRIA
Efficient Distributed Detection of Conjunctions of Local Predicates 7
2.3 Local states
2.3.1 Definition and Notations
At a given time, the local state of a process P i is defined by the values of the
local variables managed by this process. Although occurrence of an event does not
necessarily cause a change of the local state, we identify the local state of a process
at a given time with regard to the last occurrence of an event at this process. We
use oe x
i to denote the local state of P i during the period between event e x
i and event
e x+1
. The local state oe 0
i is called the initial state of process P i .
Figure

2: Local states of processes
2.3.2 Causal Precedence Relation Between Local States
The definition of the causal precedence relation between states (denoted by \Gamma!) is
based on the happened-before relation between events. This relation is defined as
follows:
8oe x
Two local states oe x
i and oe y
are said to be concurrent if there is no causal dependency
between them (i.e., oe x
j and oe y
A set of local states is consistent if any pair of elements are concurrent. In the
distributed computation shown in Figure 2, foe 0
2 g and foe 2,oe 4
2 g are three
examples of consistent sets of local states.
RR
8 M. Hurfin, M. Mizuno, M. Raynal, M. Singhal
2.4 Intervals
2.4.1 Definition and Notations
Since causal relations among local states of different processes are caused by send and
receive events, we introduce the notion of intervals to identify concurrent sequences
of states of a computation. An interval is defined to be a segment of time on a
process that begins with a send or receive event (called a communication event) and
ends with the next send or receive event. Thus, a process execution can be viewed
as a consecutive sequence of intervals.
In order to formally define intervals, we first introduce a new notation to identify
communication events. We use " x
i to denote the x th send or receive event at P i . Thus,
for each " x
i , there exists exactly one e y
i that denotes the same event. Furthermore, the
imaginary event e 0
are renamed as " 0
. If the computation terminates, imaginary
event
i at process P i is renamed as " l i +1
(l i is the number of communication
events that occurred at process P i ).
The x th interval of process P i , denoted by '
i , is a segment of the computation
that begins at "
and ends at " x
. Thus, the first interval at P i is denoted by ' 0
. If
the computation terminates, the last interval of process P i is identified by ' l i
Figure

3: The corresponding set of intervals
We say that interval ' x
i contains the local state oe y
(or oe y
i is contained in ' x
the following property holds: (" x
This relation is denoted
by oe y
. If this relation does not hold, it is denoted by oe y
. By definition,
any interval contains at least one local state.
INRIA
Efficient Distributed Detection of Conjunctions of Local Predicates 9
2.4.2 Causal Precedence Relation Between Intervals
The relation that expresses causal dependencies among intervals is denoted as !.
This relation induces a partial order on the intervals of distributed computation and
is defined as follows:
A set of intervals is consistent if for any pair of intervals in the set, say ' x
2.5 Global States
A global state (or cut) is a collection of n local states containing exactly one local
state from each process P i . A global state is denoted by f oe x 1
g. If a
global state f oe x 1
is consistent, it is identified by
The set of all consistent global states of a distributed computation form a lattice
whose minimal element is the initial global state \Sigma(0; 0;
from the distributed
computation can reach the latter from the former when process P i executes its next
event
i . Each path of the lattice starting at the minimal element corresponds to
a possible observation of the distributed computation. Each observation is identified
by a sequence of events where all events of the computation appear in an order
consistent with the "happen before" relation of Lamport. The maximal element
called the final global state and exists only if all the processes
of the distributed computation have terminated.
Given a computation and a predicate on a global state \Phi, we can use the two
modal operators proposed by Cooper and Marzullo [3] to obtain two different pro-
perties, namely, Possibly(\Phi) and Definitely(\Phi). A distributed computation satisfies
if and only if the lattice has a consistent global state verifying the
predicate \Phi, whereas Definitely(\Phi) is satisfied by the computation if and only if
each observation (i.e., each path in the lattice) passes through a consistent global
state verifying \Phi. In this paper, we focus on the class of global predicates formed
as the conjunction of local predicates and we consider only the first satisfaction
rule: Possibly(\Phi). This rule is particularly attractive to test and debug distributed
executions.
RR
M. Hurfin, M. Mizuno, M. Raynal, M. Singhal
2.6 Conjunctions of Local Predicates
A local predicate defined over the local state of process P i is denoted as L i . Notation
oe x
indicates that the local predicate L i is satisfied when process P i is in the
local state oe x
. Due to its definition, a local predicate L i can be evaluated by process
P i at any time without communicating with any other process.
We extend the meaning of symbol j= to intervals as follows:
i such that (oe y
Let \Phi denote a conjunction of p local predicates. Without loss of generality, we
assume that the p processes involved in the conjunction \Phi are . In this
paper, we write either \Phi or to denote the conjunction.
A set of p local states f oe x 1
p g is called a solution if and only if:? !
p g is a consistent set.
A global state \Sigma(x 1 called a complete solution if this set of local
states includes a solution.
By definition, Possibly(\Phi) is verified if there exists a complete solution. A consistent
set of local states containing less than n local states may be completed to form
a consistent global state (i.e., a consistent set of n elements), and thus, a solution
may be extensible to one or more complete solutions. The goal of a detection algorithm
is not to calculate the whole set of complete solutions but only to determine
a solution. This approach is not restrictive. In order to deal with complete solutions
rather than with solutions, a programmer can simply add to the conjunction,
local predicates L are true in any local state. Consequently,
we will no longer speak about complete solution.
Due to the link between local states and intervals, the following definition of a
solution is obviously consistent with the first one.
A set of p local states f oe y 1
p g is a solution iff there exists a set of
p g is a consistent set.
INRIA
Efficient Distributed Detection of Conjunctions of Local Predicates 11
Let S denote the set of all solutions. If S is not empty, the first solution is the
unique element of S denoted by f oe f 1
p g such that every element
p g of S satisfies the following property:
As the property to detect is expressed as a conjunction of local predicates, this
particular solution, if it exists, is well defined in the computation. The set of intervals
that includes this solution is also well defined. We denote this set of intervals
and we say that this set of intervals is the first one which verifies
\Phi.
3 Detection Algorithms for Conjunction of Local Predicate

3.1

Overview

As mentioned in the previous section, Possibly(\Phi) is verified by detecting a set of
concurrent intervals, each of which verifies its local predicate. We have developed
the following two approaches to resolve this problem:
1. In the first approach, processes always keep track of sets of concurrent intervals.
For each such set, each process checks whether its interval in the set verifies
its local predicate.
2. In the second approach, a process always keeps track of a set of intervals,
each of which verifies its local predicate. For each such set, the process checks
whether all intervals in the set are concurrent.
Thus, algorithms designed for those complementary approaches are dual of each
other. This section described the algorithm corresponding to the first approach in
detail, including its correctness proof. The next section describes an algorithm corresponding
to the second approach.
3.2 The First Algorithm
3.2.1 Dependency Vectors
To identify a set of p concurrent intervals, the algorithm keeps track of causal dependencies
among intervals by using a vector clock mechanism similar to that described
RR
M. Hurfin, M. Mizuno, M. Raynal, M. Singhal
in [13]. Each process P i (1  i  n) maintains an integer vector D i [1.p], called the
dependency vector. Since causal relations between two intervals at different processes
are created by communication events (and their transitive relation), values in D i are
advanced only when a communication event takes place at P i . We use D x
i to denote
the value of vector D i when process P i is in interval ' x
i . This value is computed at
the time " x
i is executed at process P i .
Each process P i executes the following protocol:
1. When process P i is in interval ' 0
all the components of vector D i are zero.
2. When P i (1  i  p) executes a send event, D i is advanced by setting D i [i] :=
1. The message carries the updated D i value.
3. When P i executes a receive event, where the message contains Dm , D i is
advanced by setting D i [k] := max(D i [k]; Dm [k]) for 1  k  p. Moreover,
the dependency vector is advanced by setting D i [i] := D
belongs to the set of p processes directly implicated in the conjunction (i.e.,
When a process P i (1  i  p) is in interval ' x
i , the following properties are
observed [15]:
1. D x
it represents the number of intervals at P i that precede interval
2. D x
represents the number of intervals at process P j that causally
precede the interval ' x
3. The set of intervals f' D x
p g is consistent.
4. None of the intervals ' y
j such that y ! D x
(i.e., intervals at P j that causally
precede ' D x
can be concurrent with ' x
. Therefore, none of them can form
a set of intervals with ' x
i that verifies \Phi.
Let D a and D b be two dependency vector clock values. We use the following
notations.
ffl D a = D b iff 8i; D a
ffl D a  D b iff 8i; D a [i]  D b [i]
INRIA
Efficient Distributed Detection of Conjunctions of Local
ffl D a ! D b iff (D a  D b
The following result holds:
3.2.2 Logs
Each process maintains a log, denoted by Log i , that is a queue
of vector clock entries. Log i is used to store the value of the dependency vector
associated with the past local intervals at P i that may be a part of a solution (i.e.,
intervals that verify L i and have not been tested globally yet). Informations about
causal relations of a stored interval with intervals at other processes will be used in
the future when the stored interval will be examined.
When P i is in a local state oe y
contained in an interval ' x
, such that oe y
it enqueues vector clock value D x
i in Log i if this value has not already been stored.
Even if there exists more than one local state in the same interval ' x
i that verifies
the value D x
i needs to be logged only once since we are interested in intervals
instead of states.
3.2.3 Cuts
In addition to the vector clock, each process P i (1  i  n) maintains an integer
vector C i [1.p], called a cut and a boolean vector B i [1.p]. Vector C i defines the first
consistent global state which could verify \Phi. In others words, all previous global
states dont satisfy \Phi. By definition, C denotes a set of p intervals that may be the
first solution. If some informations received by P i show that this set is certainly
not a solution, the cut is immediately updated to a new potential solution. At any
time, C i [j] denotes the number of interval of P j already discarded and indicate the
j of the first interval of P j not yet eliminated. If the conjunction is
satisfied during the computation, the cut C will evolve until it denotes the first
solution.
Let C x
denotes the value of C i [j] after the communication event " x
i has been
executed at P i . The value of C i remains unchanged in the interval. Each P i maintains
the values C i in such a way that none of the intervals that precede event " C i [j]
j at
can form a set of intervals that verifies \Phi. Therefore, each process P i (1  i  p)
may discard any values D i in Log i such that D i [i] ! C i [i]. Each P i (1  i  n) also
maintains the vector B i in such a way that B i [j] holds if the interval ' C i [j]
j at P j is
certain to verify its local predicate. Thus, if the system is not certain whether the
RR
14 M. Hurfin, M. Mizuno, M. Raynal, M. Singhal
interval verifies its local predicate, B i [j] is set to false. To maintain this condition,
the cut C and the B vector must be exchanged among processes. When P i sends a
message, it includes vectors C in the message.
3.3 Descriptions of the Algorithm
A formal description of the algorithm is given in Section 3.4. The algorithm consists
of the following three procedures that are executed at a process
ffl A procedure A that is executed each time local predicate L i associated to P i
ffl A procedure B that is executed when P i (1  i  n) sends a message.
ffl A procedure C that is executed when P i (1  i  n) receives a message.
In addition to vector clock D i , cut C i , boolean vector B i , and log Log i , each
process maintains a boolean variable not logged yet i . Variable
not logged yet i is true iff the vector clock value that is associated with the current
interval has not been logged in Log i . This variable helps avoid logging the same
vector clock value more than once in Log i .
A: When the local predicate L i becomes true :
Let oe y
i be the local state that satisfies the local predicate. If ' x
i is the interval that
includes state oe y
then the vector clock value D x
i , which is associated with interval
i , is logged in Log i if it has not been logged yet. To indicate that the vector clock
for this interval has already been logged in, process P i sets variable not logged yet i
to false.
Furthermore, if the current interval (denoted by ' x
or ' D x
also the oldest
interval of P i not yet discarded (denoted by ' C x
i [i] is set to true to indicate
that ' C x
sends a message:
Since it is the beginning of a new interval, a process P i (1  i  p) advances the
vector clock by setting D i resets variable not logged yet i to true.
If the log is empty, none of the intervals that precedes the new interval can form
a set of intervals that verifies \Phi. In particular, this remark holds for the last interval
that ends just when the current execution of procedure B (i.e., the sending action)
occurs. Consequently, the last interval (and also all the intervals of P i that causally
INRIA
Efficient Distributed Detection of Conjunctions of Local Predicates 15
precede this one) can be discarded by setting C i [i] to the current value of D i [i]. (At
this step of the computation, " D i [i]
i is the identity of the current send event).
Finally, sends a message along with C
receives a message from P j that contains D
Based on the definition of vector clocks, it advances D i and resets variable
not logged yet i to true. From the definition of a cut, at any process P k (1  k  p),
none of the intervals that precedes interval ' C i [k]
k or ' C j [k]
k can form a set of concurrent
intervals that verifies \Phi. Thus, C i is advanced to the componentwise maximum
of C i and C j . B i is updated so that it contains more up-to-date of the information
in B i and B j .
process P i deletes log values for intervals that precede ' C i [i]
since
these intervals do not belong to sets of concurrent intervals that verify \Phi.
After this operation, there are two possibilities:
ffl Case 1 Log i becomes empty i.e. Log i does not contain any interval that occurs
after ' C i [i]
i and before ' D i [i]
In this case, none of the intervals at P i represented
by ' y i
i such that y i ! D i [i] can form a set of concurrent intervals that verify
\Phi. The algorithm needs to consider only future intervals, denoted by ' z
i , such
that D i [i]  z.
Since none of the intervals ' y k
k such that y k ! D i [k] at other processes P k
can form a set of concurrent intervals with such future intervals ' z
C i is advanced to D i . When process P i executes the receive action, it has no
informations about intervals ' D i [k]
p). Therefore, all components of
vector B i are set to false.
contains at least one entry that was logged after the occurrence
of event " C i [i]
the oldest such logged entry be D log
. From the properties
of vector D and the definition of a cut, at any process P k , 1kp, none of the
intervals preceding ' D log
k or ' C i [k]
k can form a set of concurrent intervals with
' D log
i that verifies \Phi. Thus, C i is advanced to the componentwise maximum
of D log
. Similar to Case 1, if the value C i [k] is modified (i.e., it takes
its value from D log
not certain whether P k 's local predicate held
in the interval ' D log
k . Thus, B i [k] is set to false. If the value C i [k] remains
unchanged, the value B i [k] will also remain unchanged.
RR
M. Hurfin, M. Mizuno, M. Raynal, M. Singhal
Furthermore, since ' D log
verified its local predicate, B i [i] is set to true. At
this point, P i checks whether B i [k] is true for all k. If so, this indicates that
each interval in the concurrent set of intervals 1 f' C i [1]
verifies
its local predicate and thus, \Phi is verified.
3.4 A Formal Description of the Algorithm
Initialization procedure executed by any process P i
if (i  p) then
Create(Log i ); not yet logged i := true;
endif
Procedure A executed by process
when the local predicate L i becomes true
if (not yet logged i ) then
logged i := false;
endif
Procedure B executed by any process P i
when it sends a message
if (i  p) then
logged i := true;
endif
Append vectors D i , C i , and B i to the message;
Send the message;
Procedure C, executed by any process P i
when it receives a message from P j
We will prove in subsection 3.7 that a set of intervals numbered by C i values always are
concurrent.
INRIA
Efficient Distributed Detection of Conjunctions of Local Predicates 17
Extract vectors D j , C j and B j from the message;
if (i  p) then
logged i := true;
while ((not (Empty(Log i ))) and (Head(Log i do
/* Delete all those logged intervals that from the current
/* knowledge do not lie on a solution.
/* Construct a solution that passes through the next local interval.
else
/* Construct a solution that passes through the logged interval.
endif
endif
Deliver the message;
Function Combine Maxima ((C1,B1), (C2,B2))
B: vector [1.p] of boolean;
C: vector [1.p] of integers;
for to p do
case
endcase
3.5 A Simple Example
Since the algorithm is quite involved, we illustrate the operation of the algorithm
with the help of an example. In Figure 4, a local state contained in an interval is
RR
M. Hurfin, M. Mizuno, M. Raynal, M. Singhal
represented by a grey area if it satisfies the associated local predicate. At different
step of the computation, we indicate the values of the main variables used to detect
items with square brackets next to a process interval,
respectively, depict the contents of vectors D and C. Those values remain unchanged
during the entire interval. The value of vector B after execution of a communication
event is indicated between round brackets.
Initial value of interval number at two processes is 0 and C vector is (0 0) at
both processes. When the local predicate holds in interval ' 0
enqueues D 1 vector into Log 1 . Process P 1 also set B 1 [1] to true because it is certain
that ' C 1 [1]
sends message m1, it increments D 1 [1] to 1 and
sends vectors B 1 , C 1 , and D 1 in the message.
When receives message m1, it increments D 2 [2] to 1 and then updates its
B, C, and D vectors. P 2 finds its Log empty and constructs a potential solution
using its D vector and stores it into its C vector. When the local predicate becomes
true in state oe 1
to Log 2 . As the variable not yet logged 2 is false when
process P 2 is in local state oe 2
2 , the vector clock D is not logged twice during the same
interval. When P 2 sends message m2, it increments D 2 [2] to 2 and sends vectors B 2 ,
in the message.
When P 1 receives message m2, it increments D 1 [1] to 2 and then updates its B,
C, and D vectors. After merging with the vectors received in the message, P 1 finds
that C 1 [1] (=1)?Head(Log 1 )[1] (=0) and discards this entry from Log 1 . Since Log 1
is empty, P 1 constructs a potential solution using its D vector and stores it into its
C vector. When the local predicate becomes true in interval oe 2
to Log 1 . When P 1 sends message m3, it increments D 1 [1] to 3 and sends vectors B 1 ,
in the message.
In the meantime, local predicate holds in state oe 3
2 and consequently, P 2 logs
vector D 2 to Log 2 .
When receives message m3, it increments D 2 [2] to 3 and then updates its B,
C, and D vectors. After merging with the vectors received in the message, P 2 finds
that C 2 [2] (=2)?Head(Log 2 )[2] (=1) and discards this entry. Since the next entry
in Log 2 cannot be discarded, P 2 constructs a potential solution using Head(Log 2 )[2]
vector and stores it into its C and B vectors. The potential solution goes through
1 . The fact that this interval satisfies L 1 is known by process P 2 (B 2 [1] is
true). After P 2 sets B 2 [2] to true, it finds that all entries of vector B 2 are true and
declares the verification of the global predicate.
INRIA
Efficient Distributed Detection of Conjunctions of Local Predicates 19

Figure

4: An Example to Illustrate Algorithm 1.
3.6 Extra messages
The algorithm is able to detect if a solution exists without adding extra-message
during the computation and without defining a centralized process. The algorithm
depends on the exchange of computation message between processes to detect the
predicate. As a consequence, not only the detection may be delayed, but also in
some cases the computation may terminate and the existing solution may go unde-
tected. For example, if the first solution is the set consisting of the p last intervals,
g, the algorithm will not detect it. To solve this problem, if a
solution has not been found when the computation terminates, messages containing
vector D, C, and B are exchanged between the p processes until the first solution
is found. To guarantee the existence of at least one solution, we assume that the
set of intervals f' l 1 +1
p g is always a solution. Extra messages are
exchanged only after the computation ends and the first solution has not been detected
yet. To reduce the overhead due to these extra messages between processes,
one can use a privilege (token) owned by only one process at a time. The token
circulates around a ring consisting of the p processes, disseminating the information
about the three vectors. Another solution consists of sending the token to a process
who may know the relevant information (i.e., a process P j such that B i [j] is false).
RR
M. Hurfin, M. Mizuno, M. Raynal, M. Singhal
3.7 Correctness of the algorithm
be two vector timestamps such that the sets of intervals
represented by f' V 1 [1]
are both concur-
rent. Then, the set of intervals represented by f' V 3 [1]
p g is concurrent,
Proof: We show that a pair of intervals (' V 3 [i]
any combination of i and
concurrent. Renumbering the vectors V 1 and V 2 if
necessary, suppose V 3 There are two cases to consider:
1. This case is obvious because, from the assumption, ' V 1 [i]
are concurrent.
2. Suppose on the contrary that ' V 3 [i]
j are not concurrent.
There are two cases to consider:
In this case, "
i . This
contradicts the assumption that ' V 1 [j]
are concurrent.
By applying the same argument as the
case (a), this leads to a contradiction to the assumption that ' V 2 [i]
are concurrent.
are concurrent. 2
The following lemma guarantees that a cut C i always keeps track of a set of
concurrent intervals.
Lemma 2: At any process P i , at any given time, f' C i [1]
p g is a set of
concurrent intervals.
Proof: C i is updated only in one of the following three ways:
1. When a receive event is executed, by executing C:= D.
2. When a receive event is executed by taking maximum of C i and C j (the cut
contained in the message sent by process P j ), and then by taking maximum
of C i and D log
(The oldest value of the dependency vector still in the log).
INRIA
Efficient Distributed Detection of Conjunctions of Local Predicates 21
3. When a send event occurs, entry C i [i] is set to D i [i].
Let update(C x
the update on cut C i at communication event " x
giving
the value C x
i . We define a partial order relation (represented by ";") on all updates
on all cuts C i (1  i  p) as follows:
1. If " x
are two consecutive communication events that occur at P i (i.e.,
2. If there exists a message m such that " x
i is the sending of m to P j and " y
i is
the receiving of m from P i , then update(C x
Let SEQ be a topological sort of the partial order of update events. We prove the
lemma by induction on the number of updates in SEQ.
Induction Base: Since the set of intervals f' 0
p g is concurrent, initially the
lemma holds for any C i (i.e., after update(C 0
Induction Hypothesis: Assume that the lemma holds up to t applications of the
updates.
Induction Steps: Suppose st update occurs at process P i and let C x
the cut value after the st update operation denoted as update(C x
i is a receive event and C x
From the definition of vector clocks, for any vector clock value D, the set of
intervals f' D[1]
p g is concurrent. Thus, C x
represents a set of
concurrent intervals.
Case 2: " x
i is a receive event and C x
As " y
j is the corresponding send event, update(C y
Clearly, the
relation update(C
holds. Since from induction hypo-
thesis, both C
represent sets of concurrent intervals, max(C
represents a set of concurrent intervals (from Lemma 1). Since from the definition
of vector clocks, D log
(the oldest entry still in the log) represents a set of
concurrent intervals, C x
represents a set of concurrent intervals (from Lemma
1).
Case 3: " x
i is a send event, C x
i [i], and 8j such that j 6= i, C x
RR
22 M. Hurfin, M. Mizuno, M. Raynal, M. Singhal
Suppose no receive event occurs at process P i before the send event " x
. All the
entries of vector D x
i and vector C x
i [i], are zero. Therefore,
i and the proof is the same as in Case 1.
Suppose now that " y
i is the last receive event who occurs before the sending
event " x
in the log has been discarded since this event occurred.
As the Log is empty, we can conclude that the log was also empty when this
receive event occurred and hence, C y
. As this event is the last receive
event that occurs before " x
i , we conclude that 8j such that j 6= i, D y
and C y
. Then, the proof is the same as in case
1.The following lemma shows that if there is a solution, a cut C i will not miss and
pass beyond the solution.
Lemma 3: Consider a particular cut (identified by an integer vector S) such that
p g is a set of concurrent intervals that verifies \Phi.
i denote any communication event. If, for all communication events " y
j such
that " y
Proof: Proof is by contradiction. Suppose there exists a communication event " x
such that :(C x
and for any communication event " y
j such that " y
i is the first event that advances C i beyond S.
There are two cases to consider:
1. C x
From hypothesis, C
holds. Therefore, entry C i [j] is modified during
execution of event " x
i . This event is necessarily a receive event (" z
k is the
corresponding send event).
Note that ' C x
i denote the same interval. S[j] ! D x
holds. So from the definition of dependency vectors, ' S[j]
i . However,
either (' C x
i . This
contradicts the hypothesis that f' S[1]
p g is a set of concurrent
intervals.
INRIA
Efficient Distributed Detection of Conjunctions of Local Predicates 23
From the assumption, C
k  S. Therefore, C x
log
holds. So from the definition of dependency vec-
tors, ' S[j]
. Because of the max operation, D log
so ' S[j]
. Then the proof is the same as in Case 1.
2. C x
i is either a send or a receive event.
From the algorithm, it is clear that this case occurs only if none of the
intervals that occurred between ' C
(including this) and ' D x
verifies
This contradicts the fact that ' S[i]
verifies L i since C
k [i]); D log
i is a receive event and
" z
k is the corresponding send event. From the assumption, C
and C z
k [i]  S[i]. Assume that C
k [i]). Then C
S[i] and therefore C x
From the algorithm, it is clear that this case occurs only if none of the
intervals that occurred between ' C
(including this) and ' D log
verifies
This contradicts the fact that ' S[i]
verifies L i since C
(= D log
[i]).The following lemma proves that the algorithm keeps making progress if it has
not encountered a solution.
Lemma 4: Suppose process P i has executed the algorithm at the x th communication
event " x
is in the interval ' x
that the set f' C x
does not verify \Phi. Then, there exists " y
j such that C x
.
Proof: There are two reasons for f' C x
p g not verifying \Phi:
1. ' C x
i does not verify
RR
M. Hurfin, M. Mizuno, M. Raynal, M. Singhal
In this case, at " x
could not find an interval that verifies L i , and therefore,
set to x (i.e., the value of D x
[i]). At the next communication event
updates at least the i th entry of C i by setting C x+1
i [i] to D x+1
2. There exists at least one process P k (1  k  p) such that ' C x
k does not
verify
In this case, P k will eventually advance C k [k] to a value greater than C x
(refer to Case 1). This new value computed when event " z
occurs will propagate
to other processes. Extra messages eventually exchanged at the end of the
computation guarantee that there will eventually be a communication event
j at a process P j such that that " z
and C x
.Finally, the following theorem shows that \Phi is verified in a computation iff the
algorithm detects a solution.
Theorem: [1] If there exists an interval ' x
i on a P i such that, during this interval,
holds for all k (1  k  p), then f' C x
verifies \Phi.
Conversely, if f' C x
verifies \Phi for an event " x
on some processor
there exists a communication event " y
j such that for all k (1  k  p),
holds.
Proof:
[1] Proof is by contradiction. Suppose ' C x
k does not verify L k for some k. We show
that as long as C i [k] is not changed, B i [k] is false. There are two cases to consider:
1.
i does not verify L i
is updated to D i [i] when communication events " x
occurs. If " x
i is a receive
i [i] is set to false at the same time and remains false during the interval
necessarily empty for the entire duration of interval ' C x
modified only when event " x+1
occurs.
i is a send event, the value of B i [i] is unchanged since the last receive event
or since the beginning of the computation if no receive event occurs at process
before the send event " x
i . In both cases, Log i remains empty during this
entire period and B i [i] remains false.
INRIA
Efficient Distributed Detection of Conjunctions of Local Predicates 25
2. i 6= k:
updated C i [k] to C x
there existed a process P j that advanced
to C x
[k], and the value was propagated to P i . P j must have set B j [k]
to false and this information must have propagated to P i . This value was
propagated to P i without going through P k (else P k would have been advanced
to a value greater than C x
i [k]). It is easy to see that B x
i [k] is false: Since
k is the only process that can change B k [k] to true, P i will never see B
true together with C i
[2] Assume that f' C x
verifies \Phi. Message exchanges guarantee that
there will eventually be a communication event " y
j such that for all k, 1  k  p,
. When process P k is in interval ' C x
[k] is set to true.
From Lemma 3, once a process P h sets C h [k] to C x
does not change this
value in the future. This implies that all the processes P h that are on the path of the
message exchange from " C x
k to " y
to C x
i [k] and B h [k] to true - none
of such processes P h sets B h [k] to false by advancing C h [k] beyond C x
information is eventually propagated to P j , and so B y
holds for all k, 1  k  p.4 The Second Algorithm
In the second algorithm, every process always keeps track of a set of intervals for
all the processes such that each of the intervals verifies its local predicate. For each
such set, the process checks whether all the intervals in the set are concurrent.
4.1 Overview of the Algorithm
4.1.1 Verified Intervals
In this algorithm, only the intervals that verify their associated local predicates are
of interest. We call such intervals verified intervals. A new
i is used to
identify the x th verified interval of process P i . Thus, for
i , there exists exactly
one ' y
i that denotes the same interval.
RR
26 M. Hurfin, M. Mizuno, M. Raynal, M. Singhal
\Omega 0\Omega 1\Omega 0\Omega 1" 0
Figure

5: The corresponding set of verified intervals.
4.1.2 Dependency Vectors
As in the first algorithm, each process P i (1  i  n) maintains a dependency vector
track of the identity of the next verified interval that P i will
encounter. Even though P i does not know which interval it will be, it knows that
the next verified interval will be denoted
When has encountered the x th verified interval denoted, by
\Omega
detailed description of Log i is given later.) At
this moment, D i increments D i [i] by one to x to look for the
next verified
. Note that the existence of the verified
i , is not
guaranteed at this moment. The local predicate may not be satisfied anymore during
the computation.
In the first algorithm, vector D remains the same for the entire duration of an
interval. In the second algorithm, on the contrary, vector D may change once during
an interval if this interval is a verified interval.
In order to capture causal relation among verified intervals at different processes,
the following protocol is executed on D i by a process P i (1  i  n):
1. Initially, all the components of vector D i are zero.
2. When P i executes a send event, it sends D i along with the message.
3. When P i executes a receive event, where a message contains Dm , D i is advanced
by setting D i [k] := max(D i [k]; Dm [k]) for 1  k  p.
INRIA
Efficient Distributed Detection of Conjunctions of Local Predicates 27
Clearly, the following properties hold:
1. D i [i] represents the number of verified intervals at P i whose existence can
be confirmed by P i (i.e., P i has already passed through its (D i [i]) st verified
interval).
2. D i [j](j 6= i) represents the number of verified intervals that have occurred at
process P j and causally precede the current interval of P i .
3. The set of verified intervals
p g is not necessarily
consistent. Yet, by definition, if
exists, it satisfies the
associated local predicate.
4. None of the
j such that y ! D i [j] (i.e., verified intervals at P j that
causally
precede\Omega D i [j]
can be concurrent
. Therefore, none of them
can form a set of intervals
i that verifies \Phi.
4.1.3 Logs
Each process P i maintains a log, denoted by Log i , in the same manner as in the first
algorithm. When P i verifies its local predicate L i , it enqueues the current D i before
incrementing D i [i] by one.
When Log i is not empty, notation D log
i is used to denote the value of the vector
clock at the head of Log i . Necessarily, when the log is not empty, the existence of
\Omega D log
i has already been confirmed by P i .
4.1.4 Cuts
Like the first algorithm, each process P i maintains an integer vector C i and a boolean
vector . The meaning of C i is similar to that of the first algorithm; that
is the next possible interval at P j that may be in a solution and none of the verified
intervals that
precedes\Omega C i [j]
j can be in a solution. Therefore, each process P i may
discard any values D i in Log i such that D i
The meaning of B i is also similar to that in the Algorithm 1. Each P i maintains
in such a way that B i [j] is true if process P i is certain that verified interval
j has been confirmed by P j . Furthermore, process P i is certain that none of the
verified
causally
precede\Omega C i [j]
. Thus, if P i is not certain
RR
28 M. Hurfin, M. Mizuno, M. Raynal, M. Singhal
whether the verified
j has already been confirmed by P j , B i [j] is set to
false.
4.2 Descriptions of the Algorithm
A formal description of the algorithm is given in Section 4.3. As the first algorithm,
the second algorithm consists of three procedures that are executed at a process P i .
Again, we assume that the set of intervals f' l 1 +1
p g is a solution.
Extra messages are exchanged after the computation ends only if the first solution
has not been discovered yet.
When the local predicate L i becomes true:
Let oe y
i be a local state that satisfies the local predicate. P i has entered the verified
i that includes state oe y
i . It logs D i in Log i if D i has not been logged yet
since the beginning of this interval. In order to indicate that the vector clock for
this interval has already been logged, it sets variable not logged yet i to false. The
counter of verified interval D i [i] is incremented by one to reflect that the current
interval is a verified interval.
Furthermore, if the current verified interval is also the oldest verified interval of
discarded (denoted
[i] is set to true to confirm the existence
When P i sends a message:
Since it marks the beginning of a new interval, P i resets variable not logged yet i to
true and then it sends the message along with C
When receives a message from P j that contains D
Since a new interval begins, it resets variable not logged yet i to true. As in the
first algorithm, none of the intervals at any process P k that
precede\Omega C i [k]
can form a set of concurrent intervals that verifies \Phi. Thus, C i is advanced to the
componentwise maximum of C i and C j .
At this moment, B i is also updated. "B i [k] is true" means that P i is certain that
the existence
k has been confirmed. Thus, if C i [k] and at least one
of B i [k] and B j [k] is true, B i [k] is set to true.
deletes all entries from Log i that
precede\Omega C i [i]
i since all those verified
intervals are no more potential components of a solution.
After this operation, there are two cases to consider:
INRIA
Efficient Distributed Detection of Conjunctions of Local Predicates 29
ffl Case 1 Log i becomes empty: In this case, none of the verified intervals at P i
up to this moment forms a set of concurrent verified intervals.
The algorithm needs to consider only verified intervals that will occur in the
future. If such intervals
exist,\Omega D i [i]
i will be the first one. Since all of the verified
k such that y ! D i [k] at other processes P k causally
precede\Omega D i [i]
none of such intervals can be in a solution. Thus, cut C i is advanced to D i .
When process P i executes the receive action, it is not certain whether P k (1
p) has encountered the verified
k . Therefore, all components
of vector B i are set to false.
contains at least one logged interval: Let the oldest of such logged
entry be D log
. From the properties of vector D and the definition of a cut, all
of the verified intervals at any process P k
preceding\Omega C i [k]
or\Omega D log
causally
precede\Omega D log
none of such intervals can be in a solution. Thus, C i is
advanced to the componentwise maximum of D log
Similar to Case 1, if the value C i [k] is modified (i.e., it takes its value from
log
not certain whether P k 's will encounter the verified interval
' D log
k . Thus, B i [k] is set to false. If C i [k] remains unchanged, B i [k] also
remains unchanged to follow other processes' decision.
Furthermore, B i [i] is set to true since P i has confirmed the existence
of\Omega D log
At this moment, with the new information (C may be able
to detect a solution. Thus, P i checks whether B i [k] is true for all k. If so, this
indicates that all the verified intervals in set
have
been confirmed and concurrent with one another since no process has detected
causal relations between any pair of intervals in the set.
4.3 Formal Description of the Algorithm
Initialization procedure executed by any process P i
if (i  p) then
Create(Log i ); not yet logged i := true;
endif
RR
M. Hurfin, M. Mizuno, M. Raynal, M. Singhal
Procedure A executed by process
when the local predicate L i becomes true
if (not yet logged i ) then
logged i := false;
endif
Procedure B executed by any process P i
when it sends a message
if (i  p) then not yet logged i := true; endif
Append vectors D i , C i , and B i to the message;
Send the message;
Procedure C executed by any process P i
when it receives a message from P j
Extract vectors D j , C j , and B j from the message;
if (i  p) then
not yet logged i := true;
while ((not (Empty(Log i ))) and (Head(Log i do
/* Delete all those logged intervals that from the current
/* knowledge do not lie on a solution.
/* Construct a solution that passes through the next local verified interval.
else
/* Construct a solution that passes through the logged verified interval.
endif
endif
Deliver the message;
INRIA
Efficient Distributed Detection of Conjunctions of Local Predicates 31
4.4 Discussion
4.4.1 An Example
To help the readers understand the algorithm, in Figure 5, we illustrate the operation
of the second algorithm for a computation similar to that one used in Figure 4. In

Figure

5, the contents of vector D and C that are indicated next to a process interval
in square brackets, are the values of the vectors just after evaluation of the last local
state of the interval (i.e., just before execution of the communication event).
F
FA@
FA@
F
FA@
FA@
FA@
F
FA@
F
FA@
F
TA@
TA@

Figure

An Example to Illustrate Algorithm 2.
4.4.2 Difference Between Both Approaches
The second algorithm can be considered an optimization of the first one. Interval
counters D and C evolve more slowly in the second algorithm and updates of both
vectors occur less often. For example, vector C is not modified on a send action.
Each algorithm finds the first solution in a different way. In the first algorithm, each
interval of the solution is located via a number of communication events that occur
before the process encounters this interval. In the second algorithm, the delivered
information is the number of validated interval that precede the solution.
The difference between both algorithms is much more on the semantics and the
properties of the control variables rather than on the way they are updated. For
example, update of vector C is made in a similar way in both algorithms. Yet, each
RR
M. Hurfin, M. Mizuno, M. Raynal, M. Singhal
component is managed as a counter of interval (in the first algorithm) or as a counter
of verified interval (in the second algorithm). Both algorithms employ complementary
approaches to find the first solution. In the first algorithm, the corresponding
set of interval is always concurrent (i.e., it satisfies the first criterion of the solution).
In the second algorithm, the elements of the set are always verified intervals (i.e.,
the set satisfies the second criterion of the solution).
A correctness proof of the second algorithm is similar to the proof of the first
algorithm. However, Lemma 1 and Lemma 2 become irrelevant in the second algo-
rithm. Instead, the following lemma becomes useful:
Lemma 5: At any time during execution of P i , if B i [j] (1  j  p) is true then
Proof: Process P j has necessarily updated B j [j] to true to account for the fact that
j has been encountered and is the oldest interval not discarded yet. At
the same time, P j used the value at the head of the Log, D log
j , to update all the
other components C j [k] to a value greater or equal to D log
[k] in order to invalidate
all the verified intervals that are in the causal past
. Therefore, as the cut C
never decreases (due to the merge operation made at the beginning of each receive
share with P j the same vision of the values of B[j] and C[j] and
at the same time keep an older value for some component C i [k]. 2
The rest of the proof is the same as that of the first algorithm with the definition
of interval appropriately modified.
5 A Comparison with Existing Work
Previous work in detecting conjunctive form global predicates has been mainly by
Garg and Waldecker [6] and Garg and Chase [7]. Garg-Waldecker algorithm is centralized
[6], where each process reports all its local states satisfying its local predicate
to a checker process. The checker process gathers this information, builds only those
global states that satisfy the global predicate, and checks if a constructed global
state is consistent. This algorithm has a message, storage, and computation complexities
of O(Mp 2 ) where M is the number of messages sent by any process and p
is the number of processes over which the global predicate is defined.
INRIA
Efficient Distributed Detection of Conjunctions of Local Predicates 33
In [7], Garg and Chase present two distributed algorithms for detection of conjunctive
form predicates. In these algorithm, all processes participate in the global predicate
detection on equal basis. The first distributed algorithm requires vector clocks
and employs a token that carries information about the latest global consistent cut
such that the local predicates hold at all the respective local states. The message,
storage, and computation complexities of this algorithm is the same as of Garg-
Waldecker [6] algorithm, namely, O(Mp 2 ). However, the worst case message, sto-
rage, and computation complexities for a process in this algorithm is O(Mp); thus,
the distribution of work is more equitable than in the centralized algorithm. The
second distributed algorithm does not use vector clocks and uses direct dependencies
instead. The message, storage, and computation complexities of this algorithm
are O(Mn) and the worst case message, storage, and computation complexities for
a process in this algorithm are O(M ); thus, this algorithm is desirable when p 2 is
greater than n.
The proposed predicate detection algorithm does not cause transfer of any additional
messages (except in the end provided the predicate is not detected when the
computation terminates). The control information needed for predicate detection is
piggybacked on computation messages. On the contrary, the distributed algorithms
of Garg and Chase may require exchange of as many as Mp and Mn control mes-
sages, respectively. Although the worst case volume of control information exchanged
is identical, namely, O(Mp 2 ), in the first Garg and Chase algorithm and in the proposed
algorithm, the latter results in no or few additional message exchanges. A
study by Lazowska et al. [11] showed that message send and receive overhead can
be considerable (due to context switching and execution of multiple communication
protocol layers) and it is desirable to send few bigger from performance point of
view.
6 Concluding Remarks
Global predicate detection is a fundamental problem in the design, coding, testing
and debugging, and implementation of distributed programs. In addition, it finds applications
in many other domains in distributed systems such as deadlock detection
and termination detection.
This paper presented two efficient distributed algorithms to detect conjunctive
form global predicates in distributed systems. The algorithms detect the first consistent
global state that satisfies the predicate and work even if the predicate is uns-
RR
34 M. Hurfin, M. Mizuno, M. Raynal, M. Singhal
table. The algorithms are based on complementary approaches and the second algorithm
can be considered an optimization of the first one, where the vectors D and C
increase at a lower rate. We proved the correctness of the algorithms. The algorithms
are distributed because the predicate detection efforts as well as the necessary information
are equally distributed among the processes. Unlike previous algorithms to
detect conjunctive form global predicates, the algorithms do not require transfer of
any additional messages during the normal computation; instead, they piggyback the
control information on computation messages. Additional messages are exchanged
only if the predicate remains undetected when the computation terminates.



--R



Consistent Detection of Global Predicates.

Detection of Unstable Predicates in Distributed Pro- grams
Detection of Weak Unstable Predicates in Distributed Programs.
Distributed Algorithms for Detecting Conjunctive Predi- cates
Global Events and Global Breakpoints in Distributed Sys- tems
Detecting Atomic Sequences of Predicates in Distributed Computations.
Linear Space Algorithm for On-line Detection of Global States
File Access Performance of Diskless Workstations
Global conditions in debugging distributed programs.
Virtual Time and Global States of Distributed Systems.
Breakpoints and Halting in Distributed Programs.
A Way to Capture Causality in Distributed Systems.
Faster Possibility Detection by Combining Two Ap- proaches
"le de Nancy-Brabois, Campus scientifique, 615 rue du Jardin Botanique, BP 101, 54600 VILLERS LE  S NANCY Unite de recherche INRIA Rennes, Irisa, Campus universitaire de Beaulieu, 35042 RENNES Cedex Unite de recherche INRIA Rho"
--TR

--CTR
Punit Chandra , Ajay D. Kshemkalyani, Distributed algorithm to detect strong conjunctive predicates, Information Processing Letters, v.87 n.5, p.243-249, 15 September
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
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
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
Emmanuelle Anceaume , Jean-Michel Hlary , Michel Raynal, Tracking immediate predecessors in distributed computations, Proceedings of the fourteenth annual ACM symposium on Parallel algorithms and architectures, August 10-13, 2002, Winnipeg, Manitoba, Canada
Neeraj Mittal , Vijay K. Garg, Techniques and applications of computation slicing, Distributed Computing, v.17 n.3, p.251-277, March 2005
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
on-the-fly global predicate detection;distributed systems