Global state

Global state in distributed systems is the combined state of all nodes in the system at a specific point in time.

Snapshot problem: Making a snapshot of a consistent global state without stopping the system.

Concepts #

  • System $P$ consisting of $N$ processes: $p_1, p_2, \ldots, p_N$

  • History of process $p_i$: $$ h_i = \langle e_i^0, e_i^1, e_i^2, \ldots \rangle $$

  • History prefix: $$ h_i^k = \langle e_i^0, e_i^1, e_i^2, \ldots, e_i^k \rangle $$

  • Global history (union of all processes histories): $$ H = h_1 \cup h_2 \cup \ldots \cup h_N $$

  • Cut (union of prefixes of process histories): $$ C = h_1^{C_1} \cup h_2^{C_2} \cup \ldots \cup h_N^{C_N} $$

  • Cosistent cut (for every event $e$ in the cut, it contains the events that happend-before ($\rightarrow$) it): $$ \forall e \in C : f \rightarrow e \Rightarrow f \in C $$ A consistent cut corresponds to a consistent global state. When a cut is non consistent it is called an inconsistent cut.

  • Run: total ordering of all the events in a global history that is consistent with each local history’s ordering

  • Linearization: ordering of the events in a global history that is consistent with the happened-before ($\rightarrow$) relationship

  • Global state $S'$ is reachable from global state $S$ if there is a linearization that passes through $S$ and $S'$

Chandy-Lamport snapshot algorithm #

Assumptions:

  • FIFO unidirectional communication
  • Strongly connected graph
  • No process and channel failures
if process has not recorded its state:
- record own state
- mark incoming channel as empty
- record all incoming messages from all *other* incoming channels
- send marker over each outgoing channel (before sending any other messages!)
else:
- stop recording on incoming channel

The observed state $S_{snap}$ does not necessarily occur in execution but is reachable from $S_{init}$ (when recording begins) and $S_{final}$ (when recording ends).

Distributed Debugging #

Stable predicates: if a predicate is true in some state $S$ $\Rightarrow$ is it also true in any state reachable from $S$

Non-stable predicates: can become false again in reachable states

Predicate is true in $S_{snap}$ $\Rightarrow$ predicate is also true in $S_{final}$ (hence snapshot algorithm only works for evaluating stable predicates!)

Global state predicate $\phi$

Possibly $\phi$: there is a consistent global state $S$ with a linearization of $H$ and $\phi(S) = True$

Definitely $\phi$: for all linearizations there is a consistent global state $S$, $\phi(S) = True$