基于TLA+的CRDT协议验证框架
source link: https://zhuanlan.zhihu.com/p/86256851
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
基于TLA+的CRDT协议验证框架
[2020.4.22] 论文全文参见：CRDT协议的TLA+描述与验证
无冲突复制数据类型CRDT的研究近年引起了学术界和工业届的关注。学术界可以参考近年相关顶级国际会议的论文。工业界比较有名的包括Redis系统的企业版，提供CRDT支持，Riak中提供了CRDT支持等。
我们研究CRDT协议的形式化验证，同样以TLA+工具集为基本技术手段。近期的一份工作开源在github上：基于TLA+的CRDT验证框架。相关论文投往了软件学报的一个专刊，正式定稿后同样会发布出来。
我们这份工作，特别是框架的构建，受到下面这份基于Isabelle的验证工作的工作的启发：
Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan, and Alastair R. Beresford. 2017. Verifying strong eventual consistency in distributed systems.Proc. ACM Program. Lang.1, OOPSLA, Article 109 (October 2017), 28 pages. DOI: https://doi.org/10.1145/3133933
借用github项目中的一段话和一幅图，对这份工作做一个简单的介绍：
无冲突复制数据类型(Conflict-free Replicated Data Types,CRDTs)是一种抽象分布式数据类型,它封装了并发冲突的消解策略,向上层应用提供所需的强最终一致性。
本项目基于TLA+语言和TLC模型检验工具给出了一个可复用的、模块化的 CRDT 协议描述与验证框架,它包括网络通信层、协议接口层、具体协议层与规约层。
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK