| This dissertation examines the problem of unstable predicate detection in distributed programs, which is an important aspect of debugging distributed programs. We address this problem for a loosely-coupled message-passing environment. The significance of this research lies in the fact that detection methods are given for distributed predicates that may be unstable in nature. A distributed predicate is one that depends on state information in different processes. A stable predicate is one which, once it becomes true, stays true forever. Stable predicates can be detected by checking periodically to see if they have become true, however this is not the case with unstable predicates. The predicates in this research are both distributed and unstable and, in the past, such predicates have often been regarded as too difficult to detect.;Previous work on distributed program debugging is reviewed and we show that none of the existing approaches satisfies our requirements for unstable predicate detection. These requirements are a taxonomy for unstable distributed predicates, accurate detection methods, and feasible detection costs.;We present a structured method of constructing predicates for a distributed program and identify what constructs can be detected. This is presented in the form of a predicate logic or grammar which gives the specific rewrite rules to be used in constructing various types of distributed predicates. A restricted version of this logic is then given which characterizes those types of distributed predicates that can be feasibly detected. Detection algorithms are given for those predicates in the restricted logic along with correctness proofs. Any predicate belonging to this restricted logic can be detected directly using the algorithms we provide. Further, any predicate which can be reduced to a set of predicates from this restricted logic is detectable.;Finally, we give examples including mutual exclusion, leadership election, and database applications to illustrate the usefulness of such predicates. The algorithms presented have been implemented in C under Berkeley UNIX to further validate their correctness and practicality. |
