Hunting a 16-year-old SQLite WAL bug with TLA+
13 days ago
- #Database Corruption
- #TLA+
- #SQLite
- SQLite 最近修复了一个存在 16 年的写入前日志 (WAL) 检查点机制中的错误，该错误可能导致数据库损坏。
- 该错误涉及将新页面追加到 WAL 与检查点操作之间的竞态条件，其中写进程可能在检查点进行过程中重置 WAL，导致数据丢失。
- dqlite 团队使用 TLA+ 建模了 SQLite 的行为以理解错误序列，然后为 dqlite 创建了一个单独的模型以检查其是否受影响。
- Dqlite 的设计通过使用更严格的锁机制避免了该错误：检查点是停止世界操作，需要获取写锁，从而消除了 SQLite 中导致竞态条件的并发性。
- SQLite 的修复措施是在检查点过程中增加一个验证步骤，确认自检查点开始以来 WAL 的盐值未发生变化，从而防止数据竞争。