CRDT协议的TLA+描述与验证

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

二维表格实时协同编辑系统的一致性维护

二维电子表格是应用最为广泛的计算机应用程序之一,随着大数据和云计算的兴起,对二维电子表格的协同编辑需求也日益增长,而CRDT(无冲突复制数据类型)作为近年来被提出的一致性维护方法,基于它的二维电子表格协同编辑方法在以前的文献中很少被研究.本文提出了一种基于CRDT的同步方法,通过检测操作间的关系,调用相应的冲突消解函数,以实现表格协同文档的一致性维护.本文首先定义了4种操作关系:1)正交冲突关系、一维冲突关系、互斥关系和相容关系;2)提出了一种基于CRDT框架下的冲突消解方案来处理这4种操作关系;3)从理论上分析了本文所提出算法的时间复杂度和空间复杂度;4)通过理论证明和实例研究,验证了该算法的正确性,同时本文还开发了Web端的在线表格协同编辑系统Co-Table,进一步证实了算法的正确性.

移动协同编辑中基于CRDT的序列转换算法

为高效地处理移动协同编辑中用户积累的大量本地操作,实现移动协同编辑系统的高响应性,提出一种支持序列转换的可交换复制数据类型(commutative replicated data type,CRDT)算法.首先,提出一个移动协同编辑的总体框架,支持多个移动终端离线或在线地协同编辑共享文档副本;然后,提出一个支持序列转换的移动协同编辑算法,可以实现离线操作中多个首尾连接的顺序插入操作的自动转换和操作效果的合并,维护移动协同编辑中共享文档副本的一致性.相关实验表明所提出的算法在响应性和功耗方面优于典型的一致性维护方法.

Elsa:一种面向跨区域架构的无协调分布式键值存储系统

作为具备高性能和高可伸缩性的分布式存储解决方案,键值存储系统近年来被广泛采用,例如Redis、MongoDB、Cassandra等.分布式存储系统中广泛使用的多副本机制一方面提高了系统吞吐量和可靠性,但同时也增加了系统协调和副本一致性的额外开销.对于跨域分布式系统来说,远距离的副本协调开销甚至可能成为系统的性能瓶颈,降低系统的可用性和吞吐量.提出分布式键值存储系统Elsa,这是一种面向跨区域架构的无协调键值存储系统.Elsa在保证高性能和高可拓展性的基础上,采用无冲突备份数据结构(CRDT)技术来无协调的保证副本间的强最终一致性,降低了系统节点间的协调开销.在阿里云上构建了跨4数据中心8节点的跨区域分布式环境,进行了大规模分布式性能对比实验,实验结果表明:在跨域的分布式环境下,对于高并发争用的负载,Elsa系统的性能具备明显的优势,最高达到MongoDB集群的7.37倍,Cassandra集群的1.62倍.

文件管理中一种新颖的冲突检测和解决方法

随着云服务的快速发展,越来越多的应用软件被迁移到云端以提供更好的协作支持.而企业面对日渐增长的庞杂的文件,单人管理文件显得力不从心,提高文件管理的效率迫在眉睫.多人实时协同管理文件不仅可以提高文件管理效率,同时也可以清楚的了解同伴的意愿需求,提高用户的体验度.而实时的多人协同管理文件中面临的最大的挑战就是维护文件管理系统的一致性维护.传统的一致性维护方法通常是基于复杂的控制机制和转换函数来维护协作文本的一致性,这对于云环境下的协同管理不是很理想的.近年来,CRDT(Commutative Replicated Data Type)被提出作为协作文本编辑中的新的一致性维护机制,但鲜少将其应用到云环境和文件管理等场景下.本文提出了一种新的基于CRDT的冲突检测和解决方法,来维护文件协同管理的最终一致性.首先定义操作之间的关系,并提出了基于CRDT的冲突检测机制;其次,提出基于CRDT的冲突解决的有效方案;最后,举例并证明了提出方案的正确性,并从理论上分析其时间复杂度和空间复杂度.因此,本文所提出的方法可以大大提高云环境下文件协同管理的正确性和高效性.

大规模实时图形编辑中可交换复制数据模型一致性维护

CRDT(交换复制数据类型)已经被提出作为协作文本编辑中的新的替代机制.但是,基于CRDT的实时图形编辑系统一致性维护方法系统在以前的文献中很少被研究.本文提出了一种新颖高效的CRDT算法,并且把图形之间的存在的位置条件的约束关系,用动态规则库标识,把图形操作分为基本操作和预定义关系操作,并且给出相关解决方案.该算法集成了智能和大规模协作的不同类型的图形操作.首先,该算法在交换复制模型框架下保证协同用户的收敛和维护操作意图.其次,基于CRDT的新颖的算法,维护实时协同编辑下共享图形文档的一致性并给出了实例证明以及合理的案例分析.第三,理论上分析所提出算法的时间复杂度低于现有技术OT算法的时间复杂度.第四,实验评估表明,该算法优于现有的OT算法.同时本文开发了Web平台下的在线协同图形编辑系统Co-Drawing,进一步验证了所写算法的可行性.