软件学报

作者：纪业，魏恒峰，黄宇，吕建

单位：纪业，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002311,魏恒峰，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002302,黄宇，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002303,吕建，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002304

关键词：无冲突复制数据类型;强最终一致性;最终可见性;模型检验;TLA+

基金：国家重点研发计划（2017YFB1001801）；国家自然科学基金（61702253，61772258）

无冲突复制数据类型（conflict-free replicated data types，简称CRDT）是一种封装了冲突消解策略的分布式复制数据类型，它能够保证分布式系统中副本节点间的强最终一致性，即执行了相同更新操作的副本节点具有相同的状态.CRDT协议设计精巧，不易保证其正确性.旨在采用模型检验技术验证一系列CRDT协议的正确性.具体而言，构建了一个可复用的CRDT协议描述与验证框架，包括网络通信层、协议接口层、具体协议层与规约层.网络通信层描述副本节点之间的通信模型，实现了多种类型的通信网络.协议接口层为已知的CRDT协议（分为基于操作的协议与基于状态的协议）提供了统一的接口.在具体协议层，用户可以根据协议的需求选用合适的底层通信网络.规约层则描述了所有CRDT协议都需要满足的强最终一致性与最终可见性（所有的更新操作最终都会被所有的副本节点接收并处理）.使用TLA+形式化规约语言实现了该框架，然后以Add-Wins Set复制数据类型为例，展示了如何使用框架描述具体协议，并使用TLC模型检验工具来验证协议的正确性.

来源：2020年第5期

《软件学报》期刊编辑部

查看软件学报杂志2020年第5期