Introduction

Recently, SQLite published a new version with a fix to a long-standing bug in the way that the Write Ahead Log (WAL) is checkpointed that leads to the corruption of the database [1]. In order to find out if dqlite, a distributed version of SQLite, is affected by this bug, we first need to be able to understand the exact sequence of steps that leads to database corruption. To do that, we will be using TLA+ to model SQLite’s behavior and quickly find a trace that allows us to reason about the bug.

Modeling the Bug in TLA+

We start by modeling the behavior of SQLite’s WAL and checkpointing system using TLA+. The TLA+ model consists of several variables, including wal, db, nBackfill, mxFrame, frameNumber, checkPointState, safeMxFrame, walSalt, and pWalSalt. We also define two actions, WalAppendTakeLock and WalAppend, which represent the appending of pages to the WAL and the checkpointing of the WAL, respectively [2].

Reproducing the Bug

Once the model is in place, we can define an invariant that will trigger in the event of data loss or database corruption. Running the model-checker quickly finds a counter-example, which takes only 20 states to witness a missing page in the database [3].

Is dqlite Affected?

To answer this question, we create a model for dqlite that captures the differences with SQLite itself. We then model-check again to see if the invariant breaks. Given that dqlite needs to coordinate writes with Raft, it needs to be more restrictive with regards to which operations can proceed simultaneously. For this reason, dqlite blocks any user-initiated checkpoint and disables automatic ones [4].

Conclusion

By using TLA+ to model SQLite’s behavior and identify the exact sequence of steps needed to trigger the corruption, we were able to determine that dqlite is not affected by the bug. This is because by taking the write lock for both appending and checkpointing, they cannot proceed simultaneously, and there is no data race [5].

Sources

  1. https://www.sqlite.org/releaselog/3_51_3.html
  2. https://github.com/canonical/ubuntu.com/issues/new?template=ISSUE_TEMPLATE.yaml
  3. https://www.sqlite.org/wal.html#walresetbug
  4. https://ubuntu.com/blog/hunting-a-16-year-old-sqlite-bug-with-tla-is-dqlite-affected
  5. https://news.ycombinator.com/item?id=48730953