Efficient detection of global properties in distributed systems using partial-order methods

A new approach is presented for detecting whether a particular computation of an asynchronous distributed system satisfies Poss ɸ (read “possibly ɸ”), meaning the system could have passed through a global state satisfying predicate ɸ, or Def ɸ (read “definitely ɸ”), meaning the system definitely passed through a global state satisfying ɸ. Detection can be done easily by straightforward state-space search; this is essentially what Cooper and Marzullo proposed. We show that the persistent-set technique, a well-known partial-order method for optimizing state-space search, provides efficient detection. This approach achieves the same worst-case asymptotic time complexity as two special- purpose detection algorithms of Garg and Waldecker that detect Poss ɸ and Def ɸ for a restricted but important class of predicates. For Poss ɸ, our approach applies to arbitrary predicates and thus is more general than Garg and Waldecker’s algorithm. We apply our algorithm for Poss ɸ to two examples, achieving a speedup of over 700 in one example and over 70 in the other, compared to unoptimized state-space search.