Efficient Detection of Global Properties in Distributed Systems
Using Partial-Order Methods
Scott D. Stoller, Leena Unnikrishnan, and Yanhong A. Liu
A new approach is presented for detecting whether a particular
computation of an asynchronous distributed system satisfies $\Poss\Phi$
(read ``possibly $\Phi$''), meaning the system could have passed through
a global state satisfying predicate $\Phi$, or $\Def\Phi$ (read
``definitely $\Phi$''), meaning the system definitely passed through a
global state satisfying $\Phi$. 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. The resulting detection algorithms handle
larger classes of predicates and thus are more general than two
special-purpose detection algorithms by Garg and Waldecker, which detect
$\Poss\Phi$ and $\Def\Phi$ efficiently for a restricted but important
class of predicates. Furthermore, our algorithm for $\Poss\Phi$
achieves the same worst-case asymptotic time complexity as Garg and
Waldecker's special-purpose algorithm for $\Poss\Phi$. We apply our
algorithm for $\Poss\Phi$ to two examples, achieving a speedup of over
700 in one example and over 70 in the other, compared to unoptimized
state-space search.
BiBTeX
PDF
Scott Stoller's Home Page