This page is under construction.

Predicate Detection

Global predicate detection is a fundamental problem in distributed computing with applications in distributed debugging and monitoring of distributed programs. The predicate detection problem can be defined as follows. You are given a distributed computation modeled as a set of events E and the happened before relation ->. A subset of events G is a consistent global state of the computation if for any event f that is included in G such that another event e -> f, then e is also included in G.

Predicates based on a single consistent global state

Someone specifies a global predicate B and our job is to find if there exists a consistent global state G such that B holds in G.

Well, as one can expect, the problem is NP-complete even when processes do not communicate with each other. One can define subclasses of predicates such as stable predicates, linear predicates, and observer-independent predicates for efficient detection under special cases. These results are shown in

C. M. Chase, V. K. Garg,Efficient Detection of Global Predicates in a Distributed System, Distributed Computing, Vol. 11, No. 4, 1998, pp. 169 -- 189.Postscript

Now assume that the global predicate B is given in a disjunctive normal form boolean expression of local predicates. It is sufficient to detect conjunction of local predicates to detect B. The first algorithm to detect conjunctive predicates is given in

V. K. Garg, B. Waldecker,Detection of Weak Unstable Predicates in Distributed Programs, IEEE Transactions on Parallel and Distributed Systems, Vol. 5, No. 3, March 1994, pp. 299-307. Abstract ........... Postscript

Examples of predicates that can be detected efficiently includes (P1 is red) and (P2 is red),
(P1 is at line 65) and (variable x in P2 is negative).

A distributed algorithm appears as

V. K. Garg, C. Chase, Distributed Detection of Conjunctive Predicates,Proc. IEEE International Conference on Distributed Computing Systems, Vancouver,Canada, June 1995, pp. 423 - 430.Abstract ...........Postscript

In many cases, the predicate may refer to the state of the channels. For example, termination can be modeled as "all processes are passive" and "all channels are empty." Algorithms to detect channel predicates is given in

  • V. K. Garg, C. Chase, J. R. Mitchell, R. Kilgore, Efficient Detection of Channel Predicates in a Distributed System, Journal of Parallel and Distributed Computing , Vol. 45, No. 2,September 1997, pp. 134 -- 147.pdf

    • The paper uses a restriction on predicates called linearity. A global predicate B is linear if whenever the predicate evaluates false on a global state G, there exists an event e such that unless that event is executed the predicate can never become true. The predicate satisfies Efficient Advancement Property if the event e can be determined in polynomial time. Any linear predicate with efficient advancement property can be detected efficiently.

    The definition of linearity turns out to be equivalent to meet-closure. A global predicate B is meet-closed if the following holds:
    for all consistent global states G,H: B(G) and B(H) imply that B(G meet H).

    The meet-closure implies that there exists a "least" global state that satisfies B whenever B is true in a computation.

    What is the predicate is not linear? A class of predicates, called relational predicates, or bounded sum predicates is explored in

    A. I. Tomlinson, V. K. Garg,Monitoring Functions on Global States of Distributed Programs Journal of Parallel and Distributed Computing Vol. 41, No. 2, March 1997, pp. 173 -- 189.Abstract ...........Postscript

    This paper allows detection of predicates of the form x1+x2+...+xn >= k.

    Predicates Based on Control Flow

    Assume that you want to detect a pattern in a distributed computation. One example would be to detect a regular expression of events. This is the subject of

    E. Fromentin, M. Raynal, V. K. Garg, A. I. Tomlinson, On the fly testing of Regular Patterns in distributed computations, Proc. 23rd International Conference on ParallelProcessing, St. Charles, Illinois, August 1994, pp. 2:73-76.Abstract ...........Postscript

    Another approach is based on a recursive poset logic described in

    A. I. Tomlinson, V. K. Garg, Observation of Software for Distributed Systems with RCL,Proc. 15th Conference on the Foundations of SoftwareTechnology & Theoretical Computer Science, Bangalore, India, Lecture Notes in Computer Science1026, Springer-Verlag, Dec. 1995, pp. 195 - 209.Abstract ...........Postscript

    Temporal Logic Predicates

    Since many properties in distributed systems are specified in temporal logic, it is also natural to detect violation of these temporal logic predicates. Algorithms for unnested temporal logic formulas are presented in
  • Alper Sen and Vijay K. Garg,Detecting Temporal Logic Predicates in the Happened Before Model,International Parallel and Distributed Processing Symposium (IPDPS).April, Florida.Abstract ...........Postscript ...........
    • These are generalized to nested temporal logic predicates in
  • Alper Sen and Vijay K. Garg, Detecting Temporal Logic Predicates in Distributed Programs Using Computation Slicing, 7th International Conference on Principles of Distributed Systems La Martinique, France,December 10-13 2003, ........... Postscript ........... pdf

    • The paper uses computation slicing to represent the set of global states satisfying subformulas. The temporal logic used is a subset of CTL. One of the open problems is to deal with the AF: operator efficiently, i.e., to compute the slice for AF:B when B is regular. Some partial solutions are presented in
  • Alper Sen and Vijay K. Garg, On Checking Whether a Predicate Definitely Holds, 3rd International Workshop onFormal Approaches to Testing of Software(FATES 2003) Montreal, Quebec, Canada,October 2003............Postscript

  • V. K. Garg, B. Waldecker,``Detection of Strong Unstable Predicates in Distributed Programs,'' IEEE Transactions on Parallel and Distributed Systems, Vol. 7, No. 12, December 1996, pp. 1323 - 1333. Abstract ...........Postscript

    • Some survey/invited papers on the topic are available here