The final boss of reliability: formal verification

Turso is a rewrite of SQLite from scratch, with a novel architecture that allows us to do some cool things like concurrent writes, vector search, native WASM execution, a native sync engine, among many other cool features that modern databases need.

We put a big emphasis on correctness and reliability. In this article, we will look into how we are partnering with Aretta AI, a company offering what I dubbed “Formal Methods for Mere Mortals” to take our reliability to the next level.

#What does “Compatible with SQLite means”?

At Turso, our aim is to be fully compatible with SQLite and expand on it, not to offer a trade off. As such, it is important for us to be compatible with SQLite’s foremost feature: its extraordinarily insane autistic-level reliability.

From the beginning, we have been employing Deterministic Simulation Testing. We both have our own simulator, meaning that we can use a pluggable implementation to replace every I/O and source of randomness (including timing) in the database with a simulated version and let it run wild. On top of that, we also routinely run Antithesis, which offers a similar service at a lower level of the stack, allowing us to catch a class of bugs that our simulator wouldn’t catch (including bugs in the simulator itself).

#The importance of testing is only increasing

Coding this way has transformed the way we work (and we have been doing this since coding was something you did by typing magic symbols in a magical incantation language, not English). The main reason is that not only does this provide high levels of reliability, but it also shortens the feedback loop, allowing us to spend more time thinking and architecting and less time debugging.

Now that coding is done by asking the magic box to do things, this becomes even more crucial. Without a very fast feedback loop, clankers get lost in “thought” and go awry.

#The next frontier

But you know how it goes: at the end of the day, we’re humans. For better or worse we adapt. And what was amazing yesterday, becomes table stakes. We start seeing a new whole class of problems and want even better results.

And the problem with Deterministic Simulation Testing (DST), as we came to see, is the following: it just takes way too much time. The idea of automatically generating a large set of possibilities, executing the code is a great gate against defects. But it costs a lot in both time and money, and every time we manage to catch a bug before it reaches that stage, we’re all better off: debugging is simpler, and the feedback loop is even faster.

And much like a modern person on a plane complaining it doesn’t go fast enough, perhaps we should just be thankful for this absolute marvel of technology we have at our disposal in the form of DST and just shut the hell up. But we want more, and we shall have it!

#Enters Aristo

Aristo is a product by Aretta.ai, that allows us to encode intents about the system in natural language. The product helps us extract formal verifications out of it. Formal verifications are mathematical representations of the state of the system that can be abstractly verified, without having to actually execute an exhaustive set of states.

Formal Verification doesn't replace the testing we already have. After all, it is as Donald Knuth once said when thinking whether or not his software would work: “Beware of bugs in the above code; I have only proved it correct, not tried it.”

However deviations from the formal methods have a much faster feedback loop. They are also computationally cheap to run, and less dependent on randomness to generate the right failing seeds, and on the quality of generators. So whatever we can catch at this state is a big plus.

#An example

The gains are not just theoretical: Aristo already helped us find a bug that had escaped our DST validation. Upon later inspection it was found that this is because our generators were not generating the particular situation that would lead to this bug (faults on fsync when the database was used as a sync replica). It also found it in mere minutes, where from experience we know it would have taken us hours using our DST validation.

You can read more about the bug and the fix here. It is as follows:

When you write data to durable media (like your SSD), you may think the data is durable, and will survive restarts, power losses, etc. But people leading a database-centric lifestyle know this to be an illusion: data that you wrote to disk is as trustworthy as the Zimbabwean Dollar, until you call an Operating System facility, commonly called fsync on unix. This happens because making data really durable is very expensive and crashes are rare. So the OS allows people crazy enough to go into Databases to speed things up by faking the writes until at a later point where you can batch a lot of them together and say that after that, all of those many writes are really durable.

Turso, like any other database, has to call fsync in many specific points of its lifetime. Failure to do so can cause very nasty bugs that only reproduce when failures happen in specific ways in a specific order. Not fun to find, and even harder to debug.

Turso has a native sync engine attached to it. That means that the database can become a copy of the master database on a remote server (aka “the cloud”). And in that situation, knowing that new data pages will be sewed into the database’s B-Tree representation, we bypass the local page cache (which as the name implies, is an in-memory cache of the actual pages that exist on disk, for faster access). Pages in the page cache can become dirty if they are modified, which is our cue to fsync them when they are made durable (at which point they become clean again).

But when Turso was used as a local replica of the Cloud database, since we skipped the page cache, pages were getting dirty without the dirty bit being set in the page cache. In some situations, where other paths would trigger fsyncs, we would call it. In others, we were writing them to disk, without calling fsync.

This is the intent that caught the bug, straight from our WAL code. It states, in plain English, the durability rule the code above was violating:

#[aristo::intent(
    "A commit frame must reach stable storage via fsync \
     before the transaction is reported as durable",
    id = "aristos:wal_commit_requires_fsync",
    verify = "full",
    parent = "wal_protocol_correctness"
)]
fn commit_dirty_pages_inner(
    &self,
    allowed_auto_actions: WalAutoActions,
    ...

#Why this makes sense

This is exactly where formal verification shines: the system has properties that can be encoded by the system designer, like “after a page is written to the media, fsync must eventually be called”. Runtime-based validation may fail to find this, since the majority of the runs will end up calling it for unrelated reasons. The formal method encodes this property at the code-level, and is able to demonstrate where the property fails to hold.

For us, it is one more tool to have in our arsenal in the task to make Turso a worthy replacement for the most reliable database on Earth. A tool that has already proved its value. Because of that, we are deepening our partnership with Aretta.ai, and bringing them into the fold of our testing routine. Our goal is to get to our upcoming 1.0 with a level of reliability as high as humanly (or now machinely) possible, and we are excited for what formal verification can do.