Chapter 20. The Predicate Detection Problem

Detecting global predicates on distributed computations using vector clocks and consistent cuts.

Predicate detection on distributed systems

Given a distributed computation represented by vector clocks, the predicate detection problem asks whether there exists a consistent cut satisfying a given global predicate. For conjunctive predicates (conjunctions of local conditions), efficient algorithms exist that exploit the lattice structure of consistent cuts.

Conjunctive Predicate Detection

The conjunctive algorithm maintains a global cut $G$ where each $G[j]$ is an index into the local trace of process $j$. The forbidden condition detects when $G[j] \to G[i]$ (happened-before), meaning process $j$'s state is in the causal past of process $i$'s state. Advancing increments $G[j]$ to the next local state. At termination, either a consistent cut satisfying the conjunctive predicate is found, or one process reaches the end of its trace.

Time complexity: $O(n^2 m)$, where $n$ is the number of processes and $m$ is the number of events per process.

int[] ConjunctiveAlgorithm(int[][] vc, int[] T) {
  int n = vc.length;
  int[] G = new int[n];
  forall k in [0..n-1] : G[k] = 1;
  forbidden (j) : happenedBefore(j, G, vc) =>
    advance : {
      if (G[j] >= T[j]) { return G; }
      else { G[j] = G[j] + 1; }
    };
  return G;
}

LLP predicates for this chapter

Each LLP program in this chapter defines a state vector $G$ and a forbidden predicate; the algorithm runs until no $j$ is forbidden. The table below lists, for each algorithm, what $G[j]$ represents and the negation of the forbidden clause from the matching .llp source.