强化 Turso：使用形式化方法和 Quint 查找 SQLite Bug

对于任何构建数据库的团队来说，SQLite 代表了可靠性的最高标准。由于 Turso 是 SQLite 的重写版，保持同等的可信度不仅是目标，更是必需。为此，Turso 采用了包括确定性模拟测试（DST）、差分测试器、模糊测试以及并发模拟器在内的严格测试体系。

尽管方法全面，团队仍意识到其策略中缺少了一环：形式化方法。虽然传统上被视为难以接近或过于复杂，形式化方法却能提供传统测试无法达到的数学确定性。通过集成 Quint——一种现代的形式化验证工具，Turso 将硬化过程进一步推进，最终在 SQLite 本身中发现了超过 10 个 bug。

形式化方法的挑战

形式化方法（如 TLA+）是业界验证系统正确性的基准。然而，它们往往存在高门槛以及“谁监督监督者”的难题——即验证系统模型本身是否正确的困难。

为了解决这些问题，Turso 与社区成员 Pavan Nambi 合作，使用 Quint。Quint 将时序逻辑动作（Temporal Logic of Actions，TLA）的理论基础与现代类型检查和开发工具相结合，使其对工程师更易上手。

团队并未尝试对整个 SQLite 系统进行建模，而是聚焦于 C API。由于 C API 文档完善且是大多数 SQLite 驱动的主要接口，对其建模提供了高杠杆的覆盖点。这一做法使团队能够将 API 规范作为真相来源，以验证模型和实际实现的一致性。

“Quinting” 过程

发现 bug 的方法论是一个重复的四步循环：

  1. 建模合约：挑选一个已文档化的 SQLite C API 合约，并在 Quint 中建模所需的状态和属性。
  2. 生成轨迹：使用 Quint 生成可能违反合约的状态序列（轨迹）。
  3. 执行：将这些轨迹转化为一个小型 C 程序，并在 SQLite 上运行。
  4. 比较：将系统的实际行为与文档中规定的结果进行对比。

当模型检查器发现失败时，会产生一个反例——导致违规的具体状态序列。虽然许多反例仅验证了模型的正确性，另一些则揭示系统偏离了自身规范。

案例研究：sqlite3_deserialize()

一个突出的例子涉及 sqlite3_deserialize() 函数，该函数允许将序列化的数据库镜像加载为内存数据库。

根据规范，若目标数据库正处于读取事务或参与备份操作，sqlite3_deserialize() 应返回 SQLITE_BUSY。Quint 模型生成的轨迹如下：

  1. 打开数据库 → 创建表 → 序列化数据库。
  2. 开始对数据库进行读取。
  3. 在读取事务仍然活跃时调用 sqlite3_deserialize()。

预期的返回码是 SQLITE_BUSY，但实际结果却是系统崩溃。因为崩溃几乎从未是预期行为，这立即确认了 bug 出在实现而非模型。该问题随后在 SQLite 源码中得到修复。

结果与发现

使用 Quint 的探索极为高效，揭示了从优化逻辑错误到关键崩溃的广泛 bug。主要发现包括：

  • 优化失效：EXISTS-to-join 优化错误地应用了 LIMIT/OFFSET 或丢失外部关联，导致有效行被过滤。
  • 约束违规：约束名称被引用后变得不可删除，或 xfer 优化绕过检查约束，导致数据库不一致。
  • 稳定性问题：在内部表上执行 ALTER ADD CHECK 时崩溃，或在 sqlite3changegroup_change_finish() 中出现 NULL pzErr 导致的崩溃。
  • 内存与对齐：与 sqlite3_mutex 128 字节对齐相关的未定义行为。

结论

SQLite 是现存最经过严格测试的软件之一。然而，通过 Quint 应用形式化方法，Turso 发现了数十年传统测试未能捕获的 bug。

通过将形式化轨迹转化为可执行的 C 程序，Turso 不仅强化了自身实现，还对更广泛的 SQLite 生态系统的稳定性作出了重要贡献。这表明，当形式化方法针对特定、定义明确的接口（如 C API）时，能够成为现代软件可靠性的强大工具。

Sources