用 TLA+ 复查 SQLite 存在 16 年的检查点缺陷 RSS

Canonical 的 Marco Manino 与 Alberto Carretero 用 TLA+ 复查了 SQLite 里一个 2010 年就存在的数据损坏缺陷：检查点与写入并发地重置 WAL 文件时会发生竞态。他们为追加页面和检查点行为写了形式化规格，模型检查器很快找出触发问题的执行序列。SQLite 的修复办法是比较检查点前后的 WAL salt，变了就跳过。dqlite 不受影响，它在两种操作期间都持有写锁。

发布于 2026-09-10T10:59:44.571877Z · Marco Manino、Alberto Carretero · Ubuntu 博客

SQLite WAL 形式化验证

Canonical 的 Marco Manino 与 Alberto Carretero 用 TLA+ 复查了 SQLite 里一个 2010 年就存在的数据损坏缺陷：检查点与写入并发地重置 WAL 文件时会发生竞态。他们为追加页面和检查点行为写了形式化规格，模型检查器很快找出触发问题的执行序列。SQLite 的修复办法是比较检查点前后的 WAL salt，变了就跳过。dqlite 不受影响，它在两种操作期间都持有写锁。

Canonical 的 Marco Manino 与 Alberto Carretero 用 TLA+ 复查了 SQLite 里一个 2010 年就存在的数据损坏缺陷：检查点与写入并发地重置 WAL 文件时会发生竞态。他们为追加页面和检查点行为写了形式化规格，模型检查器很快找出触发问题的执行序列。SQLite 的修复办法是比较检查点前后的 WAL salt，变了就跳过。dqlite 不受影响，它在两种操作期间都持有写锁。

原始来源 ↗

来源记录

• center.info_item · 074f3bba38cbfef4 · 2026-10-03T04:08:35.169032Z
• pgweb.info_item · 074f3bba38cbfef4 · 2026-10-03T04:08:55.967155Z