Local detection of exclusive global predicates

Detecting global predicates in distributed program executions is a useful tool for debugging and testing. A new form of global predicates, called exclusive global predicates, is considered in this paper to provide a natural and efficient way to describe mutual exclusion conditions. One exclusive global predicate is enough to express mutual exclusion condition for n local predicates, one for each process; the O(n²) conjunctive global predicates are required to describe the same condition. In this paper, a local on-line detection algorithm of exclusive global predicates is presented with formal proof. This algorithm detects a violation of mutual exclusion during the execution at each local process. This algorithm uses timestamps to get dependence relations between events. The n+2 numbers are piggybacked to each message, and no extra communication overhead for control information is required. This allows the proposed model to be useful and efficient for testing and debugging of distributed programs compared to the previous method with conjunctive global predicates