验证 $\delta$-CRDT 中的强最终一致性

无冲突复制数据类型（CRDTs）是一种自然的结构，用于在可能无法容忍协调开销且允许个体参与者暂时偏离整体计算的分布式环境中传递有关共享计算的信息。在此设定下，存在两种经典方法：基于状态与基于操作的 CRDTs。前者定义可交换、结合且幂等的连接操作，其状态为单调连接半格。基于状态的 CRDTs 可进一步区分为经典状态 CRDTs 与 $\delta$-状态 CRDTs。前者在每次更新后传达其完整状态，而后者仅传达变化的状态。基于操作的 CRDTs 传达操作（而非状态），从而使其更新非幂等。尽管基于操作的 CRDTs 所需交换的信息很少，但其要求相对强的网络保证（恰好一次消息投递），而基于状态的 CRDTs 则面临相反的问题。二者均满足强最终一致性（SEC）。我们假定 $\delta$-状态 CRDTs 既（1）因载荷大小而需要更少的通信开销，又（2）容忍相对弱的网络环境，使其成为 CRDTs 实际应用的理想候选。我们的核心直觉是状态、$\delta$-状态与基于操作的 CRDTs 之间的一对归约。我们在 Isabelle 交互式定理证明器中形式化了该直觉，并证明基于状态的 CRDTs 实现了 SEC。我们在 Isabelle 中给出了一个宽松的网络模型，并证明基于状态的 CRDTs 仍保持 SEC。最后，我们扩展了工作，证明即使在相对弱的网络条件下，仅传达 $\delta$-状态片段时 $\delta$-状态 CRDTs 仍保持 SEC。