无冲突复制数据类型(conflict-free replicated data types,简称CRDT)是一种封装了冲突消解策略的分布式复制数据类型,它能够保证分布式系统中副本节点间的强最终一致性,即执行了相同更新操作的副本节点具有相同的状态.CRDT协议设计精巧...无冲突复制数据类型(conflict-free replicated data types,简称CRDT)是一种封装了冲突消解策略的分布式复制数据类型,它能够保证分布式系统中副本节点间的强最终一致性,即执行了相同更新操作的副本节点具有相同的状态.CRDT协议设计精巧,不易保证其正确性.旨在采用模型检验技术验证一系列CRDT协议的正确性.具体而言,构建了一个可复用的CRDT协议描述与验证框架,包括网络通信层、协议接口层、具体协议层与规约层.网络通信层描述副本节点之间的通信模型,实现了多种类型的通信网络.协议接口层为已知的CRDT协议(分为基于操作的协议与基于状态的协议)提供了统一的接口.在具体协议层,用户可以根据协议的需求选用合适的底层通信网络.规约层则描述了所有CRDT协议都需要满足的强最终一致性与最终可见性(所有的更新操作最终都会被所有的副本节点接收并处理).使用TLA+形式化规约语言实现了该框架,然后以Add-Wins Set复制数据类型为例,展示了如何使用框架描述具体协议,并使用TLC模型检验工具来验证协议的正确性.展开更多
为高效地处理移动协同编辑中用户积累的大量本地操作,实现移动协同编辑系统的高响应性,提出一种支持序列转换的可交换复制数据类型(commutative replicated data type,CRDT)算法.首先,提出一个移动协同编辑的总体框架,支持多个移动终端...为高效地处理移动协同编辑中用户积累的大量本地操作,实现移动协同编辑系统的高响应性,提出一种支持序列转换的可交换复制数据类型(commutative replicated data type,CRDT)算法.首先,提出一个移动协同编辑的总体框架,支持多个移动终端离线或在线地协同编辑共享文档副本;然后,提出一个支持序列转换的移动协同编辑算法,可以实现离线操作中多个首尾连接的顺序插入操作的自动转换和操作效果的合并,维护移动协同编辑中共享文档副本的一致性.相关实验表明所提出的算法在响应性和功耗方面优于典型的一致性维护方法.展开更多
文摘无冲突复制数据类型(conflict-free replicated data types,简称CRDT)是一种封装了冲突消解策略的分布式复制数据类型,它能够保证分布式系统中副本节点间的强最终一致性,即执行了相同更新操作的副本节点具有相同的状态.CRDT协议设计精巧,不易保证其正确性.旨在采用模型检验技术验证一系列CRDT协议的正确性.具体而言,构建了一个可复用的CRDT协议描述与验证框架,包括网络通信层、协议接口层、具体协议层与规约层.网络通信层描述副本节点之间的通信模型,实现了多种类型的通信网络.协议接口层为已知的CRDT协议(分为基于操作的协议与基于状态的协议)提供了统一的接口.在具体协议层,用户可以根据协议的需求选用合适的底层通信网络.规约层则描述了所有CRDT协议都需要满足的强最终一致性与最终可见性(所有的更新操作最终都会被所有的副本节点接收并处理).使用TLA+形式化规约语言实现了该框架,然后以Add-Wins Set复制数据类型为例,展示了如何使用框架描述具体协议,并使用TLC模型检验工具来验证协议的正确性.
文摘为高效地处理移动协同编辑中用户积累的大量本地操作,实现移动协同编辑系统的高响应性,提出一种支持序列转换的可交换复制数据类型(commutative replicated data type,CRDT)算法.首先,提出一个移动协同编辑的总体框架,支持多个移动终端离线或在线地协同编辑共享文档副本;然后,提出一个支持序列转换的移动协同编辑算法,可以实现离线操作中多个首尾连接的顺序插入操作的自动转换和操作效果的合并,维护移动协同编辑中共享文档副本的一致性.相关实验表明所提出的算法在响应性和功耗方面优于典型的一致性维护方法.
