It is often desirable to determine whether a particular property is true of a distributed system as it executes. We’d like to use logical time to construct a global view of the system state and determine whether a particular property is true. A few examples are as follows:

• Distributed garbage collection: Are there references to an object anywhere in the system? References may exist at the local process, at another process, or in the communication channel.
• Distributed deadlock detection: Is there a cycle in the graph of the “waits for” relationship between processes?
• Distributed termination detection: Has a distributed algorithm terminated?
• Distributed debugging: Example: given two processes p₁ and p₂ with variables x₁ and x₂ respectively, can we determine whether the condition |x₁-x₂| > δ is ever true.

In general, this problem is referred to as Global Predicate Evaluation. “A global state predicate is a function that maps from the set of global state of processes in the system ρ to {True, False}.”

• Safety – a predicate always evaluates to false. A given undesirable property (e.g., deadlock) never occurs.
• Liveness – a predicate eventually evaluates to true. A given desirable property (e.g., termination) eventually occurs.

Cuts

Because physical time cannot be perfectly synchronized in a distributed system it is not possible to gather the global state of the system at a particular time. Cuts provide the ability to “assemble a meaningful global state from local states recorded at different times”.

Definitions:

• ρ is a system of N processes p_i (i = 1, 2, …, N)
• history(p_i) = h_i = < e i 0 , e i 1 ,…>
• h i k =< e i 0 , e i 1 ,…, e i k > – a finite prefix of the process’s history
• s i k is the state of the process p_i immediately before the kth event occurs
• All processes record sending and receiving of messages. If a process p_i records the sending of message m to process p_j and p_j has not recorded receipt of the message, then m is part of the state of the channel between p_i and p_j.
• A global history of ρ is the union of the individual process histories: H = h₀ ∪ h₁ ∪ h₂ ∪…∪h_N-1
• A global state can be formed by taking the set of states of the individual processes: S = (s₁, s₂, …, s_N)
• A cut of the system’s execution is a subset of its global history that is a union of prefixes of process histories (see figure below).
• The frontier of the cut is the last state in each process.
• A cut is consistent if, for all events e and e’:
  • ( e ∈ C and e ‘ → e ) ⇒ e ‘ ∈ C
• A consistent global state is one that corresponds to a consistent cut.

Distributed Debugging

To further examine how you might produce consistent cuts, we’ll use the distributed debugging example. Recall that we have several processes, each with a variable x_i. “The safety condition required in this example is |x_i-x_j| <= δ (i, j = 1, 2, …, N).”

The algorithm we’ll discuss is a centralized algorithm that determines post hoc whether the safety condition was ever violated. The processes in the system, p₁, p₂, …, p_N, send their states to a passive monitoring process, p₀. p₀ is not part of the system. Based on the states collected, p₀ can evaluate the safety condition.

Collecting the state: The processes send their initial state to a monitoring process and send updates whenever relevant state changes, in this case the variable x_i. In addition, the processes need only send the value of x_i and a vector timestamp. The monitoring process maintains a an ordered queue (by the vector timestamps) for each process where it stores the state messages. It can then create consistent global states which it uses to evaluate the safety condition.

Let S = (s₁, s₂, …, S_N) be a global state drawn from the state messages that the monitor process has received. Let V(s_i) be the vector timestamp of the state s_i received from p_i. Then it can be shown that S is a consistent global state if and only if:

V(s_i)[i] >= V(s_j)[i] for i, j = 1, 2, …, N