Читать книгу From Traditional Fault Tolerance to Blockchain - Wenbing Zhao - Страница 49
2.2.2.2 Correctness of the Protocol.
ОглавлениеIt is easy to see why the protocol always produce a set of checkpoints that can be used to reconstruct a consistent global state in the absence of failures. As shown in Figure 2.2(a) and (b), a consistent global state consists of only two scenarios with respect to each pair of local states:
1 All messages sent by one process prior to its taking a local checkpoint have been received and executed before the other process takes its local checkpoint.
2 Some messages sent by one process prior to its taking a local checkpoint might arrive after the other process has checkpointed its state, however, these messages are logged at stable storage for replay.
In the Tamir and Sequin protocol, if neither the coordinator nor any of the participants receives any regular message once the global checkpointing is initiated, then the scenario 1 holds. On the other hand, if a process receives one or more regular messages, it logs them and append them to the local checkpoint, ensuring their replayability. Hence, the scenario 2 holds. Because the protocol prohibits any process from continuing normal execution (including the sending of a message) as soon as it initiates (if it is the coordinator) or receives the very first CHECKPOINT message (for a participant), no process would receive a message prior to its checkpointing that has been sent by another process after that process has taken its local checkpoint in the same round. That is, the inconsistent global state scenario shown in Figure 2.2(a) does not occur.