Kleppmann Deploys CRDTs to Ditch Cloud Servers in Document Editing

Kleppmann采用CRDT摆脱文档协作对云端服务器的依赖 与丢弃冲突输入的共识算法或需要中心化协调的云架构不同，经过形式化验证的CRDT通过保留所有并发操作，确保去中心化网络中的副本收敛。 Kleppmann将共识机制（选出单一胜者以防止双重支付）与协作收敛进行了对比，后者允许系统保留并合并所有并发编辑。在分析了操作转换（OT）在历史上容易出错的演变及其对中心化服务器的依赖之后，他介绍了无冲突复制数据类型（CRDT），将其作为一种稳健、经过数学验证的替代方案，支持离线优先和去中心化工作流。他详细介绍了其团队如何利用Isabelle交互式定理证明器，在对抗性网络条件下对RGA等算法进行形式化验证，从而确保强最终一致性。最后，Kleppmann解析了开源JavaScript JSON CRDT库Automerge，展示了仅追加操作日志、稳定的字符ID以及跳跃遍历规则如何在实践中解决复杂的并发编辑问题。 协同编辑依赖的是收敛而非共识；分布式共识通过选出单一胜者来丢弃冲突操作，而CRDT则保留并合并所有并发变更，最终达到完全一致的状态。 (14:11) 传统的操作转换（OT）经历会长达二十年存在缺陷的收敛证明，最终稳定为像Google Docs这样依赖中心化服务器的实现，但这也阻碍了本地网络间的直接同步。 (9:55) Kleppmann的团队使用Isabelle交互式定理证明器，形式化验证了CRDT实现（包括RGA、OR-Set和计数器）在对抗性网络条件下均满足强最终一致性。 (17:26) Automerge通过ES6代理将标准的命令式JSON修改转换为仅追加的操作日志，保留完整的编辑历史，从而实现类似Git的分支处理以及时间旅行状态重构。 (20:02)

Martin Kleppmann argues that collaborative software should move beyond centralized client-server models by adopting Conflict-free Replicated Data Types (CRDTs), which achieve deterministic convergence across arbitrary, decentralized network topologies. Convergence vs. Consensus and Centralized Operational Transformation (1:17) Collaborative applications require convergence, ensuring that all distributed replicas reach an identical state after concurrent edits propagate. Kleppmann contrasts this goal with consensus algorithms like Paxos or Raft: while consensus protocols and blockchains select a single valid proposal and reject conflicting alternatives, collaborative editing must merge all concurrent actions into a coherent state. For two decades starting in the late 1980s, the dominant collaborative mechanism was Operational Transformation (OT), but early proposals suffered from subtle concurrency bugs that caused replicas to diverge permanently. Although provably correct OT algorithms eventually emerged to power systems like Google Docs, they require a star topology centered around a single server. This requirement prevents direct, local-network peer synchronization between devices in physical proximity without an external internet connection. Formal Verification and Algorithmic Mechanics (17:26) To prevent the design errors that historically afflicted OT, Kleppmann's research group used the Isabelle interactive theorem prover to formally verify their CRDT designs, including Replicated Growable Arrays (RGA), Observed-Remove Sets, and distributed counters. The proofs established that these structures satisfy Strong Eventual Consistency across an adversarial network model that arbitrarily delays, duplicates, reorders, or drops messages. In text editing CRDTs, stability is achieved by addressing characters using unique, monotonic identifier pairs (such as a counter and a node ID like 4a) rather than shifting array offsets. When concurrent insertions target the same location, replicas execute a deterministic comparison rule: an incoming operation advances past any consecutive characters whose IDs are strictly greater than its own until encountering a smaller ID or the end of the run. This symmetry ensures identical character ordering across all replicas regardless of network delivery sequence. Automerge Architecture and Conflict Handling (20:02) These concepts are implemented in Automerge, an open-source JavaScript library that models state as an immutable, JSON-like tree of nested lists and maps. Applications execute standard imperative mutations intercepted by JavaScript ES6 proxies, which translate operations into granular micro-operations appended to an immutable operation log. Full log retention enables time travel debugging and reconstruction of prior document states without complex compaction routines. Disjoint updates and idempotent operations (like concurrent character deletions) combine cleanly. When concurrent writes conflict over a single field—such as differing values for a task description—Automerge deterministically displays one value while retaining alternatives in an internal conflicts metadata structure so client applications can surface manual resolution if needed. For concurrent text edits, both entries are preserved and sequenced by node ID, mirroring the operational expectations of applications like Google Docs. Network Independence and Prototype Applications (20:48) Automerge operates entirely in-memory as a local data structure library, remaining deliberately agnostic to underlying networking protocols. Developers can transport operation logs over standard WebSockets, direct WebRTC data channels via libraries like MPL, or peer-to-peer append-only systems like the Dat project's Hypercore via Hypermerge. The research group validated this transport flexibility using prototype applications: Trellis, a serverless peer-to-peer Kanban board, and Pixel Pusher, a collaborative pixel art canvas supporting asynchronous branching, variant inspection, and manual merge workflows. Kleppmann emphasizes that while Automerge has supported functional non-trivial applications, it remains research software rather than a turnkey production system. Algorithmic implementations continue to evolve beyond earlier published JSON CRDT papers, with active architectural documentation maintained in the project's repository.

剑桥大学分布式系统研究员 Martin Kleppmann 指出，协作应用的核心目标是通过无冲突复制数据类型（CRDT）实现收敛，而非传统区块链所依赖的全局共识。通过交互式定理证明器对算法正确性进行形式化验证，可以在摆脱集中式服务器限制的前提下，构建健壮的去中心化与本地优先（Local-First）协作系统。 协作收敛与分布式共识的本质区别 (1:17) 在以 Google Docs 为代表的协作软件中，首要目标是收敛（Convergence），即无论用户操作以何种网络顺序传播，停止并发修改后所有节点的文档状态必须完全一致。Kleppmann 明确指出，这与分布式共识（Consensus，如 Paxos 或 Raft）有着根本区别。共识算法的核心机制是在出现冲突提案时进行仲裁，选出一个全局唯一且全序的胜者并丢弃其他冲突，典型的应用是区块链用于防止数字货币的双重支付。然而，协作协议的目标是完整保留所有协作者的并发修改意图，并将这些部分有序的变更确定性地合并为同一状态，而不是挑选赢家。 操作转换的历史困境与 CRDT 形式化验证 (9:55) 自 20 世纪 80 年代末以来，协作系统长期采用操作转换（OT）算法，但 OT 在学术界遭遇了长达二十年的困境：学者们提出算法并给出逻辑证明后，往往几年后就会被后续研究发现微妙的并发边界漏洞导致永久性发散。为了彻底避免这种问题，最终被证明正确的 OT 变体不得不严格依赖集中式星型拓扑，迫使所有通信必须经由中心服务器进行全局排序。这种限制导致两台相距仅 50 厘米的本地设备即使通过 Wi-Fi 或蓝牙也无法直接同步，必须将流量绕经远端数据中心。为打破这一限制，Kleppmann 团队转向基于多主架构的 CRDT，并使用 Isabelle 交互式定理证明器对可增长复制数组（RGA）、集合（OR-Set）与计数器（P-N Counter）进行机器级形式化验证，在数学上证明了这些算法在任意网络延迟、消息重排、重复甚至丢包等恶劣网络模型下，均能严格满足强最终一致性（SEC）。 Automerge 的 JSON 抽象与底层微操作模型 (20:02) 为了将经过形式化验证的 CRDT 算法付诸工程实践，Kleppmann 团队开发了开源 JavaScript 库 Automerge。Automerge 提供类似于原生 JSON 的数据模型，由任意嵌套的列表（List）和键值字典（Map）组成，其内部状态保持不可变性。上层应用调用 `Automerge.change` 时，底层通过 ES6 Proxy 代理对象拦截常规的命令式操作（如 `.push()` 或直接属性赋值），并将其分解为细粒度的原子操作日志，包括创建 Map 实体、填充键值、分配列表槽位及建立关联。这种仅追加操作日志（Append-only Log）的设计借鉴了 Git 的版本控制思想，不仅使系统天然具备任意历史快照的时空穿梭（Time Travel）与差异审查能力，还通过轻量级网络解耦设计，允许上层接入 WebSockets、基于 WebRTC 的 MPL 库，或基于 Dat 项目 Hypercore 日志的 Hypermerge 等多种点对点网络栈，并在 Trellis（看板系统）和 Pixel Pusher（像素画编辑器）等原型中完成了验证。 字段覆盖与文本序列并发插入的确定性规则 (32:15) 在处理并发修改时，无冲突操作能天然合并，但同一实体被并发修改时需依赖算法规则。对于对象属性覆盖冲突（例如两部设备同时离线修改待办事项，分别填写不同的文本），Automerge 无法判断主观对错，因此会确定性地选取一个默认展示值，同时将另一个竞态值与节点 ID 保存在 `_conflicts` 元数据对象中，以便上层界面提供手动冲突解决选项；而对于文本删除，并发删除相同内容被视为幂等操作。在文本序列并发插入中，Automerge 彻底舍弃了因增删而动态漂移的数字索引，为每个字符分配全局唯一且不可变的位置标识符（由单调递增计数器和节点 ID 组成，例如 `4a`、`4b`），并通过前驱字符标识符锚定插入位置。当两个节点在完全相同的前驱后并发插入时，算法采用基于 ID 大小的扫描规则：若新到达操作的 ID 小于后续已有元素的 ID，指针将持续向右跳过这些更大 ID 的元素，直至遇到小于自身 ID 的节点或末尾再执行插入。这一确定性遍历规则确保了不同节点按任意顺序接收网络消息时，都能将交叉文本拼装为严格一致的字符序列。 Kleppmann 坦言 Automerge 当初作为研究型代码开发，尚不能视作完备的生产就绪级软件，也尚未实现复杂的操作日志垃圾回收机制。但其实践验证了 CRDT 在构建无需中心化服务器、支持完全离线和点对点直接同步的分布式富协作系统上的巨大潜力与可靠性。

## Background 该视频由技术分享频道 InfoQ 于 2018 年 10 月 2 日发布在 YouTube 上，记录了 Martin Kleppmann 在 QCon London 2018 上的技术演讲。根据页面介绍，演讲探讨了在缺乏中心权威节点的分布式系统中如何确保数据一致性，涵盖手机与笔记本无需借助云端即可直连同步，以及基于点对点（P2P）网络的多人文档协同算法。 ## TL;DR Martin Kleppmann 深入剖析了多人实时协同系统在去中心化网络环境下面临的数据一致性难题。他回顾了操作转换（OT）算法因边界漏洞频出、长年无法在无中心化服务器场景下自洽的“血泪史”，指出文档协同追求的是接纳所有修改并实现最终收敛，这与区块链中以丢弃冲突分支为手段的共识协议有着本质区别。通过引入 Isabelle 定理证明器对 CRDT（无冲突复制数据类型）进行严格的数学形式化验证，其团队开发了基于类 JSON 不可变数据模型的开源库 Automerge，并在此之上成功构建了无需中心服务器的看板 Trellis 和像素画协同工具 Pixel Pusher。演讲还重点拆解了文本 CRDT 为每个字符分配全局唯一 ID、基于前驱字符进行相对插入，以及利用确定性“跳过规则”（Skip-over Rule）解决同位插入冲突的底层运行机制。 ## Atmosphere & style 整场演讲开篇带有一丝别样的现实戏剧性——主讲人平静地声明自己当天正因英国高校养老金争议处于正式罢工状态，但仍以纯粹的技术爱好者身份登台。随后，演讲迅速转入学术硬核与工程务实兼具的技术分享，在回顾操作转换算法二十年屡屡翻车时言辞幽默而辛辣，直击痛点。随着话题推进至定理证明器、字符唯一标识以及跳过规则的逐步推演，现场氛围严谨周密、层层递进，主讲人既有着直面并发边界盲区的理性克制，又毫不掩饰将研究成果转化为开源可用工具的探索热情。 ## Bulletin - [09:55](https://www.youtube.com/watch?v=B5NULPSiOGw&t=595s) 操作转换（OT）历经 20 年的证伪与算法缺陷循环，最终仅存的正确实现均强依赖中心化服务器，限制了对等与离线协作拓扑。 - [14:09](https://www.youtube.com/watch?v=B5NULPSiOGw&t=849s) CRDT 与区块链共识具有本质差异：共识协议通过仲裁丢弃冲突提案以防止双花，而协同编辑追求接纳并融合所有并发操作以保证最终收敛。 - [17:27](https://www.youtube.com/watch?v=B5NULPSiOGw&t=1047s) 研究团队使用 Isabelle 交互式定理证明器对 RGA 等 CRDT 算法及极端不可靠网络抽象完成形式化验证，在数学上证明了强最终一致性（SEC）。 - [19:55](https://www.youtube.com/watch?v=B5NULPSiOGw&t=1195s) 开源项目 Automerge 为去中心化协同应用提供了类 JSON 的数据抽象，并借助不可变状态、Proxy 代理拦截和全量操作日志支持原生“时间旅行”机制。 ## Key takeaways - [01:17](https://www.youtube.com/watch?v=B5NULPSiOGw&t=77s) 协同系统的核心技术目标是收敛性（Convergence），即多节点并发修改经异步网络交换后必须呈现完全一致的状态。 - [06:29](https://www.youtube.com/watch?v=B5NULPSiOGw&t=389s) 为保留文本意图、集合增删以及计数器自增操作，系统不能仅做静态状态对比或直接覆盖，必须捕获并重放细粒度的变更操作序列。 - [09:55](https://www.youtube.com/watch?v=B5NULPSiOGw&t=595s) 早期操作转换（OT）算法在学术界反复出现隐蔽的并发边界漏洞，导致长达二十年的证伪循环，最终可行的方案均被迫绑定中心服务器。 - [12:09](https://www.youtube.com/watch?v=B5NULPSiOGw&t=729s) 去中心化协同旨在摆脱中心化云端转发约束，允许设备在局域网、蓝牙或 P2P 等任意非集中式网络拓扑中直接双向对齐。 - [14:09](https://www.youtube.com/watch?v=B5NULPSiOGw&t=849s) 区块链共识在面对冲突时采取“多选一”并淘汰其余提案，而协同编辑若抛弃用户输入会造成灾难性数据丢失，两者理论目标截然不同。 - [17:27](https://www.youtube.com/watch?v=B5NULPSiOGw&t=1047s) 直觉推演极难覆盖并发边界，研究团队通过 Isabelle 定理证明器确立了 CRDT 在丢包、乱序等极端恶劣网络模型下的强最终一致性。 - [23:59](https://www.youtube.com/watch?v=B5NULPSiOGw&t=1439s) Automerge 本身解耦了网络传输层，开发者可根据需要在 WebRTC、Dat/Hypercore 或中心化 WebSocket 之间自由切换通信方案。 - [26:30](https://www.youtube.com/watch?v=B5NULPSiOGw&t=1590s) Automerge 遵循不可变状态理念，通过 JavaScript Proxy 拦截命令式调用并拆解为底层微操作，完整保留操作日志以实现“时间旅行”切片还原。 - [32:15](https://www.youtube.com/watch?v=B5NULPSiOGw&t=1935s) 当面对同名字段覆盖冲突时，系统采用确定性规则选出一个展示值，并将其他冲突值保存在 _conflicts 对象中交由 UI 和人工决断。 - [35:42](https://www.youtube.com/watch?v=B5NULPSiOGw&t=2142s) 文本 CRDT 通过为字符分配由递增计数器与节点 ID 构成的全局唯一标识，使用相对锚点定位来免疫绝对偏移量漂移。 - [40:33](https://www.youtube.com/watch?v=B5NULPSiOGw&t=2433s) 在相同位置并发插入字符时，CRDT 引入基于操作 ID 比较的跳过规则（Skip-over Rule）实现确定性偏序排序，确保所有副本达成无歧义收敛。 - [42:26](https://www.youtube.com/watch?v=B5NULPSiOGw&t=2546s) Automerge 虽仍属研究性质代码库，但已通过宽松开源协议开放给社区，足以支持看板和多人绘图等非平庸的离线优先应用开发。 ## Detailed walkthrough ### [00:04](https://www.youtube.com/watch?v=B5NULPSiOGw&t=4s) 个人背景与罢工声明 演讲者 Martin Kleppmann 首先向观众介绍了自己。大约一年前，他出版了《Designing Data-Intensive Applications》（设计数据密集型应用）一书。不过他明确指出，那本书的主题并不是 CRDT（无冲突复制数据类型），而是对大规模数据系统架构以及分布式系统各类难题的广泛综述。而他当天要分享的内容则属于另一个完全不同的技术领域。 随后现场出现了一段插曲，Martin Kleppmann 坦言自己是剑桥大学的研究员，但“今天我实际上在正式罢工”。当时英国多所大学正处于激烈的劳资争议之中，校方高层试图以一种非常激进且毫无道理的方式大幅削减教职工的养老金计划，这实质上等同于一次严重且不合理的降薪。尽管正在参与罢工，但他依然选择按原计划登台演讲，因为教职工针对的是大学资方而非 QCon 大会。Martin Kleppmann 郑重声明：“我今天是以一个碰巧对分布式系统感兴趣的普通个人身份来做这场演讲，而不是代表大学。” - Martin Kleppmann 著有《Designing Data-Intensive Applications》，该书聚焦于大规模数据架构与分布式系统问题。 - 当时英国高校正就养老金削减方案展开教工罢工争议。 --- ### [01:17](https://www.youtube.com/watch?v=B5NULPSiOGw&t=77s) 协同应用与收敛性属性 切入技术正题后，Martin Kleppmann 提出了本次演讲的核心探讨对象——协同应用（Collaborative Applications）。这类系统最经典的代表就是 Google Docs。在 Google Docs 中，多位用户可以同时对同一份文档展开协作与编辑，完全免去了通过电子邮件来回发送文档附件的繁琐流程。 在这类系统中，系统的核心目标是“收敛性”（Convergence Property）：即使多位用户在同一时刻并发修改文档，当他们在网络中完成通信和数据同步后，所有人的屏幕上最终必须展现出完全一致的文档内容。当天上午，Heidi Howard 刚做过一场关于共识算法（Consensus）的精彩演讲，共识同样旨在让分布式系统中的多个节点就某项决定达成一致。尽管协同应用与共识问题表面上看起来非常相似，但 Martin Kleppmann 强调两者存在本质区别，其系统属性和理论模型截然不同，而在后续演讲中对比这两者将是一个非常有趣的切入点。 ```mermaid flowchart LR accTitle: 文档协作的收敛性流程 accDescr: 多节点并发编辑并最终收敛为相同状态的示意图 subgraph LocalEdits["并发本地修改"] A["用户 A: 修改本地副本"] B["用户 B: 修改本地副本"] end subgraph Sync["异步通信传播"] Net["网络同步 / 消息交换"] end subgraph Convergence["收敛目标"] State["最终一致状态 (收敛)"] end A --> Net B --> Net Net --> State ``` --- ### [02:26](https://www.youtube.com/watch?v=B5NULPSiOGw&t=146s) 异步并发协同：从 Git 到 Google Docs 为了剖析并发编辑的机制，Martin Kleppmann 用一个开发者极其熟悉的场景举例：一名开发者（蓝色小人）在笔记本电脑上编写代码，修改文件后保存到本地磁盘；当准备好与团队分享时，他将代码提交到版本控制系统，并推送到 GitHub 等中心仓库。与此同时间，另一名同事（粉色小人）也在修改同一份代码并进行提交。当粉色小人想要将修改推送到服务器时，必须先拉取蓝色小人已推送的提交并执行合并（Merge）。如果两人修改的是不同文件，或者同一文件的顶部和底部，Git 可以毫无阻碍地自动完成合并；但若修改了同一行代码，Git 就会产生合并冲突（Merge Conflict），迫使开发者手动介入解决。 从更抽象的分布式系统视角来看，这些节点无论是笔记本电脑、智能手机还是数据中心的服务器，其本质都是各自保存一份数据副本的计算节点。当用户发起编辑时，修改会首先作用在本地副本上，随后这些变更才被通信传递给拥有数据副本的其他节点。在 Git 中，这种同步是通过显式的 `git push` 等操作触发的；而在 Google Docs 这类实时协同工具中，同步是在后台连续自动发生的。在 Google Docs 中，本地副本直接保存在浏览器的内存标签页中，用户每敲击一个字符，变更会“立即应用到文档的本地副本上”，绝不会等待网络往返（Round-trip）给服务器确认后再显示在屏幕上，因为那样的延迟会让输入无法忍受。在本地生效后，浏览器才在后台异步将变更发送给服务器并广播给其他协作者。 当遇到离线编辑（例如网络分区阻断了某个节点与外界的联系）时，并发问题会变得更加明显。断网的粉色用户仍然可以在本地持续修改文档，变更暂存在本地设备上，直到网络恢复后才被刷新发送出去。系统面临的严峻挑战在于：当这些脱节的变更重新汇合时，如何保证它们能被天衣无缝地自动合并在一起。 > “在那种情况下，Google Docs 实际上绝不会提示你去解决合并冲突，它总是会根据它所认为的合理方式自动合并这些变更。” —— Martin Kleppmann --- ### [06:29](https://www.youtube.com/watch?v=B5NULPSiOGw&t=389s) 多种数据类型的合并语义（文本、集合与计数器） 为阐述如何自动且合理地合并冲突，Martin Kleppmann 逐一分析了文本、集合与计数器三种数据类型的合并场景： 首先是文本序列。假设文档初始状态为字符串 `"hello!"`。粉色用户并发地在感叹号前插入单词 `"world "`，而蓝色用户则在感叹号后追加笑脸符号 `":)"`。若在 Git 中，同一位置附近的修改极可能引发人工冲突合并；但在协同文本系统中，合理的合并策略显然应当保留两者的输入意图——将 `"world "` 放在感叹号前，将笑脸放在感叹号后，最终收敛得到 `"hello world!:)"`。 ``` 初始状态: "hello!" 粉色用户: "hello world!" (在 '!' 前插入 "world ") 蓝色用户: "hello!:)" (在 '!' 后插入 ":)") ------------------------------------------------ 合并结果: "hello world!:)" (保留双向插入意图) ``` 第二种数据类型是集合（Set）。集合是无序元素的汇集。假设集合初始包含 `{A, B}`。红色用户执行删除了元素 `B`，本地仅剩 `{A}`；并发的紫色用户执行了并集操作添加了新元素 `C`，本地变为 `{A, B, C}`。当这两处变更互相传播后，合理的合并规则是：元素 `A` 未被任何人改动，予以保留；`B` 被明确删除，因此不应存在；`C` 被新增，应当纳入。最终合理的合并状态即为 `{A, C}`。 第三种数据类型是计数器（Counter），例如社交媒体贴文的点赞数。假设初始数值为 `1`。两个用户各自并发点赞了一次，两台机器在本地都将数值从 `1` 修改为了 `2`。Martin Kleppmann 强调，如果系统单纯比较两个节点的最终状态数值（两者都是 `2`）并直接取 `2` 作为合并结果，就会丢失关键信息。两台节点实际上各自执行了一次独立的增量（Increment）操作。无论这两个自增操作以何种先后顺序应用，最终正确的点赞数都应该是 `3`。 通过这三个案例，Martin Kleppmann 得出了一个核心结论：“这意味着我们不能只考虑任意时刻的数据状态值，因为如果我们仅仅对比 2 和 2，它们看起来一模一样；实际上我们必须捕获对数据所做出的变更操作序列并将它们重新应用，唯有这样才能让我们达成合理且一致的合并结果。” - 文本协同需要保留各字符插入位置的相对意图。 - 集合合并要求独立处理元素的添加与删除语义。 - 计数器合并不能单纯做状态覆盖，而必须追踪底层自增操作的发生次数。 ### [09:55](https://www.youtube.com/watch?v=B5NULPSiOGw&t=595s) 操作转换（OT）的历史与“失败算法的血泪史” 多人同时编辑内容并自动合并这一难题已被学术界研究了相当长的时间。从高层次来看，该领域主要发展出了两大算法家族：一个是自 20 世纪 80 年代末期就开始被学术界深入研究的操作转换（Operational Transformation，简称 OT），它也是 Google Docs 内部实现协同的核心基石；另一个则是为了克服 OT 缺陷而在 2000 年代初兴起的研究方向——无冲突复制数据类型（Conflict-free Replicated Data Types，简称 CRDT）。 回顾 OT 的学术发展历程，Martin Kleppmann 将其描述为一段令人沮丧的历史。80 年代末期学者们提出的第一批 OT 论文读起来条理清晰、看似无懈可击，但几年之后其他研究人员便指出：该算法根本是错的。在协同系统中，“正确”的定义是达到收敛性（Convergence），即停止编辑后，所有人的屏幕上最终必须呈现完全相同的文档内容。然而这些早期算法存在无法处理的并发编辑边界情况，会导致副本陷入永久分歧（Permanent Divergence），再也无法恢复一致。随后学者们吸取教训提出了新算法，结果几年后同样被证明存在类似的隐蔽漏洞。这种“提出算法-数年后被证伪”的循环持续了整整二十年，Martin Kleppmann 直言这演变成了一场“失败算法的血泪史（A real bloodbath of failed algorithms）”。 ```mermaid flowchart TD accTitle: 操作转换算法历史缺陷循环 accDescr: 展示学术界二十年间提出OT算法又不断被证明存在分歧缺陷的历史循环 subgraph FailureLoop["OT 算法的证伪循环（1980s-2000s）"] A["提出新 OT 算法<br/>（论文逻辑看似严密）"] --> B["数年后发现并发边界缺陷"] B --> C["系统无法收敛<br/>导致文档永久分歧"] C --> A end C --> D["硕果仅存的正确算法<br/>（强制依赖中心化服务器）"] D --> E["Google Docs 架构实现"] ``` - 学术界历经 20 年反复尝试与修补，大量 OT 算法最终均被证实无法在无约束环境下保证数据收敛。 - 最终被证明正确的少数 OT 算法（如 Google Docs 所采用的方案）都必须引入一个严格的前提约束：**依赖中心化服务器**。 --- ### [12:09](https://www.youtube.com/watch?v=B5NULPSiOGw&t=729s) 集中式协同的局限与去中心化通信拓扑 虽然基于中心化服务器的 OT 算法能够保证正确性，但这带来了极大的通信限制。在 Google Docs 模型中，所有用户（例如粉色用户与紫色用户）产生的修改必须经由中心服务器进行中继与仲裁，绝对不允许在设备之间建立侧向通道（Back Channel）直接同步，否则就会打破算法的前提假设，从而破坏收敛性。Martin Kleppmann 批评指出，即使你的手机和笔记本电脑相距仅 50 厘米，仅仅为了同步一点数据，流量也必须绕道几千公里外的弗吉尼亚数据中心，这种设计在物理与逻辑层面上都非常荒谬。 Martin Kleppmann 追求的目标是将通信模型彻底泛化，支持任意的网络拓扑结构。无论是局域网互联、蓝牙还是临时建立的对等网络，哪怕设备当前根本没有连接公网，两台设备只要能连通就应该可以直接双向同步；等到未来重新接入互联网时，再与远程节点完成最终对齐。为了实现这种摆脱中心化服务器依赖、支持离线优先的去中心化协作模式，就必须寻找比 OT 更强大的算法基础。 ```mermaid flowchart LR accTitle: 中心化与去中心化同步拓扑对比 accDescr: 对比Google Docs必须经由云端服务器与CRDT支持任意对等拓扑的通信模式 subgraph Centralized["Google Docs 集中式架构"] P1["手机"] -->|"必须走外网"| Svr["弗吉尼亚数据中心"] Lap1["笔记本"] -->|"必须走外网"| Svr end subgraph Decentralized["CRDT 任意网络拓扑"] P2["手机"] <-->|"局域网 / 离线直连"| Lap2["笔记本"] Lap2 <-.->|"恢复网络后按需同步"| Remote["远程协作节点"] end ``` > “即使只是在相隔 50 厘米的手机和笔记本电脑之间同步一些数据，数据仍然必须绕道弗吉尼亚州的数据中心，细想起来这相当荒唐。” —— Martin Kleppmann --- ### [14:09](https://www.youtube.com/watch?v=B5NULPSiOGw&t=849s) 去中心化协作与区块链共识的根本差异 当提及“去中心化”时，人们往往会下意识联想到区块链（Blockchain）。Martin Kleppmann 澄清道，尽管区块链社区也以无须信任中心服务器的去中心化为口号，但他个人对区块链并没有太大兴趣，二者的核心计算抽象有着根本性的不同。 区块链依托密码学哈希链和默克尔树保证历史记录的不可篡改与完整性，其核心机制是拜占庭共识协议（Byzantine Consensus），目标是在存在恶意节点的环境下，强行确立一个全序递增、无分叉的区块序列。在数字货币场景中，为了防止同一枚代币被双重花费（Double Spending），当出现多个冲突交易时，共识协议的职责是强行“多选一”，批准其中一笔并丢弃其余所有交易。 然而，文档协同的业务诉求恰恰与共识相反。在多人协作编辑时，如果共识算法因为冲突而选择采纳一方的修改、强行抛弃另一方辛苦写下的文字，协作体验将会彻底崩塌。协同系统追求的是保留所有人的并发输入，并通过确定性规则将其优雅地合并为一致状态。因此，协同领域的“收敛”与区块链领域的“共识”存在本质区别：共识是淘汰冲突选项的仲裁器，而 CRDT 是接纳并融合一切变动的收敛模型。 | 比较维度 | 区块链（共识协议） | 文档协同（CRDT） | |:--- |:--- |:--- | | **核心抽象** | 拜占庭共识 / 确立全序 | 保持并发操作因果关系的半格合并 | | **冲突处理** | 仲裁多选一，**抛弃**冲突的其它提案 | **保留**所有并发编辑，算法自动合并收敛 | | **典型目标** | 防止双重支付（双花） | 汇聚所有参与者的创作成果 | | **用户体验** | 丢弃无效分支属于预期保护 | 丢弃用户写的内容会导致严重数据丢失 | > “共识协议所做的，是决定采纳其中一个提案并丢弃其他的——这在区块链场景中正是你想要的，但在文档协作场景中恰恰是你最不想要的。” —— Martin Kleppmann --- ### [17:27](https://www.youtube.com/watch?v=B5NULPSiOGw&t=1047s) CRDT 的形式化验证与可靠性证明 为了避免重蹈操作转换算法长达二十年屡屡出错的覆辙，Martin Kleppmann 的研究团队在设计 CRDT 算法时，不再单纯依赖非形式化的直觉推理，而是引入了严苛的数学形式化证明。因为并发边界状态极其微妙，单凭人类肉眼和非形式化推演，根本无法百分之百确保算法在所有时序下都能收敛。 该团队采用交互式定理证明器 Isabelle，对多种核心 CRDT 算法展开了形式化建模。他们形式化证明了包括用于文本协同的 RGA 算法（Replicated Growable Array）、集合型 CRDT（AWSet / Observed-Remove Set）以及分布式计数器，确认它们严格满足“强最终一致性”（Strong Eventual Consistency, SEC）。更进一步，为了确保算法运行前提在现实世界中成立，研究团队建立了双层证明体系：第二层直接构建了一个极端不可靠的网络抽象模型——该网络被允许任意丢弃报文、乱序投递消息。形式化验证表明，即便底层网络竭尽所能地丢包与错序，第一层所需的假设依然能够在所有可能的网络执行路径中得到满足，从而在数学上确立了 CRDT 在恶劣网络环境下依然能够实现数据强收敛的铁律。 - **工业应用落地**：CRDT 已在 GitHub Atom 文本编辑器的实时协同套件（Teletype）以及 Riak 分布式键值数据库的内部冲突合并中得到实际落地。 - **数学证明工具**：使用 Isabelle 定理证明软件，排除了人为直觉漏洞，从逻辑根源杜绝并发合并 bug。 - **分层证明结构**： 1. 上层证明：在给定操作传递假设下，数据结构（RGA、集合、计数器）满足强最终一致性（SEC）。 2. 下层证明：在允许无限丢包与乱序的极端不可靠网络模型中，上述前提假设在所有执行序列下恒成立。 ### [19:55](https://www.youtube.com/watch?v=B5NULPSiOGw&t=1195s) Automerge 库的定位与 Trellis 协作看板原型 演讲者 Martin Kleppmann 提到，相关的论文即便在读者没有形式化算法验证经验的情况下，可读性也相当高，非常值得一读。不过，他希望把更多时间留给 Automerge。Automerge 是他们正在积极开发的一个开源库，实现了前述关于无冲突复制数据类型（CRDT）的一系列思想。Automerge 目前使用 JavaScript 编写，原则上它可以由任何编程语言实现，但选择 JavaScript 是看重它在多平台上的极强可移植性。 开发者可以将 Automerge 视为一个数据模型层（data model layer）或数据结构库，用来作为基础构建多人协同应用。它提供了一个与普通 JSON 非常相似的高层抽象，开发者可以直接修改这个类似 JSON 的文档，在其之上支撑业务逻辑。 为了展示其实际应用，演讲者展示了基于 Automerge 构建的原型应用。第一个叫作 Trellis，是知名项目管理工具 Trello 的复刻版本： - 界面与 Trello 极为相似，拥有泳道（columns）和泳道中的任务卡片（cards），用户可以在不同泳道间自由拖拽卡片。 - 演示示例是一个“超级英雄招募计划（superhero recruiting initiative）”，支持将列分配给不同成员、在卡片下发表评论等常见看板功能。 - 该应用最酷的地方在于**完全没有中心化服务器**；所有的协作都基于对等网络（Peer-to-Peer, P2P）运行。他们借用了通常在浏览器中用于视频通话的 WebRTC 技术，利用 WebRTC 的数据通道在不同终端之间传输 CRDT 编辑操作。 - 界面右侧配备了管理对等网络的控制面板，右下方则展示了一个变更日志（log of changes）。无论是移动卡片还是修改卡片内容，每次编辑都会即时追加在操作日志中。 ```mermaid flowchart LR accTitle: Trellis P2P Architecture accDescr: High-level peer-to-peer synchronization flow for Trellis using WebRTC and Automerge. subgraph ClientA["客户端 A (浏览器)"] UI_A["Trellis 看板 UI"] Doc_A["Automerge JSON 文档"] UI_A -->|"拖拽卡片/评论"| Doc_A end subgraph P2P["WebRTC DataChannel (无需中心服务器)"] Sync["传输 CRDT 编辑操作"] end subgraph ClientB["客户端 B (浏览器)"] Doc_B["Automerge JSON 文档"] UI_B["Trellis 看板 UI"] Doc_B -->|"更新视图"| UI_B end Doc_A --> Sync Sync --> Doc_B ``` --- ### [22:01](https://www.youtube.com/watch?v=B5NULPSiOGw&t=1321s) Pixel Pusher 与基于分支/合并的协作界面探索 团队构建的另一个原型应用是 Pixel Pusher，这是一个趣味性很强的多人协同像素画编辑器。像素艺术带有强烈的复古游戏美学特征，仅用极少数量的像素网格绘制画面，玩家常用它做出非常可爱的动画。团队拿来了 Xavier Balon 编写的现成开源单机像素画应用（原本仅是运行在浏览器中的本地客户端），在其底层接入 Automerge，改造成了一款多人协作应用。 在 Pixel Pusher 中，团队尝试探索更深层次的协作形态。协作不应仅仅是“一人改动立刻同步到另一人屏幕上”的实时敲字模式，他们希望探索类似 Git 的 Pull Request 或 Google Docs 的“建议修改（Suggesting Changes）”机制： - 在 Git 中，开发者提交 Pull Request 提出更改，仓库维护者可以选择合并、拒绝或修改后接受；Google Docs 也有提议编辑和评论的功能。 - Pixel Pusher 尝试在像素画编辑器中实现类似的界面：右上角展示了该文档的多个衍生版本。例如，基础版本画布上只有两颗眼珠，其中一个衍生版本被画成了一个“土豆人（potato man）”，另一个版本则是其他构图。 - 任何用户都可以基于当前文档创建自己的副本（分支），随心所欲地绘制；其他协作者如果满意该修改，只需通过极轻量直观的 UI 一键将其合并到自己的本地主干中。 这种分支切换与提议合并之所以能够轻量实现，关键在于 Automerge 在系统内部忠实记录了所有变更的历史流变。 --- ### [23:59](https://www.youtube.com/watch?v=B5NULPSiOGw&t=1439s) 解耦的网络层设计与类 JSON 数据模型 Martin Kleppmann 特别强调了 Automerge 的架构边界：它本身纯粹是一个数据结构抽象层，运行在单一进程中，**完全没有内置网络传输层**，也不强加任何节点间同步协议。开发者可以根据需求自由插拔不同的网络底座： - Trellis 基于 WebRTC，通过他们编写的 MPL 库实现 P2P 通信。 - Pixel Pusher 试验了另一种完全不同的网络底座——来自 DAT 项目的底层抽象（DAT 专注于对等网络数据集同步）。他们利用其 Append-only Log 抽象构建了 Hypermerge 库，将 Dat 的 Hypercore 与 Automerge 无缝拼接。 - 开发者也可以完全不走 P2P，直接使用传统的 WebSocket 或中心化服务器来转发变更。 在数据结构层面，Automerge 提供了类似 JSON 的嵌套结构。JSON 核心组合机制只有两种： 1. **列表（List）**：有序序列（ordered sequence）。 2. **字典映射（Map）**：将键（key）关联到特定值的字典结构。 这两者可以任意层级无限嵌套，构建诸如待办事项（To-do list）的应用。应用对其支持的修改操作覆盖了标准的数据交互： - 覆盖或更新现有键的原语值（如点击 Checkbox 将 `done` 状态切换为 true）。 - 编辑列表或映射中的字符串文本。 - 在列表既有项之间插入新元素。 - 在映射中添加新键，或者删除不需要的键值对。 --- ### [26:30](https://www.youtube.com/watch?v=B5NULPSiOGw&t=1590s) 不可变状态、代理拦截与“时间旅行”机制 在具体编程模型上，Automerge 遵循类似 Redux 或 Immutable.js 的不可变状态（immutable state）理念，但为了开发者体验保留了直观的命令式语法。 当需要变更数据时，开发者调用 `Automerge.change(state, commitMessage, callback)` 函数： - 当前的 `state` 永远不会被就地篡改（never modified in place），调用后将返回一个包含更新内容的全新状态对象。 - 开发者可以附带一条类似 Git 的提交说明（commit message），例如 `"Add todo item"`，它作为任意字符串原样存入编辑历史，便于用户后续回溯。 - 在传入的回调函数中，暴露出的 `doc` 对象仅在回调生命周期内可变。Automerge 巧妙地利用 JavaScript 的 `Proxy`（代理）对象拦截所有的标准命令式操作（例如直接调用 `doc.todos.push({...})` 向数组追加元素，或直接赋值）。 在底层，开发者写下的简单 `push` 会被 Automerge 拆解为细粒度的微操作（micro operations）并计入日志：创建一个空 Map、设置 `title` 字段、设置 `done` 字段、在目标列表中创建占位符位置、将新 Map 节点链接到该列表中。开发者无需手写这种繁琐的底层微操作，底层会自动完成转换。 Automerge 会永久保留整个操作日志。针对这种设计是否会导致存储膨胀的顾虑，Martin Kleppmann 打了个比方：“如果在 Git 仓库里不做浅克隆（shallow clone），其实仓库中包含了该代码库有史以来发生过的所有 commit；既然 Git 可以永久保存全部历史，那么我们也可以。”实践证明，现阶段全量保存操作日志在存储和性能上的表现出奇地好；如果未来确实出现空间压力，团队也会在后续引入压实（compaction）机制。 全量保留历史记录带来了一项杀手级特性——时间旅行（time travel）。由于所有微变更与可读的提交信息均被完整保留，系统可以极其轻巧地提取出文档自创建起经历的每一个历史状态切片。 > “And so if Git can keep all history forever, then so can we.” — Martin Kleppmann ### [29:55](https://www.youtube.com/watch?v=B5NULPSiOGw&t=1795s) 并发修改与 CRDT 的核心保证：强最终一致性（收敛） Automerge 能够通过在特定时间点筛选操作子集，高效还原出文档在历史任意时刻的快照视图。Martin Kleppmann 借此切入协作场景的核心挑战——并发修改与冲突解决。以家庭场景为例，两个用户共享一份待办清单，初始状态只包含一条未完成的任务：“浇花”（watering the plants，`done: false`）。用户与妻子各自在离线状态下编辑手机上的清单：丈夫添加了新任务“买牛奶”（buy milk，`done: false`），而妻子浇完了花，将该任务标记为已完成（`done: true`）。在本地无网络时，修改会立即写入本地副本；当网络恢复连接后，两台设备交换操作。Automerge 识别出两项操作作用于不同的数据对象，因此能够无缝合并：左侧副本应用了任务状态变更，右侧副本添加了新条目，最终两边视图完全统一。 ```mermaid flowchart LR accTitle: CRDT Convergence Model accDescr: Two offline nodes apply local edits independently, then converge to identical states after syncing. subgraph Initial["初始状态"] Doc0["待办清单: 浇花 (done: false)"] end subgraph Offline["离线并发更新"] NodeA["节点 A (丈夫)<br/>添加: 买牛奶 (done: false)"] NodeB["节点 B (妻子)<br/>更新: 浇花 (done: true)"] end subgraph Synced["同步与收敛"] MergedA["节点 A 最终状态<br/>1. 浇花 (done: true)<br/>2. 买牛奶 (done: false)"] MergedB["节点 B 最终状态<br/>1. 浇花 (done: true)<br/>2. 买牛奶 (done: false)"] end Doc0 --> NodeA Doc0 --> NodeB NodeA -->|"网络恢复同步操作"| MergedB NodeB -->|"网络恢复同步操作"| MergedA ``` 这种行为展现了 CRDT 最本质的形式化属性——收敛性（Convergence）。Martin Kleppmann 总结了这一核心原则：“如果任意两个设备或节点见到了相同的一组更新或操作，即便它们接收操作的顺序完全不同，一旦双方看全了所有的操作，其文档状态就必然完全一致。”这种强保证彻底摆脱了系统对消息到达先后顺序的依赖，保证了离线协作与弱网通信下的数据可靠性。 ### [32:15](https://www.youtube.com/watch?v=B5NULPSiOGw&t=1935s) 冲突处理机制：字段覆盖与文本并发插入 对于大多数并发操作，CRDT 都能自动干净地合并，唯一无法由算法完全“合理解析”的边缘情况，是并发修改覆盖了同一个字段或列表中的同一位置。例如，双方并发将买牛奶修改为“买豆奶”（buy soy milk）与“买杏仁奶”（buy almond milk）。系统本身无法判定哪种奶更好，因此 Automerge 采用确定性但任意（arbitrary but deterministic）的规则挑选一个值作为默认展示，同时把未选中的值保存在附属对象 `_conflicts` 中（例如标注冲突字段为 `title`，记录冲突节点 ID 及对应值 `buy almond milk`）。上层 UI 可以据此向用户呈现冲突选项，由人工介入决断。Martin 强调，向同一字段重复赋值是唯一必须保留人工决断路径的场景。 而在富文本协作中，情况截然不同。以将“hey guys”修改为性别中立用词为例，一人将其改为“hey everyone”，另一人并发改为“hey folks”。Automerge 的处理逻辑与 Google Docs 完全一致： 1. 双方都删除了“guys”，由于“删除两次等同于删除一次”，该词直接移除； 2. 双方各自插入了新内容，“everyone”与“folks”都会被保留，并依据节点唯一标识以确定性的随机顺序拼接在一起； 3. 所有副本最终统一展示为“hey everyone folks”或“hey folks everyone”。 针对文本合并可能产生语法不通顺的疑虑，Martin Kleppmann 明确指出：千万级用户每天都在依赖 Google Docs 的这种处理机制，实践证明它行之有效。相比于复杂的语义分析，更切合实际的做法是引入“建议性冲突提示”（advisory conflict）：当算法检测到两次并发编辑的物理位置极其接近（如在 20 个字符阈值之内）时，弹窗提示用户检查该语句是否通顺。 - 字段赋值冲突：系统根据节点 ID 等信息确定性地选出一个默认值，其他冲突值放入 `_conflicts` 供 UI 读取。 - 文本并发插入：保留全部插入内容，利用确定性规则统一步伐，避免内容丢失或副本分裂。 - 协作体验权衡：与其构建复杂的语义仲裁逻辑，不如借鉴成熟协同软件的机制，配合位置邻近度提示来辅助人工校对。 ### [35:42](https://www.youtube.com/watch?v=B5NULPSiOGw&t=2142s) 文本 CRDT 底层原理：唯一字符标识符与基于相对位置的插入 Martin Kleppmann 拆解了富文本列表 CRDT 的内部运行机制。假设文档初始字符为 `H-e-l-o`，节点 A 在中间补入第二个 `l` 构成“hello”，节点 B 并发在末尾加入感叹号 `!`。CRDT 解决该问题的基础，是为文档中的每一个字符赋予一个全局唯一的标识符。该标识符由一个单调递增的计数器（counter）与节点唯一标识（node ID）组合而成，形如 `2a`、`3a`、`4b`。由于各节点拥有独立的名称，且自身每生成一个操作就自增计数器，因此生成的 ID 在全网永远不会重复。 在数据同步阶段，网络传输的不是传统的基于全局偏移量的指令（如“在第 15 个字符处插入”），因为前面的任何并发增删都会破坏绝对索引。CRDT 传递的是“在某一特定 ID 的字符之后插入新字符”的相对指令： - 节点 A 产生操作：在标识符为 `2a`（即第一个 `l`）的字符后插入字符 `l`，其新标识符为 `4a`； - 节点 B 产生操作：在标识符为 `3a`（即字符 `o`）的字符后插入字符 `!`，其新标识符为 `4b`。 由于每个字符通过 ID 唯一定位，接收方无论在何时收到网络消息，都能精确找到挂载锚点并插入字符。即便节点 B 在收到节点 A 的消息时本地索引已经后移，依据 ID 进行的定位也完全不受绝对偏移量漂移的影响。 ```mermaid flowchart TD accTitle: Text CRDT Insertion Mechanics accDescr: Characters are identified by unique IDs (counter + node name) and reference their preceding character ID instead of absolute positions. subgraph Base["基准序列"] C1["H (ID: 1a)"] --> C2["e (ID: 2a)"] C2 --> C3["l (ID: 3a)"] C3 --> C4["o (ID: 4a)"] end subgraph Ops["并发操作（基于前驱 ID 插入）"] OpA["节点 A 操作:<br/>在 ID 2a 之后插入 'l' (ID: 5a)"] OpB["节点 B 操作:<br/>在 ID 4a 之后插入 '!' (ID: 5b)"] end Base -.-> OpA Base -.-> OpB ``` ### [38:20](https://www.youtube.com/watch?v=B5NULPSiOGw&t=2300s) 解决同位插入冲突：确定性移位与确定性排序规则 当两个用户同时在文档的完全相同位置插入字符时，简单的相对定位就会出现问题。设文档包含 `A-B-C`，节点 A 在 `A`（ID `1a`）与 `B` 之间插入字符串 `XY`（形成 `A-X-Y-B-C`），节点 B 并发在 `A` 与 `B` 之间插入字符串 `PQ`（形成 `A-P-Q-B-C`）。若将节点 B 的操作发送给节点 A： 1. 插入 `P`（ID `4b`），指令为插在 `1a`（字符 `A`）之后，此时 `P` 被排在 `A` 之后、`X` 之前； 2. 插入 `Q`（ID `5b`），指令为插在 `4b`（字符 `P`）之后，最终节点 A 处的序列呈现为 `A-P-Q-X-Y-B-C`。 此时如果直接将节点 A 的操作（在 `1a` 后插入 `X`，ID `4a`）原样盲目应用到节点 B，由于指令同样声明“插在 `1a` 之后”，节点 B 上的 `X` 会被排在 `P` 之前，导致双方结果镜像颠倒，违背收敛性。 为了确保节点 B 也能获得完全相同的 `A-P-Q-X-Y-B-C` 顺序，CRDT 必须引入更严谨的移位扫描规则。当节点 B 收到“在 `1a` 之后插入 `4a`”的指令时，不能直接落在 `1a` 的紧邻右侧，而必须从初始目标锚点 `1a` 出发向右扫描，对比后续并发插入元素的唯一标识符（例如比较 `4a` 与 `4b`、`5b` 的大小），依规则将插入游标越过 `P`（`4b`）和 `Q`（`5b`），最终将 `X` 放置在 `5b` 之后，从而保证跨节点的所有操作都能确定性地收敛到完全一致的排列序列。 ### [40:33](https://www.youtube.com/watch?v=B5NULPSiOGw&t=2433s) CRDT 并发列表插入与跳过规则（Skip-over Rule） Martin Kleppmann 深入拆解了在分布式列表中处理并发插入时的具体仲裁机制——基于操作 ID 比较的“跳过规则”（Skip-over Rule）。当一个新的插入操作到达时，系统会将新操作的 ID 与列表中紧随其后的元素 ID 进行大小比对。例如，当前要插入带有 ID `4a` 的字符 `X`，而当前列表中的下一个元素是字符 `P`（其 ID 为 `4b`）。由于新操作的 ID `4a` 小于已有元素的 ID `4b`，算法判定需要跳过（skip over）该元素并继续向右移动。紧接着，系统再比对下下一个元素 `Q`（其 ID 为 `5b`）；因为 `4a` 依然小于 `5b`，依据相同的规则，算法再次跳过 `Q`。直到移动到字母 `B`（其 ID 为 `2a`），系统发现 `2a` 小于 `4a`，此时终止跳过，将字符 `X` 精准插入到该位置。 Martin Kleppmann 坦言，这种规则初看并不符合直觉，这也是团队投入大量精力进行形式化验证的原因所在。他强调说：“This rule it does actually work it takes a little bit of convincing and this is why we did all of that formal proof stuff because it's not entirely obvious immediately that this actually does the right thing but it turns out that it does actually always do the right thing.” 随后处理在 `4a` 之后插入带 ID `5a` 的字符 `Y` 时，逻辑就非常直观：直接挂在刚定位好的 `X` 后面即可。因为 `2a` 小于 `5a`，`5a` 绝不会越过 `2a`；同样，另一侧拥有 ID `4b` 的插入操作 `P` 也绝不会跳过 `4a`，因为 `4b` 大于 `4a`。通过这套确定性的 ID 偏序规则，不同副本无需中心节点协调，就能收敛到完全一致的最终文档序列。 ```mermaid flowchart TD accTitle: 并发插入中的跳过规则判断流程 accDescr: 展示新元素插入列表时通过比较新旧 ID 决定向右跳过还是立即落位插入的逻辑分支 A["新操作到达: 待插入元素 (ID: 4a)"] --> B["获取下一个元素 (P, ID: 4b)"] B --> C{"4a < 4b?"} C -- "是 (跳过 P 向右移)" --> D["获取下一个元素 (Q, ID: 5b)"] D --> E{"4a < 5b?"} E -- "是 (跳过 Q 向右移)" --> F["获取下一个元素 (B, ID: 2a)"] F --> G{"4a < 2a?"} G -- "否 (4a > 2a, 停止跳过)" --> H["在 B 之前完成插入 X (ID: 4a)"] H --> I["后续插入 Y (ID: 5a) 紧随 X 之后"] ``` - **跳过判断条件**：若待插入元素的 ID 小于当前对比节点的 ID，指针继续向右跳过；若待插入元素的 ID 大于当前节点的 ID，则停止跳过并在此处落位。 - **并发插入的确定性**：ID 结合了计数器与客户端唯一标识（如节点 a、节点 b），保证了全局全序关系，从而消除歧义。 - **形式化证明的必要性**：分布式并发交错场景极为复杂，仅凭直觉极易出错，数学形式化验证是确保算法“在任何时序下始终做出正确决策”的核心保障。 --- ### [42:26](https://www.youtube.com/watch?v=B5NULPSiOGw&t=2546s) Automerge 开源项目与相关研究成果 在演示完核心算法后，Martin Kleppmann 将话题转向了实际的工程落地与开源实现——Automerge。他介绍道，Automerge 已经完全开源并采用了极其宽松的开源协议（liberal license），非常欢迎参会者和社区开发者基于它去构建和试验各类去中心化协作原型应用。不过，他也给出了坦率的技术预期管理，明确向听众说明：“I'll tell you this is research code it's not production ready we're not pretending that it's perfect in all circumstances but it does seem to be working reasonably well we were able to build some non-trivial applications on top of it so maybe you will be able to as well.” Martin Kleppmann 特别感谢了来自 Dat 项目的 Hypercore，团队在近期的研究与工程实现中正是借助了 Hypercore 来处理底层的点对点网络通信。针对想要深入探究底层理论的听众，他指引了相关的学术资源：对于形式化验证感兴趣的，可以查阅团队发表的证明论文；而目前的工程实现则是脱胎于早期关于 JSON CRDT 的研究论文。不过他也解释道，Automerge 目前所采用的算法相比最初那篇论文已经有了演进和改进，虽然最新版本的算法论文还没来得及整理成文，但 Automerge 代码仓库中提供了一份 Markdown 格式的内部架构设计文档供大家参考。最后，他顺带推荐了自己的经典著作《Designing Data-Intensive Applications》（数据密集型应用系统设计），幽默地表示这本书虽然并不专门讲 CRDT，但相信对现场关注分布式系统与数据架构的工程师依然大有裨益。 - **Automerge 现状**：属于研究性质的代码库，尚未达到工业级生产就绪状态，但已足够支撑非平庸（non-trivial）的复杂应用开发。 - **底层网络依赖**：依托 Dat 项目中的 Hypercore 协议组件实现点对点（P2P）数据流传输与同步。 - **文档与演进**：算法相比最早发表的 JSON CRDT 论文有所迭代，最新实现细节可通过 Automerge 仓库中的内部设计文档进行查阅。 ## Notable quotes > [12:09](https://www.youtube.com/watch?v=B5NULPSiOGw&t=729s) 即使只是在相隔 50 厘米的手机和笔记本电脑之间同步一些数据，数据仍然必须绕道弗吉尼亚州的数据中心，细想起来这相当荒唐。 — Martin Kleppmann > [14:09](https://www.youtube.com/watch?v=B5NULPSiOGw&t=849s) 共识协议所做的，是决定采纳其中一个提案并丢弃其他的——这在区块链场景中正是你想要的，但在文档协作场景中恰恰是你最不想要的。 — Martin Kleppmann > [29:55](https://www.youtube.com/watch?v=B5NULPSiOGw&t=1795s) 如果任意两个设备或节点见到了相同的一组更新或操作，即便它们接收操作的顺序完全不同，一旦双方看全了所有的操作，其文档状态就必然完全一致。 — Martin Kleppmann ## Mentioned Martin Kleppmann, Designing Data-Intensive Applications, Heidi Howard, Google Docs, Git, GitHub, Atom, Teletype, Riak, Isabelle, Automerge, Trellis, Trello, Pixel Pusher, Xavier Balon, WebRTC, Dat, Hypercore, Hypermerge, Redux, Immutable.js ## Video description Download the slides & audio at InfoQ: https://bit.ly/2P1IGJe Martin Kleppmann explores how to ensure data consistency in distributed systems, especially in systems that don't have an authoritative leader. He explains how to sync data between a phone and a laptop without sending it via a remote server. He also explores algorithms that allow several people to collaborate on a shared document, communicating via a peer-to-peer network. This presentation was recorded at QCon London 2018: https://bit.ly/2hxsoN1 #SoftwareArchitecture #DistributedSystems #CRDT #Consistency #InfoQ #QCon #QConLondon [Source](https://www.youtube.com/watch?v=B5NULPSiOGw)

[12:09] Martin Kleppmann: 即使只是在相隔 50 厘米的手机和笔记本电脑之间同步一些数据，数据仍然必须绕道弗吉尼亚州的数据中心，细想起来这相当荒唐。 [14:09] Martin Kleppmann: 共识协议所做的，是决定采纳其中一个提案并丢弃其他的——这在区块链场景中正是你想要的，但在文档协作场景中恰恰是你最不想要的。 [29:55] Martin Kleppmann: 如果任意两个设备或节点见到了相同的一组更新或操作，即便它们接收操作的顺序完全不同，一旦双方看全了所有的操作，其文档状态就必然完全一致。

[0:04] my name is Martin Chapman you might know [0:07] me from this book that I published about [0:09] a year ago called designing data [0:10] intensive applications this book is not [0:13] about CRD T's instead it's a very broad [0:16] overview of the architecture of [0:17] large-scale data systems and problems of [0:20] distributed systems what I'm going to [0:22] talk about today is a different area so [0:25] I am a researcher at the University of [0:28] Cambridge except today actually I am [0:31] formerly on strike you might have you [0:35] might have gathered I mean this [0:36] seriously does there's a dispute going [0:38] on at the moment at many UK universities [0:41] where the powers that be want to [0:43] essentially cut back our pension schemes [0:45] in a very radical and unjustified way [0:47] which amounts to a massive pay cut and [0:50] really is not justified so as part of [0:52] this I am on strike I'm still going to [0:54] give to talk to you because our we have [0:57] no problems with koukin it's our [0:59] university that we have a problem with [1:02] but just to say that I am giving this [1:04] talk as a private individual who happens [1:06] to be interested in distributed systems [1:08] rather than ok so let's talk about some [1:17] technical stuff so what I'd like to talk [1:20] about is collaborative applications and [1:22] so a classic example of this would be [1:24] Google Docs so there as you know you can [1:27] have several people who can all [1:29] collaborate in a document they can edit [1:31] the document at the same time without [1:33] having to email this back and forth [1:34] which is very convenient now what we [1:37] want in this kind of systems is that [1:40] eventually like even though several [1:41] people might be editing the document at [1:43] the same time they should all end up [1:46] with the same document on their screen [1:47] at the end so this is what we call a [1:49] convergence property everyone should end [1:52] up as they communicate having the same [1:54] state so if you were here this morning [1:57] Heidi Howard gave a great talk on [1:59] consensus which is also about getting [2:02] several nodes in the distributed system [2:04] to agree on something and so it looks [2:06] like superficially the problem that we [2:08] have here is kind of similar to [2:10] consensus so as we'll explain later in [2:13] this talk act [2:14] this is a very different kind of problem [2:16] even though it looks superficially [2:18] similar the properties that it has are [2:20] fundamentally different and comparing [2:22] those two will be an interesting part of [2:24] this talk okay so let's take a scenario [2:27] that is probably familiar to you this is [2:29] you a little blue stick figure who is [2:32] hacking on some code on your laptop and [2:34] you make some changes you edit some [2:36] source files you save them to your local [2:38] disk at some point you decide you're [2:40] ready to share this code with your [2:42] colleagues and so you commit it to your [2:44] favorite version control system and then [2:46] you maybe push it to a centralized [2:48] repository maybe to github or something [2:50] like that [2:51] some mechanism by which you can send [2:53] your commits to your co-workers and so [2:56] at the same time while you've been [2:58] editing the code maybe your colleague [3:00] who is this pink stick figure has also [3:03] been editing the code has also been [3:05] changing it maybe also making commits [3:06] and what you end up now with is that if [3:10] this colleague wants to also push their [3:12] changes to the server they will first [3:13] have to fetch that the commit that you [3:15] pushed and have to merge those together [3:17] and so as you've probably experienced [3:20] before this kind of merge it's [3:22] straightforward if you were editing two [3:24] different files because in that case get [3:26] just knows well two different files I'm [3:28] just going to merge them together those [3:30] changes are independent if one of you [3:32] changed the top of a file and the other [3:34] one changed the bottom of the same file [3:36] then that's probably still fine as well [3:38] because the changes are fine up in the [3:40] part a part in the file that git just [3:42] says okay I'll merge those automatically [3:44] but if you were editing actually the [3:46] same lines then you've got a merge [3:48] conflict that you need to resolve [3:50] manually so if we look at this kind of [3:53] system more abstractly you can say there [3:55] are a couple of nodes these might be [3:57] like your laptop and your phone or they [4:00] might be servers in a data center we [4:01] don't really care too much there's some [4:03] kind of computing nodes each of which [4:04] can store some data and when you want to [4:07] edit that data you make a change to your [4:09] local copy which might like in the case [4:11] of the source code is the source code [4:13] files living on your local hard disk you [4:16] change that and then at some point those [4:18] changes get communicated to anyone else [4:20] who also has a copy of that data so to [4:23] any other nodes and so while this is [4:25] going on maybe a purple user can [4:27] simultaneously [4:28] in making some change to their copy of [4:30] the data and they similarly will then [4:32] forward on those changes to the other [4:34] users and so whether these these changes [4:38] here are like wire gets pushed by this [4:40] kind of explicit operation or if you're [4:43] using Google Docs these kind of changes [4:45] are sent automatically continuously in [4:47] the background so in the case of Google [4:49] Docs this the local copy that you apply [4:52] the changes to is living in memory in [4:55] your web browser so in the tab that [4:57] you've opened the Google Doc in when you [4:59] type a letter and you change the [5:01] document that's change gets immediately [5:04] applied to your local copy of the [5:06] document so it doesn't wait for a [5:08] round-trip to the server before showing [5:10] the letter that you just typed on your [5:11] own screen because that would take too [5:13] long so what Google Docs does in that [5:15] case is it immediately applies the [5:17] change locally and then asynchronously [5:20] in the background which might take a few [5:22] seconds or whatever it sends on the meta [5:25] change to the server will then sir sends [5:27] on the change to anyone else who's got a [5:29] copy of that document open and so you [5:32] kind of get the same kind of property [5:35] that several people can make changes [5:36] independently without knowing about each [5:38] other's changes just like you get with [5:41] gits [5:41] get commits just on a shorter timescale [5:43] but you still have exactly the same [5:45] concurrency issue in particular this [5:49] concurrency issue becomes more obvious [5:51] if you have offline editing so in this [5:54] case you can think of this as a network [5:55] partition that is separating one of the [5:58] nodes from the rest of the system and so [6:00] the pink user might still be changing [6:03] the local copy their local copy of the [6:05] document but they can't send the changes [6:08] to any of the other users because they [6:09] are offline right now they don't have an [6:11] internet connection or because there's [6:13] some network disruption and so in this [6:15] case the changes will stay local to [6:18] their own machine and then only sometime [6:20] later once the network is restored those [6:22] changes will then be flushed but what we [6:25] still want in that case is for those [6:27] changes to be merged together so taking [6:30] this type of type of Google Docs again [6:31] as an example you can let's take the [6:34] state of the thing that is that we're [6:36] working on as a text document so this is [6:38] like just a sequence of characters which [6:41] currently [6:41] hello and so you have two users who can [6:44] currently update this document the pink [6:47] user adds the word the word world [6:49] before the exclamation mark and the blue [6:52] user adds a smiley face after the [6:54] exclamation mark and so now if this was [6:57] gits this would probably be a merge [6:59] conflict that you would have to resolve [7:01] manually but if you tried this kind of [7:03] thing in Google Docs it turns out that [7:05] actually Google Docs never prompts you [7:07] to to resolve a merge conflict it will [7:10] always just merge the changes [7:11] automatically based on what it thinks is [7:14] a sensible way of merging this and in [7:16] this case we can actually define quite a [7:18] sensible way of merging it because we [7:20] can say well the world clearly came [7:22] before the exclamation mark the smiley [7:24] face came after the exclamation mark so [7:26] we could just preserve both of those [7:27] insertions and so a final sensible final [7:30] merged state is hello world exclamation [7:32] mark smiley and this is in fact what [7:35] what Google Docs will do but we're not [7:38] limited to only text documents so let's [7:40] look at a different data type you could [7:41] use a set for example so a set is just [7:44] some unordered collection of elements [7:46] and you could have the read user maybe [7:49] removes the item B from the set so it [7:51] was previously a B removes B so only a [7:54] is left and concurrently while that is [7:57] happening [7:57] the purple user decides to add a new [7:59] element C to the set written here with [8:02] that set Union operator so the set then [8:05] is merged ABC so as those two changes [8:09] get propagated from one node to the [8:11] other again we can set just define what [8:14] we consider to be a sensible merged [8:16] outcome and in this case I'm going to [8:18] say well a was not touched by either [8:20] user so we're just going to leave a [8:21] there B was removed by all of the users [8:24] C was added by one of the users so we [8:26] want in the final state to contain C but [8:28] not B and so we just say a and C is a [8:31] sensible merged outcome in this case one [8:35] more example I consider a counter so [8:38] maybe like the number of likes on a [8:41] Facebook post or something like that [8:42] would be a counter that you can [8:44] increment and so here let's say we're [8:47] starting in the initial state where the [8:49] counter value is one and you have two [8:51] users who are both increment that [8:53] counter [8:54] so they both chained [8:55] the value from 1 to 2 now you could say [8:58] that's well both us design the same [9:00] state so we should just continue we [9:03] should just consider 2 to be the merged [9:05] final states but that would actually [9:07] lose information because here we know [9:10] from inspecting the chain the set of [9:13] changes that happened that actually to [9:15] increment operations happened so really [9:18] what we want is for both increment [9:20] operations to still take effect in the [9:22] final result so what we want is that the [9:25] final result is actually three because [9:26] we started in one and then one user [9:29] incremented it the other user [9:30] incremented it the order in which you do [9:32] those two increments doesn't matter but [9:34] the final value should be three so what [9:36] this is saying is that we need to [9:38] consider not just the state the value at [9:41] any one time because if we just compare [9:43] two and two they look the same but [9:45] actually we need to capture the sequence [9:47] of changes that were made to the data [9:49] and we apply those and that will allow [9:52] us to reach a sensible merged outcome [9:55] okay so this problem of people editing [9:59] stuff simultaneously and having to merge [10:00] it has been studied for a rather long [10:02] time and they are at a high level to [10:05] families of algorithms that were [10:07] developed one is operational [10:08] transformation which has been studied by [10:10] academics since the late 80s and which [10:13] is actually the foundation of Google [10:15] Docs so Google Docs internally uses an [10:17] operational transformation algorithm [10:20] however due to some problems that I'll [10:22] explain in a minute people got rather [10:24] frustrated with operational [10:26] transformation in the early 2000s and [10:28] then started this separate direction of [10:30] research called conflict-free replicated [10:33] data types or CRE T's for short and this [10:36] is SEO duties has been the focus of our [10:38] research so let me just give you a bit [10:40] of historical background because it's [10:42] kind of interesting and also some [10:45] motivation for why we wanted C Aditi's [10:47] so as I mentioned a whole bunch of [10:50] people across research community have [10:53] proposed operational transformation [10:55] algorithms [10:56] so the first ones in in the late 80s and [10:59] you know the paper reads quite nicely [11:01] and they kind of make sense and looks [11:03] plausible when you read it except you do [11:06] win then realize reading some more [11:07] papers [11:08] they're actually a few years after this [11:11] was published people discovered that [11:12] this application was this algorithm was [11:14] simply wrong so what I mean with wrong [11:16] is what these algorithms are supposed to [11:19] achieve is convergence that is everybody [11:21] ends up with the same document on their [11:23] screen at the end if no more edits are [11:25] happening however this algorithm did not [11:27] achieve convergence attacked there were [11:29] certain edge cases where certain edits [11:32] could happen concurrently where you [11:33] would end up permanently diverged so [11:36] these two different copies would be [11:38] permanently out of sync with each other [11:39] and never become consistent again so [11:42] that is kind of a problem so of course [11:44] people thought about this a bit harder [11:46] and proposed another algorithm [11:47] unfortunately a few years later that one [11:50] also turned out to be wrong it's had a [11:51] very similar bug and this story just [11:53] kept continuing so over the course of [11:56] about two decades all of these [11:58] algorithms were proposed and then of [12:00] only a few later few years later to [12:02] discover that it's wrong so a real [12:05] bloodbath of failed algorithms here we [12:09] did end up with a couple of algorithms [12:11] which are correct and in fact Google [12:13] Docs is based on one of those that is [12:14] not wrong but the particular property of [12:18] those remaining ones is that they [12:20] require a centralized server so they [12:23] restrict the communication flows in the [12:25] system so that if the think user here [12:28] changes something and the purple user [12:30] has changed it's something the changes [12:32] they make have to be exchanged via this [12:34] central server so it's not allowed for [12:37] them to have some kind of back channel [12:38] or some kind of other communication [12:40] paths on the side because if they had [12:42] that they would break the consumptions [12:44] of the algorithm and that it would no [12:46] longer achieve this convergence so this [12:50] is a severe restriction here all of the [12:52] communication has to go by a Google [12:54] server even if it's just like syncing [12:56] some data between your phone and your [12:58] laptop and they are like 50 centimeters [13:00] away from each other you still have to [13:02] go by a data center in Virginia or [13:04] whatever which is kind of ridiculous if [13:06] you think about it so what I'm [13:08] interested in is generalizing this model [13:11] so that actually you can just have any [13:12] communication topology in the system so [13:15] for example if the blue user here has [13:17] two devices or a phone and a laptop and [13:19] they want to synchronize some data [13:22] the pink use also has two devices well [13:24] they should just be able to synchronize [13:26] by our local network or whatever [13:28] connectivity they happen to have even if [13:31] they're actually not connected to the [13:32] internet right now so this kind of [13:36] communication pattern is simply won't [13:38] work in the google docs case because you [13:41] cannot safely have this communication [13:43] directly between devices without going [13:45] through the central server so I think [13:48] it's it would be really great if [13:50] applications can not depend on this [13:53] central server be more decentralized so [13:56] that you can actually just use whatever [13:57] network is available and then at some [13:59] point later if connectivity is [14:01] re-established then of course the node [14:04] should be able to synchronize again [14:05] using the Internet so this is a more [14:09] kind of decentralized pattern for [14:11] building applications and when I talk [14:13] about decentralization people inevitably [14:16] ask is that something to do with block [14:18] chains because because a lot of people [14:21] in the blockchain community who are [14:24] interested in building these these [14:26] systems without trust in a central [14:28] server also label their their work under [14:33] the heading of decentralization so I'm [14:36] personally not all that interested in [14:38] block chains I'm happy for other people [14:40] to work on it but let me just compare [14:43] the two briefly because it is such a [14:45] frequently asked question so as you [14:48] probably know a block chain consists of [14:50] some blocks of data each subsequent [14:53] block contains a hash of the previous [14:55] block a cryptographic hash and that [14:57] means then if you have a signature on [14:59] the last block you can follow through [15:00] the hashes and you're guaranteed the [15:01] integrity of this entire sequence of [15:04] blocks and then there might be some ugly [15:06] trees and stuff like that which allow [15:07] you to cryptographically prove that a [15:09] certain record appears in this chain and [15:12] so that's like the foundation for [15:14] Bitcoin transactions and such like [15:15] moreover what you have in most of these [15:18] blockchain protocols is some kind of [15:20] consensus protocol which decides what [15:23] the next block in the chain is going to [15:25] be and typically those are Byzantine [15:28] consensus protocols which just means [15:30] that they can tolerate some of the nodes [15:32] actually being actively malicious and [15:34] still [15:35] despite the presence of malicious nodes [15:37] this thing will agree on the next block [15:41] so this agreement property is quite [15:44] strong that you get in block chains so [15:46] in particular what the protocol is [15:49] supposed to guarantee is if there are no [15:51] Forks you have this linear sequence of [15:54] blocks it's a totally ordered sequence [15:56] and there's this decision process which [16:00] ensures that no conflicting transactions [16:02] get put into the same block so what this [16:04] means is if you're wanting to prevent a [16:08] user from spending the same coin twice [16:10] you have to make a decision as to [16:13] whether this transaction or that [16:15] transaction that they made using the [16:16] same coin is the valid one so what you [16:19] need here is consensus which if there [16:21] are several conflicting proposed [16:23] transactions [16:24] it picks one and that is what prevents [16:26] double spending in these [16:27] cryptocurrencies so that is the [16:30] fundamental abstraction of consensus [16:32] there are several proposed values [16:34] potentially conflicting and what the [16:36] consensus protocol does is to decide on [16:39] one of them and to throw away the others [16:41] and that is exactly what you want in the [16:43] case of a blockchain and it's exactly [16:45] what you don't want in the case of [16:47] collaborating on the document because if [16:50] you think about it if you make some [16:51] changes to a document and your colleague [16:53] makes some changes to the document what [16:55] a consensus protocol would do is to [16:57] choose to do the changes from one of you [16:59] and throw the other one away which is [17:01] actually what it would probably make you [17:03] a bit unhappy so what we want here for [17:06] collaboration protocols is to keep all [17:08] of the changes that were made and to [17:10] merge them in such a way that they [17:12] converge towards the same state so that [17:15] is what I mean with this thing look [17:17] superficially like consensus and is [17:19] really different because consensus is [17:20] fundamentally around this idea of [17:22] choosing one okay so back to these two [17:27] families of algorithms for achieving [17:29] convergence I'm going to talk briefly [17:30] about some research that we did on the [17:33] oddities so the oddities are also a [17:36] family of data structures which several [17:39] people on different nodes can update [17:41] concurrently and which will [17:43] automatically merge the changes together [17:44] very much like those examples I showed [17:46] earlier anders talked and [17:48] been used in a few practical systems so [17:50] for example the autumn text editor just [17:53] recently released a collaboration [17:55] feature that is built on CRD T's the [17:58] react database used them internally for [18:00] merging things and so on [18:02] so given this poor history of problems [18:06] with operational transformation [18:07] algorithms what we wanted to do is to be [18:10] really sure that we're not repeating the [18:12] same problems with CRD T's so we want to [18:15] prove formally mathematically that the [18:18] CR D T's really do converge that they [18:20] really do behave as they're supposed to [18:23] because as we saw with the problems with [18:25] the OT algorithms some of these [18:27] algorithms can be quite subtle and just [18:30] like thinking about it unform aliy you [18:32] might not be able to fully convince [18:34] yourself that it really under all [18:35] circumstances does converge so what we [18:38] did is we used Isabel which is a theorem [18:40] proving software which you can use to [18:44] write down formally the properties that [18:46] we want that you want and so we use this [18:49] software to write down several CR DT [18:51] algorithms so our GA is a is a text [18:53] editing C R DT [18:54] up set is a set and the counter is like [18:57] what I showed earlier and we can show [19:00] that they satisfy a consistency property [19:03] called strong eventual consistency which [19:05] in particular implies convergence and so [19:08] we can show that these data types [19:11] satisfy this consistency property under [19:13] certain assumptions but now how do we [19:16] know that those assumptions are valid we [19:18] now have a second layer of proof in [19:20] which we have a model of a network it's [19:22] a very unreliable network it's allowed [19:24] to throw away any number of messages [19:26] reorder messages and what we prove here [19:29] is that those assumptions under which [19:31] this strong eventual consistency holds [19:34] are satisfied in all possible executions [19:37] of this network model so no matter how [19:40] badly the network tries to mess things [19:42] up we can prove that these algorithms [19:44] will always satisfy the guarantees they [19:46] claim so unfortunately I don't have time [19:49] to talk about this theoretical work in [19:51] any more detail if you're interested [19:53] there's a URL there at the bottom of the [19:55] paper it's reasonably readable even if [19:57] you don't have prior experience in [19:58] formal verification of algorithms so do [20:01] have a look at [20:02] what I do want to spend a bit more time [20:04] talking about is Auto merge which is an [20:07] application an implementation of these [20:10] ideas that we've been working on this is [20:12] an open source library in JavaScript in [20:15] principle you could implement it in any [20:16] language but guess JavaScript is very [20:19] portable across many platforms which is [20:21] why we're using that at the moment and [20:23] you can think of this as a data model [20:27] layer or data structure library on top [20:30] of which you can build collaborative [20:31] applications so what it gives you is a [20:35] abstraction that looks very much like [20:37] JSON and you can modify this JSON [20:41] document and use that to build [20:43] applications on top of it so I'll show [20:44] you some examples of prototype [20:46] applications that we built using this [20:48] the first one is called trellis it's a [20:51] clone of Trello the the popular project [20:54] management tool looks like this [20:55] so just like Trello you have columns and [20:59] you have cards in those columns and you [21:01] can drag and drop the cards between [21:02] columns this year's a superhero [21:05] recruiting initiative that we've used as [21:07] an example and you can assign columns to [21:11] people and you can leave comments on [21:12] cars and so on all the typical stuff you [21:14] would expect the cool thing with this is [21:17] that it's implemented without any [21:19] servers at all so we are able to do this [21:22] based on a peer-to-peer networking model [21:24] using WebRTC which is normally what [21:27] enables like video calls in your web [21:28] browser but you can use it for [21:30] transferring data as well in particular [21:32] we can transfer them edits made to a C R [21:35] DT over something like WebRTC and as a [21:38] bit of use interface here on the right [21:39] hand side for managing that network and [21:42] moreover what it does it keeps track of [21:44] all of the changes that happened so [21:46] whenever you move a card around or you [21:49] update a card or whatever it actually [21:51] appears in this log of changes here and [21:53] on the bottom right hand side so that's [21:55] just one example app that we built on [21:57] top of auto mode another example is an [22:01] app we call pixel pusher which is quite [22:04] a fun one it's a collaborative pixel art [22:07] editor so like pixel art is kind of sort [22:10] of retro gaming aesthetic where you try [22:14] to make [22:15] pictures consisting from just this grid [22:17] of a fairly small number of pixels and [22:19] people like make really cute animations [22:21] and stuff like that with this so we took [22:25] this off-the-shelf [22:26] open-source implementation by xavier [22:29] balan i think is his name and this was [22:33] just a user app running in your web [22:35] browser and we made it turned it into a [22:38] collaborative app by building on top of [22:40] auto merge so it looks like this pixel [22:43] pushes our variant and what we wanted to [22:46] experiment with this here is not just [22:48] like the straightforward collaboration [22:49] where one user makes a change it shows [22:51] up on another user's device but also [22:54] wanted to think about like for example [22:56] with git you get pull requests which is [22:58] a mechanism by which a user can suggest [23:01] some changes and then the maintainer of [23:04] a repository can accept or not accept or [23:06] maybe accept with some changes or with [23:08] Google Docs there's this future for [23:10] suggesting changes and making comments [23:12] and so we wanted to explore a bit like [23:15] what would a similar kind of suggesting [23:17] changes like user interface look like [23:19] for a collaborative pixel art editor so [23:22] then in the top right hand side there's [23:24] this bit of user interface where you can [23:26] actually see there several different [23:27] versions of the document so the base [23:29] document contains just the eyeballs but [23:31] then there's one variant that is like a [23:33] potato man and so another variant and [23:36] you can switch back and forth between [23:37] those variants any user can create our [23:40] own copy and then another user if they [23:43] like it can merge that into their local [23:45] kind of like a pull request but just [23:47] with a very lightweight user interface [23:49] so these kind of things are enabled [23:52] simply by keeping track of the history [23:54] of all of the changes that are done and [23:56] that is what autumn urge does internally [23:59] so as I said Auto merge is this kind of [24:02] data structure abstraction on top of [24:04] which you can build applications what [24:07] emerged does not itself have a [24:08] networking layer so it's just a piece of [24:11] JavaScript that runs in one process it [24:13] doesn't prescribe a way how that [24:15] communicates with copies of the document [24:17] running on other devices [24:19] so we've now also been experimenting [24:21] with different network layers that you [24:23] can plug underneath what emerge so as I [24:25] mentioned earlier trellis is built on [24:27] top of web RTC [24:28] peer-to-peer communication using a [24:30] library that we called MPL the pixel [24:35] pusher pixel art editor is actually [24:37] built on a different networking layout [24:38] because we were just experimenting with [24:40] different layers this one taken from the [24:42] DAT project so they are about a peer to [24:44] peer synchronization of datasets it's a [24:46] really interesting project so we were [24:49] able to build on top of that using their [24:51] long abstraction which actually worked [24:53] really nicely as well so that's library [24:55] called hyper merge which makes the [24:57] connection between hyper call and Auto [24:59] merge but if you like you can just send [25:02] updates via server via WebSockets or [25:05] what have you like really so autumn urge [25:07] doesn't prescribe any particular network [25:09] protocol for using here so let's look a [25:12] bit more at the kinds of data structures [25:14] you can use to build these collaborative [25:17] applications so as I said Auto merge [25:19] gives you this kind of JSON like [25:20] abstraction and you can use JSON to [25:22] implement for example a to-do lists so a [25:25] to-do list consists on some fairly [25:28] simple structures so in particular JSON [25:31] has two ways of combining things [25:34] together one is a list which is just an [25:36] like an ordered sequence of things and [25:39] one and the other is maps and so maps [25:42] are just like a dictionary that map's a [25:44] key to some value and the value can be [25:48] again a map or it could be a nested [25:50] sequence so you can nest these lists and [25:52] maps inside each other [25:53] arbitrarily and when you have this [25:55] structure now you can modify it in [25:57] several ways so for example you can [25:59] change a value that appears somewhere so [26:01] overwrite one primitive with another so [26:04] setting and an item that's done like [26:06] clicking the checkbox that this item is [26:08] done would just trigger this flag here [26:11] probably another thing you might do is [26:13] edit a string that appears in here or [26:15] you might insert a new item into a list [26:18] between some existing items or you might [26:21] like insert a new key into a map or you [26:22] might remove things from this of course [26:24] so you can do any sorts of editing [26:26] operations on this data structure and in [26:30] auto merge it looks like this so this is [26:33] a some example JavaScript code of how [26:35] you do this in auto mode so auto mode [26:38] uses an immutable state object that is [26:41] the [26:42] State here is the current state of your [26:45] data and that is never modified in place [26:47] instead if you want to change it you [26:49] call this water merged or changed [26:51] function you pass in the current state [26:53] and you get back a new object which is a [26:56] new state in which steps new item has [26:58] been reflected so it's very much like [27:00] immutable J yes if you've used that kind [27:03] of things it's a very similar way of [27:04] thinking except what we wanted to try [27:06] here is to keep a sort of familiar [27:08] imperative programming model and so what [27:11] we have here is you pass in this one [27:13] thing you do is you can provide a kind [27:15] of like a commit message we call it [27:16] which is just arbitrary string it's not [27:19] interpreted but it is stored alongside [27:21] the editing history and so if you want [27:23] to see what changes happened it's kind [27:25] of nice to provide that sort of human [27:27] readable explanation of the change and [27:30] then there's this callback here where we [27:33] have this document object which is [27:35] mutable just within the period of this [27:37] callback and any changes that you make [27:39] within here are intercepted in [27:41] JavaScript using a proxy object so here [27:43] for example this to do is not push [27:45] pushes the JavaScript or method for [27:48] appending a new item to an array so it's [27:50] here using the dock - duze doc dot - [27:53] duze as an array appending this new item [27:56] to the end of it and so these are just [27:59] kind of standard javascript methods you [28:01] can use assignment or whatever you like [28:03] as well and autumn urge captures any of [28:06] those changes and internally stores it [28:09] as a log of operations so you don't [28:11] normally have to deal with this [28:12] operation log I'm just explaining it to [28:15] you so you have a bit of an idea of [28:16] what's going on under the hood and so [28:18] internally this this one command here of [28:21] adding a new to-do item gets broken down [28:24] into these lots of little micro [28:25] operations so what we do is we we create [28:28] a new empty map object then we set the [28:31] title key of that map object we set the [28:34] donkey of that map object then we insert [28:37] a place it create a new placeholder [28:40] position in a list which is where we [28:42] want to insert that to-do item and then [28:44] we link that object we created into the [28:46] list so fortunately you don't have to [28:48] ever write these kind of operations [28:49] yourself that would get extremely [28:51] tedious but this is just to an idea of [28:53] what's going on internally [28:55] and now water merge simply remembers all [28:59] of these operations forever and so this [29:01] does use some storage but our basically [29:03] of thinking there is that well gets if [29:06] you ever get repository and you don't do [29:07] a shallow clone actually the repository [29:09] contains all of the commits that ever [29:11] happened in that repository and so if [29:13] gifts can keep all history forever then [29:15] so can we [29:16] and if we need to do compaction things [29:18] in the future we'll solve that in the [29:20] future but for now we're just storing [29:21] everything and it's working surprisingly [29:23] well actually and keeping all of the [29:26] operations where ever has some really [29:28] nice properties like we can do time [29:30] travel so which sounds amazing it's [29:33] actually really simple because we have [29:35] all of the changes that happened we can [29:37] look at past states of the document and [29:40] so you can just ask for the history and [29:42] it'll just give you a list of states [29:44] that the document went through since the [29:46] began in beginning of time and it'll [29:50] keep the commit message that you attach [29:51] to to any changes there there's human [29:53] readable like add the to-do item and [29:55] give you a snapshot of what the document [29:57] was at that point in time and so auto [30:00] mode is able to do this efficiently by [30:02] just selecting the subset of operations [30:04] at any given moment and figuring out [30:05] from those operations what the document [30:08] looked like at that time okay so we were [30:12] talking about collaboration so let's [30:13] talk about some concurrent changes [30:15] because that's where the conflict [30:17] resolution comes in so let's say that [30:19] our starting point is two users both [30:23] have this to-do lists can containing a [30:26] single item which is watering the plants [30:28] and it is not yet done and so two users [30:31] now concurrently update this to-do list [30:33] like maybe like one of them is me and [30:35] the other one is my wife and we're [30:36] sharing this to-do list between our two [30:38] phones so for example maybe I add buying [30:42] the milk which is done false and my wife [30:44] says our she's watered the plants now so [30:46] she marks that item as done and so these [30:48] are two independent changes that happen [30:50] maybe while the devices are offline so [30:52] now we want to merge them together and [30:55] so firstly we immediately apply any [30:58] change to your local copy of the data of [31:01] course that's what we want because even [31:03] if you don't have an internet connection [31:04] you should still be able to update the [31:06] data obviously but then at some [31:09] later the network comes back and we're [31:11] able to communicate these changes from [31:13] one device to the other and so at that [31:16] point then Auto merge will figure out [31:17] that well changes to two different [31:19] objects we can merge these two together [31:21] cleanly so setting done to true for the [31:24] watering the plants get supplied to the [31:26] left copy and inserting the new item of [31:29] buying milk with done falls on the right [31:31] hand side they both get applied and so [31:33] in this case the merger is quite [31:36] straightforward and what auto merge [31:38] guarantees you this is the fundamental [31:40] property of CR DTS is convergence and [31:43] that is more formally defined if any two [31:46] devices any two nodes have seen the same [31:49] set of updates or the same set of [31:51] operations even if they might have seen [31:54] those operations in a different order as [31:56] soon as they've seen the same set of [31:58] operations then the state of the [32:00] document will also be the same this is a [32:02] really nice property to have because it [32:04] means we're not depending on like who [32:06] saw which operation in which order we [32:08] just have this simple property that once [32:10] the data has been exchanged everyone's [32:12] in the same state now there are some [32:15] edge cases in which there are conflicts [32:17] that are not neatly result abour and [32:19] this is really the only one actually [32:21] that we can't sensibly resolve [32:23] automatically which is the same field or [32:26] the same item in the list [32:27] it's overwritten with two different [32:29] values and so like that's fundamentally [32:33] the the most basic type of conflict and [32:35] in this case you know it's not really [32:37] defined is it better to buy soymilk or [32:39] better to buy almond milk you know that [32:41] could be a subject of debate and auto [32:44] merge is not opinionated on whether soy [32:46] or almond milk milk is better [32:48] so what auto mage merge does is firstly [32:51] it picks one of them arbitrarily but [32:54] deterministically as the default value [32:56] and so if you just like look at the [32:59] document without inspecting conflict [33:02] it'll just pick one of the two that's [33:04] about the best we can do but it keeps [33:06] the other one in the side object here [33:09] called underscore conflicts and it will [33:11] tell you hey you know there was a [33:13] conflict for the field title and this [33:15] other nodes node ID one two three four [33:18] set the value to buy almond milk so even [33:20] though we've got here buying soy milk as [33:22] default value there's also this other [33:24] one and so then it's up to the user [33:26] interface do you want to show like both [33:27] conflicting values and let the user [33:29] choose one you can implement that kind [33:32] of manual conflict resolution if you [33:34] need to but this is actually this [33:36] assignment to the same field is the only [33:39] case in which that manual conflict [33:41] resolution has to happen so if it's text [33:44] editing for example let's say we've got [33:47] an document that says hey guys and we [33:49] may want to make it more gender-neutral [33:51] so maybe one user changes guys to [33:53] everyone the other user concurrently [33:55] changes guys to folks and so you could [33:59] say like how do we handle this kind of [34:01] conflict and what auto modes does for [34:04] this is in fact the same as what Google [34:06] Docs would do in the same situation [34:08] which is it thinks well ok guys was [34:12] deleted on both replicas so delete it [34:15] twice is the same as deleted once so [34:17] guys is gone everyone was inserted on [34:20] the left-hand side folks was inserted on [34:22] the right-hand side if two things were [34:24] inserted we're just going to keep both [34:26] of them and we're just going to put them [34:28] in an arbitrary order but we're going to [34:29] make sure that the order is the same on [34:31] all of the replicas so ensure that [34:33] everyone sees either [34:34] hey everyone folks or hey folks everyone [34:37] I hope those is a valid merged outcome [34:41] but which of the two gets chosen is [34:43] non-deterministic sorry it's it's random [34:47] but deterministic it's been chosen based [34:49] on the unique identifiers of the nodes [34:51] so like this is fundamentally the [34:54] properties you get you might think it's [34:57] not ideal maybe you do want more manual [34:59] conflict resolution the basis on which [35:02] we are going here is that actually like [35:04] Google Docs does this and millions of [35:05] people use Google Docs so it seems to be [35:07] fine [35:08] in many cases maybe what we want is kind [35:11] of like an advisory conflict like notion [35:15] that says that maybe if some edits [35:18] occurred within like 20 characters of [35:20] each other or whatever defines some kind [35:22] of threshold that we show you a little [35:25] note to the user saying by the way there [35:27] were some edits close together here you [35:28] might want to check if the most outcome [35:30] is like a valid English sentence or not [35:32] we can't figure that out [35:35] but I think that's about as much [35:37] conflict resolution as you might need [35:39] here so I'd like to show you just [35:42] briefly before we wrap up here held the [35:45] algorithm behind this works because I [35:47] think it's kind of neat and so although [35:48] you don't need to implement this kind of [35:50] algorithm yourself it's kind of cool to [35:51] see what happens here so let's take as [35:54] example a document consisting of the [35:56] letters H e l and o and we have two [36:00] concurrent edits happening to this [36:02] document so one user adds a second L to [36:04] make it reread hello and the user the [36:07] other user the purple goos on the right [36:09] adds an exclamation mark at the end so [36:12] the way the CR DT works is it gives each [36:15] character in the document a unique [36:17] identifier and it has a particular [36:19] scheme for creating those identifiers [36:21] and that is it consists of a number [36:25] which is just like a counter and the a [36:28] and B here is the name of the node that [36:31] created this particular list element so [36:34] node a on the Left creates new list [36:37] elements with a and node B here creates [36:40] a new LMS tellement for B so using their [36:43] name no to name me and so because each [36:47] node increments the counter for every [36:49] operation is generated and two different [36:52] nodes will have different names so that [36:53] makes these identify as unique across [36:56] all of the nodes and so now when when [37:00] these nodes exchange data might be viola [37:03] server or any kind of network doesn't [37:04] really matter what they exchange is [37:06] these operations which say insert a new [37:09] list element new character L with ID for [37:13] a so that's the new the new ID given to [37:15] this new element after the existing list [37:18] element with ID to a so this is [37:20] important it doesn't say like insert at [37:23] position 15 because position 15 might [37:26] change if somebody inserts or deletes [37:27] something before position 15 so instead [37:30] we use these identifiers as a way of [37:32] reliably pointing to a particular [37:35] position in the sequence and the other [37:39] user similarly creates this operation [37:41] that says insert exclamation mark with [37:43] ID for be after the existing element 3 a [37:46] which is the O and [37:48] these messages simply get forwarded on [37:50] to the to users and they each apply [37:54] exactly what what you would expect so [37:56] the purple one here looks for the [37:59] character with ID 3a and puts the [38:02] exclamation mark with 4p after the 3a so [38:04] it doesn't matter that the position has [38:06] shifted along by 1 this unique [38:08] identifier still clearly identifies the [38:10] position to where to insert and we just [38:13] need this doesn't rely on any ordering [38:15] guarantees particularly so this can just [38:17] go through any kind of network so you [38:20] might realize that I haven't told you [38:22] about one of their issues which is what [38:25] happens if two people insert in the same [38:27] place in the same document and so this [38:30] one requires a little bit more [38:32] explanation so imagine we have a [38:34] document that reads ABC and on the left [38:39] hand side the user adds XY between the a [38:42] and the B so it reads a XY BC and [38:45] independently of that on the purple side [38:48] the letters P and Q get added similarly [38:52] between a and B and so what we want to [38:55] ensure is that still here in this case [38:58] everybody ends up in the same state at [39:01] the end ok and so for this I'm now going [39:06] to start with sending that that [39:09] insertion of P over from the right hand [39:10] side to the left hand side this works as [39:12] you would expect so insert p with ID 4 [39:16] be after 1a 1a is still there's the [39:18] letter A so it puts the pede directly [39:21] after a but before the X and then [39:23] similarly the Q comes across insert Q [39:26] with ID 5b after 4 B so for P is there [39:30] bits there letter P that we just [39:32] inserted so it puts the Q after the P [39:34] okay so that's one direction sorted [39:37] we've got a PQ x y BC now we need to [39:41] ensure that if the message is going the [39:42] opposite direction we end up in the same [39:44] state and if we just do this naively so [39:47] just applying say insert for a after one [39:50] a it's actually going to end up with [39:52] this in the in the opposite order on the [39:54] right hand side so here we need to be a [39:56] little bit more clever so we need to [39:59] ensure that the X ends up after the Q [40:02] so even though the the operation for [40:05] inserting X says insert after 1a what we [40:09] need to do is actually shift along and [40:11] put it not directly after 1a but after [40:14] 5b which it's a Q and so for that we're [40:17] going to use the following rule when a [40:21] new insertion comes in so in this case [40:23] the insertion of for a comes in after 1a [40:26] first of all we set to our starting [40:29] position which is 1a so we want to [40:30] insert after 1a and now we're going to [40:33] compare the ID of the new incoming [40:36] operation to the ID of the next element [40:39] in the list and in this case at the next [40:41] element is the is 4b that's the P and so [40:46] what we're going to do now is if the ID [40:48] of the incoming operation is less than [40:51] the ID of the next element in the list [40:53] we're going to skip over that element [40:55] and move on so move one further to the [40:58] right and we'll repeat the same thing so [41:00] now we look at the next next element in [41:03] the list which is Q Q has an ID of 5b 5b [41:07] is also greater than 4 a so we're going [41:09] to skip over it as well so apply the [41:11] same rule skip over any of the elements [41:14] that have a greater ID than the one [41:17] we're inserting and so then we've [41:20] skipped over Q now the next next element [41:23] to look at is the letter B which has an [41:25] ID of 2a 2a is less than 4 a so now we [41:29] stop the skipping and this is where we [41:31] insert the letter X and so this rule it [41:36] does actually work it takes a little bit [41:38] of convincing and this is why we did all [41:40] of that for more proof stuff because [41:42] it's not entirely obvious immediately [41:43] that this actually does the right thing [41:45] but it turns out that it does actually [41:47] always do the right thing and now [41:49] finally for the insertion of y this one [41:51] is easy again because here now we have [41:53] just insert y with ID 5 a after ID for a [41:57] for a is that X that we've really placed [41:59] in the list so now we can just put it [42:02] directly after the X just to show you [42:05] that the skipping doesn't happen in any [42:07] other circumstances so this 5a is not [42:09] going to skip over 2a because 2a is less [42:10] than 5 a on the other side here this [42:13] insertion of p4 [42:15] will not skip over the X here because 4 [42:19] P is greater than 4 a so for P you will [42:22] not skip over for a ok so this whole [42:26] thing is just an example of how the CR [42:28] DTS work if you want to play around with [42:30] this stuff what emerges open source and [42:32] liberally licensed and it would be [42:34] really great if anyone wants to try and [42:36] just prototype some applications on top [42:38] of it I'll tell you this is research [42:40] code it's not production ready we're not [42:42] pretending that it's perfect in all [42:44] circumstances but it does seem to be [42:46] working reasonably well we were able to [42:48] build some non-trivial applications on [42:50] top of it so maybe you will be able to [42:52] as well thanks to especially the hyper [42:56] core from the doc project which we used [42:58] for the networking in our last work if [43:01] you're interested in the formal [43:02] verification there's a link to the paper [43:04] this is this work is based on our [43:06] earlier work on a Jason CR DT which is [43:09] this penultimate paper here on the list [43:11] except the algorithm we use in auto mode [43:14] is actually a bit different from what is [43:15] in the paper so we need to write an [43:17] updated version of that with the latest [43:19] algorithm but we haven't got around to [43:20] that yet I'm afraid but there is a like [43:23] a mock down page on the auto mode [43:25] repository telling you about the [43:26] internals if you're interested in that [43:29] and finally this book which as I said [43:31] it's not about CRD T's but might also be [43:33] interesting to anyone thank you very [43:35] much [43:37] [Applause]