基于保持交互抽象的 TLA+ 共识协议组合模型检测
分布式、并行与集群计算
2022-02-24 v1 形式语言与自动机理论
摘要
共识协议广泛用于构建可靠的分布式软件系统,其正确性至关重要。TLA+ 是一种轻量级形式化规约语言,能够精确描述系统设计并无须人工干预地穷尽检查设计。TLA+ 的特性使其在学术界与工业界的共识协议规约与模型检测中被广泛使用。然而,TLA+ 的应用受限于模型检测中的状态爆炸问题。尽管组合模型检测对抑制状态爆炸问题至关重要,现有组合检测技术并未充分考虑 TLA+ 的特性。本工作中,我们提出保持交互抽象(IPA)框架,其利用 TLA+ 的特性,实现对 TLA+ 规约的共识协议实用且高效的组合模型检测。在 IPA 框架中,系统规约被划分为多个模块,每个模块分为内部部分与交互部分。保持交互抽象的基本思想是省略各模块的内部部分,使得另一模块无法区分其是在与原模块交互还是与粗化后的抽象模块交互。我们将 IPA 框架用于 Raft 与 ParallelRaft 两个共识协议的 TLA+ 规约的组合检测。Raft 是最初在学术界提出、后被工业界广泛使用的共识协议。ParallelRaft 是商业数据库阿里 PolarDB 的分布式文件系统 PolarFS 中的复制协议。我们展示了 IPA 框架在真实场景中易于使用,同时显著降低了模型检测代价。
引用
@article{arxiv.2202.11385,
title = {Compositional Model Checking of Consensus Protocols Specified in TLA+ via Interaction-Preserving Abstraction},
author = {Xiaosong Gu and Wei Cao and Yicong Zhu and Xuan Song and Yu Huang and Xiaoxing Ma},
journal= {arXiv preprint arXiv:2202.11385},
year = {2022}
}
备注
32 pages, 18 figures (with appendix)