无冲突复制数据类型(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)算法.首先,提出一个移动协同编辑的总体框架,支持多个移动终端离线或在线地协同编辑共享文档副本;然后,提出一个支持序列转换的移动协同编辑算法,可以实现离线操作中多个首尾连接的顺序插入操作的自动转换和操作效果的合并,维护移动协同编辑中共享文档副本的一致性.相关实验表明所提出的算法在响应性和功耗方面优于典型的一致性维护方法.展开更多
随着云服务的快速发展,越来越多的应用软件被迁移到云端以提供更好的协作支持.而企业面对日渐增长的庞杂的文件,单人管理文件显得力不从心,提高文件管理的效率迫在眉睫.多人实时协同管理文件不仅可以提高文件管理效率,同时也可以清楚的...随着云服务的快速发展,越来越多的应用软件被迁移到云端以提供更好的协作支持.而企业面对日渐增长的庞杂的文件,单人管理文件显得力不从心,提高文件管理的效率迫在眉睫.多人实时协同管理文件不仅可以提高文件管理效率,同时也可以清楚的了解同伴的意愿需求,提高用户的体验度.而实时的多人协同管理文件中面临的最大的挑战就是维护文件管理系统的一致性维护.传统的一致性维护方法通常是基于复杂的控制机制和转换函数来维护协作文本的一致性,这对于云环境下的协同管理不是很理想的.近年来,CRDT(Commutative Replicated Data Type)被提出作为协作文本编辑中的新的一致性维护机制,但鲜少将其应用到云环境和文件管理等场景下.本文提出了一种新的基于CRDT的冲突检测和解决方法,来维护文件协同管理的最终一致性.首先定义操作之间的关系,并提出了基于CRDT的冲突检测机制;其次,提出基于CRDT的冲突解决的有效方案;最后,举例并证明了提出方案的正确性,并从理论上分析其时间复杂度和空间复杂度.因此,本文所提出的方法可以大大提高云环境下文件协同管理的正确性和高效性.展开更多
文摘无冲突复制数据类型(conflict-free replicated data types,简称CRDT)是一种封装了冲突消解策略的分布式复制数据类型,它能够保证分布式系统中副本节点间的强最终一致性,即执行了相同更新操作的副本节点具有相同的状态.CRDT协议设计精巧,不易保证其正确性.旨在采用模型检验技术验证一系列CRDT协议的正确性.具体而言,构建了一个可复用的CRDT协议描述与验证框架,包括网络通信层、协议接口层、具体协议层与规约层.网络通信层描述副本节点之间的通信模型,实现了多种类型的通信网络.协议接口层为已知的CRDT协议(分为基于操作的协议与基于状态的协议)提供了统一的接口.在具体协议层,用户可以根据协议的需求选用合适的底层通信网络.规约层则描述了所有CRDT协议都需要满足的强最终一致性与最终可见性(所有的更新操作最终都会被所有的副本节点接收并处理).使用TLA+形式化规约语言实现了该框架,然后以Add-Wins Set复制数据类型为例,展示了如何使用框架描述具体协议,并使用TLC模型检验工具来验证协议的正确性.
文摘为高效地处理移动协同编辑中用户积累的大量本地操作,实现移动协同编辑系统的高响应性,提出一种支持序列转换的可交换复制数据类型(commutative replicated data type,CRDT)算法.首先,提出一个移动协同编辑的总体框架,支持多个移动终端离线或在线地协同编辑共享文档副本;然后,提出一个支持序列转换的移动协同编辑算法,可以实现离线操作中多个首尾连接的顺序插入操作的自动转换和操作效果的合并,维护移动协同编辑中共享文档副本的一致性.相关实验表明所提出的算法在响应性和功耗方面优于典型的一致性维护方法.
文摘随着云服务的快速发展,越来越多的应用软件被迁移到云端以提供更好的协作支持.而企业面对日渐增长的庞杂的文件,单人管理文件显得力不从心,提高文件管理的效率迫在眉睫.多人实时协同管理文件不仅可以提高文件管理效率,同时也可以清楚的了解同伴的意愿需求,提高用户的体验度.而实时的多人协同管理文件中面临的最大的挑战就是维护文件管理系统的一致性维护.传统的一致性维护方法通常是基于复杂的控制机制和转换函数来维护协作文本的一致性,这对于云环境下的协同管理不是很理想的.近年来,CRDT(Commutative Replicated Data Type)被提出作为协作文本编辑中的新的一致性维护机制,但鲜少将其应用到云环境和文件管理等场景下.本文提出了一种新的基于CRDT的冲突检测和解决方法,来维护文件协同管理的最终一致性.首先定义操作之间的关系,并提出了基于CRDT的冲突检测机制;其次,提出基于CRDT的冲突解决的有效方案;最后,举例并证明了提出方案的正确性,并从理论上分析其时间复杂度和空间复杂度.因此,本文所提出的方法可以大大提高云环境下文件协同管理的正确性和高效性.