Cutoff Theorems for the Model Checking of Crash-Tolerant Causal Broadcast

This paper proposes a method for the proof of correctness of a distributed algorithm for crash-tolerant Causal Broadcast (CB), which is a fundamental building block of numerous distributed applications (e.g., key-value storage). Since the CB algorithm can be instantiated for an unbounded number of processes, proving its correctness regardless of the number of processes is a significant problem. Moreover, moving beyond manual proofs will provide higher correctness assurances. To this end, we identify cutoff values for the model checking of five important properties of CB, namely validity, integrity, causal delivery, termination and strong termination. A cutoff value \(\varvec{C>0}\) $\mathit{C}\mathbf{>}\mathbf{0}$ enables us to show that, an instance of CB with \(\varvec{C}\) $\mathit{C}$ processes is correct for some property \(\varvec{P}\) $\mathit{P}$ if and only if any instance of CB with any number of processes greater than or equal to \(\varvec{C}\) $\mathit{C}$ is correct for \(\varvec{P}\) $\mathit{P}$ . We show that the cutoff for validity, integrity, termination and strong termination is three, and the cutoff for causal delivery is four, where there is at most one faulty process. To provide higher assurances in the correctness of CB, we utilize model checking to verify the CB properties in instances of CB with three and four processes, called the cutoff models. To enable such verification, we specify the properties of CB in Linear Temporal Logic, and develop a Promela specification of the cutoff models for verification in the Spin model checker. To the best of our knowledge, this is the first work that presents cutoffs for the CB algorithm.