Exercise 6: Chandy-Lamport Snapshot Protocol builds a consistent global state.

[dag7dev]

Exercise 6: Show that the Chandy-Lamport Snapshot Protocol builds a consistent global state.

[susannacifani]

I'm not sure about this one.

We know that the Chandy-Lamport protocol makes use of FIFO channels, so let’s assume the channels are FIFO.
If we take a cut $S'$, that is made from a snapshot and an event, and that it's not consistent, we have $e \rightarrow e' \land e' \in S' \Rightarrow e \notin S'$.
We have a snapshot $s1$ taken before $e$ because $e \notin S'$ and we have a snapshot $s2$ after $e'$ because $e' \in S'$.
$s1$ will trigger a take snapshot message that will arrive after $s2$ (and $e'$) and this is impossible because our channels are FIFO.
So we can say that a global state is consistent if $e \rightarrow e' \land e' \in S \Rightarrow e \in S$ and that the Chandy-Lamport algorithm builds a consistent global state.

[rotiroti]

Let $e$ and $e'$ two events. We aim to prove that if $e'$ is part of the snapshot $S$ and $e \to e'$, then $e$ should also be in $S$.
Let's demonstrate it by contradiction.

• Assume the contrary: $e' \in S \land e \notin S$.
• This contradiction is immediately evident if $e$ and $e'$ are on the same process because a process's state is captured atomically.
• If $e$ is a send event and $e'$ is a corresponding receive event on another process, then the marker message causing $e'$ to be in the snapshot $S$ must have been after $e$ since the Chandy-Lamport Snapshot Protocol assumes that channels are FIFO. Thus, it means the process of event $e$ must have recorded its state (including $e$) before sending the marker. Therefore, $e$ should be in S, which contradicts our assumption.

We conclude from the contradiction that if $e'$ is in the snapshot $S$ and $e \to e'$, then $e$ must also be in $S$.

[Tommaso-Sgroi]

Assume communication's channels are FIFO and network reliable.
We list 3 properties of the snapshot protocol that can show the build of a consistent global state:

1. A process $P_i$ before sending the "take-snapshot" message must deliver its outgoing message, if there is one (FIFO assumption).
2. After receiving the first "take-snapshot" from process $P_j$ message, a process $P_i$ starts recording incoming messages from all channels excluding $P_j$'s one.
3. After receiving another "take-snapshot" message (we have received a "take-snapshot" message yet) from process $P_k$, we stop recording incoming messages from channel $P_k$ and we can add those to the local history.
4. If we receive $n-1$ "take-snapshot" messages we can send our local history.

Being $S$ the global state as the merge of processes local histories got from (4), for each event we have $e \rightarrow e' \in S$. $e \in S$ is ensured by (1) and $e' \rightarrow S$ is ensured by (2) and (3).