Ariaki
/
返回博客

2026.10.27

阅读进度的冲突框弹了 170 次，106 次的对手是我自己：一个只有我在用的阅读器，同步逻辑能错几处？

我自己写的网页阅读器在手机和平板之间同步进度，冲突记录里 62% 是同一台设备在跟自己冲突。我把同步规则写成 TLA+ 模型，TLC 把 8 条规则全部打穿，最快的不到一秒，真代码复现出 7 个 bug，另有 2 条是模型自己的错。这篇给两个能自己算的数：冲突记录里的自冲突比例，和「晚到的旧写入能赢」的时间窗；再讲怎么看一份「0 违规」的验证结果，我修完之后就有一条是空通过。

形式化验证TLA+同步方法论

我自己写了个网页阅读器，手机和平板上都装着，读到哪儿两边同步。

它的数据库里，冲突框一共被处理过 170 次。其中 106 次，冲突发生前的上一次写入，来自同一台设备。

也就是说，62% 的「冲突」，是一台设备在跟它自己吵架。

这个阅读器从头到尾只有我一个人在用，两台设备。我原本以为这种规模的同步，出错也就是偶尔的边角。后来拿形式化验证工具跑了一遍，8 条我写下的规则，全部能找到反例，最快的不到一秒。

想直接拿两个公式的看第 2 章和第 5 章；想知道怎么看一份「验证通过」的报告，看第 6 章，我修完之后自己就有一条是空通过。

1. 这个阅读器是怎么同步的

规则不复杂，我先照代码念一遍：

  • 服务端每本书存一行进度，带一个版本号。客户端写的时候报上「我手里的版本是几」，对上了才写，版本 +1；对不上就回 409，把服务端现在的值给你，前端弹冲突框
  • 翻页后等 1.2 秒再推，翻得快就合并成一次。这个等待叫 debounce
  • 切到后台或者锁屏，用浏览器的 sendBeacon 把当前位置甩出去。beacon 的特点是发出去就不管了，响应读不到
  • 断网时进度先存进本地的离线队列，一本书一条，有网再推
  • 另外每次写成功，顺手双写一份到家里 NAS 上的 KOReader 同步服务（KOSync），这样墨水屏阅读器也能跟上。每次打开书时反过来检查一下 KOSync 有没有更新的进度，有就拉回来

每一条单看都挺合理。问题都出在它们凑到一起的时候。

2. 跟自己吵架的那 106 次

先说那 62% 是怎么来的。

翻一页，debounce 开始倒数 1.2 秒。如果 1.2 秒之内锁了屏，beacon 先把位置写上去了，服务端版本从 v1 变成 v2。可 beacon 读不到响应，手机手里的版本号还停在 v1。

解锁之后，那个还挂着的 debounce 照常发出去，报的版本是 v1。服务端一看，现在是 v2，409。冲突框弹出来，框里「云端」那一栏写的设备名，就是这台手机自己。

我用真代码在浏览器里复现了一遍，下面是输出摘录：

1) phone 读到 40% → { f: 0.4011, v: 1 }
2) 锁屏 beacon 后 → { f: 0.4521, v: 2 }
3) 回到前台: 冲突框出现= true  框里"云端"标签= 云端（iOS Safari）

翻完一页马上锁屏，这个动作我每天都在做。

这里能拿走的第一个数，任何带版本号同步的东西都能算：

自冲突比例 = 冲突前一次写入与冲突方是同一设备的次数 ÷ 冲突总次数
我的：106 ÷ 170 ≈ 62%

这个比例高，说明你的冲突检测在抓自己。正常的多设备冲突应该发生在设备切换的时候，同一台设备连续两次写入之间本来不该冲突。

有一点得先说清楚：上面那个锁屏机制能解释这个形状，但 106 条我没有逐条归因。里面可能混着别的路径，比如下面第 4 章那条冲突后自动拿版本号的 bug。

3. 把规则写成模型，TLC 跑了不到一秒

TLA+ 是一种把系统写成「状态 + 动作」的语言，TLC 是配套的检查器：它会把所有动作在所有顺序下的组合挨个走一遍，看有没有哪条路走到了你说不允许的状态。说白了就是暴力穷举时序。

我把两台设备、服务端、离线队列、KOSync、在途的网络请求全写了进去，每个动作旁边标上对应的代码行号。规模压得很小：两台设备，进度只有三档，每台最多读两次、开关书一次、断网两次。

然后写了 8 条「不许发生」，比如：

  • 一台设备没见过更远的进度，却把服务端写回了更早的位置
  • 离线队列里较新的条目被旧的覆盖或误删
  • 关书时最后的位置既没上服务端也没进离线队列
  • 跟自己上一次的写入冲突

每条单独跑。结果 8 条全部违反。我又把其中一条按来源拆成三条子规则，两条也违反，合计 10 条违规：

规则 走过的状态数 反例步数 耗时
跟自己冲突 567 4 不到 1 s
关书丢位置 494 4 不到 1 s
写回更早的位置 25,466 7 不到 1 s
离线队列被覆盖 367,580 8 1 s
KOSync 把进度拉回旧值 2,024,203 9 3 s

最短的反例只有 4 步。拿「跟自己冲突」那条说，大致就是翻页、锁屏、解锁、推送。我自己每天都在走这 4 步，只是从来没意识到它是个反例。

装起来有两个小坑。TLC 要 Java 11 以上，我机器上只有 8，装了个便携版 JDK 21。另外它的状态目录很能吃盘，跑大一点的规则一轮就写到 7G 左右，跑完自己删，但峰值能把一块快满的盘顶穿。我那天根分区见底，它就是帮凶之一。

4. 10 条反例，7 个是真的

TLC 给的是模型的反例。模型是我写的，我写错了它照样报。所以每一条都得拿真代码再走一遍。

我搭了一个小台子：服务端那段同步代码按标记原样切出来，逻辑一行不手抄；KOSync 换成本地假的一个，线格式一样；前端直接用仓库源码起；Playwright 开两个互相隔离的浏览器上下文当两台设备，真的去翻页、断网、切后台。下面的输出都是摘录，设备名我简化过。

10 条违规按根因去重，剩 9 个。最后 7 个复现了，2 个没复现。

最狠的两个：

冲突之后，下一次写入直接覆盖别人。 收到 409 时，前端顺手把自己的版本号改成了服务端的。冲突框弹着，你还没选，又翻了一页，这次版本号对上了，写成功。平板上读到的 60%，被手机的 30.6% 盖掉：

5) phone 在 30% 处翻一页 → 冲突框= true  row { f: 0.6008, v: 4, dev: 'tablet' }
6) phone 再翻一页（没碰冲突框）→ { f: 0.3059, v: 5, dev: 'phone' }

冲突框是个弹窗，可键盘、手柄翻页根本不理它。

离线读的那一截，重新开书时被旧值盖掉。 地铁里离线从 30% 读到 50%，出站有网，打开书。代码先拉服务端（30%），跳过去，然后才推离线队列（50%）。服务端是 50% 了，屏幕还停在 30%。这时候翻一页，30.4% 写上去，50% 没了：

4) 重新打开书: 屏幕显示 30.1 % ; row { f: 0.5008, v: 2 }
5) 在屏幕位置翻一页: 屏幕 30.4 % ; row { f: 0.3036, v: 3 }

没复现的那 2 条，是模型比代码宽。模型里我允许离线也能开书，TLC 顺着这条路找出了「离线开书从头开始」，另一条的最短路径也踩在离线开书上。真代码离线时连书架都加载不出来，直接显示「书不存在」，这条路根本走不到。这个 bug 不存在，可它顺带告诉我：离线阅读只在「开着书时掉线」这一种情况下成立。

9 个里 7 真 2 假。我一开始挺想把 10 条全报成 bug 的，数字好看。

5. 跨时钟比较：我以为怕的是时钟漂移

KOSync 那条，我原来以为毛病在时钟上。

回灌的判据是这样的：KOSync 上那条记录的时间戳，比服务端这行的更新时间晚 1.5 秒以上，并且不是同一台设备写的，就当成「别处有更新」拉回来。KOSync 的时间戳是 NAS 的钟，服务端是另一台机器的钟，两个钟在比。

我第一反应是测时钟偏差，结果两边差在 ±20 毫秒以内，1.5 秒的余量绰绰有余。

可它照样出事。复现用的是这个顺序：

1) phone PUT 30%        → 服务端 v1，双写 KOSync（这次在 NAS 上卡了 4 秒）
2) tablet PUT 60%       → 服务端 v2，双写 KOSync 先落盘
3) phone 那次旧写入后到 → KOSync 变成 30%，时间戳反而是最新的
4) 任一设备打开书       → {"fraction":0.3,"version":3,"deviceId":"phone"}

旧写入后落盘，带的就是新时间戳。这里一个钟都没漂，只是两个请求的到达顺序反了。

这个窗口有多大，按代码里两个常数就能算。设手机那次双写在路上走了 d 秒，平板在手机之后 g 秒写入。回灌会发生，要求旧写入落盘的时刻比平板那次写入晚 1.5 秒以上：

d > g + 1.5
d 最多到双写的超时，5 秒
⇒ 两台设备先后写入的间隔 g < 5 − 1.5 = 3.5 秒，就有可能被拉回旧值

推广一下：

回退窗口 = 写入链路允许的最大延迟 − 时间戳比较的安全余量

余量比延迟上限小，这个窗口就一定存在，跟钟准不准无关。3.5 秒是按常数推出来的上限。NAS 平时多久能响应完，我没测，所以触发概率我说不出来，只能说它不是零。

修法也没去调余量：服务端自己推到 KOSync 的值，回来时一律不回灌，只回灌真正的墨水屏阅读器写的；双写按书排队，只推最新一次。

6. 怎么看一份「0 违规」

这一章是给读别人验证报告的时候用的。我自己修完以后，就差点被自己的「通过」骗了。

修复做完，TLC 再跑修好的模型，7 条规则各跑 300 秒，每条走了四千多万个不同状态，没有反例。真代码那边，一个检查器 28 项全过。

听起来稳了。三个地方要拆开看：

跑完没有。 300 秒是我设的上限，到点就停，状态空间没穷尽。修复前有一条规则我跑了 15 分钟、生成了 2.7 亿个状态没找到反例，也是我手动停的。TLC 没跑完时报 0 违规，意思就是「这么多状态里没撞见」，跟证明差得远。

那条路径在模型里走得到吗。 修完以后，「KOSync 把进度拉回旧值」这条在模型里是通过的。我回头查可达性才发现，修复加了「自己推过去的值不回灌」，而模型里的两台设备全是我自己的阅读器，没有一台墨水屏，回灌那段逻辑在模型里一次都没被执行过。这条规则是空通过：它检查的那条路根本没人走。真正的墨水屏回灌，最后是靠一个真代码用例兜住的。

检查器能不能分出好坏。 跑这 28 项的同时，我把同一个检查器喂给修复前的代码，报 10 项 FAIL。这一步不做，28/28 什么都说明不了，一个永远报绿的检查器也能 28/28。

所以看到「形式化验证通过」，先问三句：跑完了还是到点停的；它检查的那条路径，在模型里有没有被走到过；同一套判据喂给已知有 bug 的版本，会不会报红。三句里任何一句答不上来，这个「通过」先打个问号。

7. 这次没做到的

  • 模型规模很小：2 台设备、3 档进度、每台最多读 2 次。更长的序列里有没有别的东西，不知道
  • 时钟偏差只建模了 0。偏差超过 1.5 秒时，KOSync 还有一条「推送丢失 + 漂移」的路，没探索也没复现。实测偏差 ±20 毫秒，暂时不急
  • 锁屏是拿 Playwright 的 visibilitychange 模拟的，断网是 setOffline。真 iOS Safari 冻结后台页面的行为只会更糟，不会更好
  • KOSync 那条用的是我注入的 4 秒延迟。NAS 的真实延迟分布没测，所以第 5 章只给得出窗口上限，给不出概率
  • 106 次自冲突没有逐条归因到具体机制
  • 同一台设备开多个标签页、阅读器的独占会话和冲突交织的全部时序，都没建模

8. 下次再写同步逻辑，按这个顺序过一遍

  1. 先翻一下冲突记录，算自冲突比例。高于一半，先别查多设备，先查自己的 debounce、beacon 和版本号什么时候前进
  2. 任何「发出去不看响应」的写入，都要问：它成功之后，本地的版本号谁来更新
  3. 收到冲突时，别顺手采用服务端版本号。冲突没解决之前，后续写入要停
  4. 开书、恢复网络这类时刻，先推本地积压，再拉远端
  5. 有跨机器时间戳比较的地方，把「最大延迟 − 安全余量」算出来。大于零，就别靠时间戳判谁新
  6. 把规则写成 TLA+ 跑一遍，最短的反例往往只有四五步，几秒钟就出来。每条反例都拿真代码复现一遍再算 bug
  7. 修完后的「0 违规」，补三件事：跑完没有、路径可达吗、检查器喂旧代码会不会红
  8. TLC 的状态目录放到空间大的盘上