Using synchronized atoms to check distributed programs

The execution of a distributed program generates a large state space which needs to be checked in testing and debugging. Atoms are useful abstractions in reducing the state lattice of a distributed computation; we refer to the reduced lattice as the atomic state lattice. However, general predicates remain difficult to check if they are asserted over all states. This paper presents a formulation to attack this problem involving separation of two different concerns: (a) order/synchronization requirement, and (b) computational dependency among atoms. Order requirement is modeled by the serialization of the global states reached by a synchronized set of atoms. Synchrony among atoms is specified by a synchronization predicate. Computational dependency among synchronized states is modeled by a general predicate. With this modeling assumption, the number of the states where a general predicate needs to be checked will be bounded by the number of atoms executed. Two efficient algorithms for checking a general predicate, in the cases where the synchronization predicate is conjunctive or disjunctive, are presented along with their proof of correctness.