Reasoning about Weak Isolation Levels in Separation Logic

TL;DR

This paper formalizes weak isolation levels in separation logic, enabling reasoning about their implementations and verifying a key-value database satisfies snapshot isolation, which is crucial for industrial database correctness.

Contribution

It introduces modular separation logic specifications for weak isolation levels and verifies an implementation against these specifications, bridging theory and practical database systems.

Findings

Formal separation logic specifications for weak isolation levels.

Verification of a key-value database implementation satisfying snapshot isolation.

Implication proofs between different isolation levels.

Abstract

Consistency guarantees among concurrently executing transactions in local- and distributed systems, commonly referred to as isolation levels, have been formalized in a number of models. Thus far, no model can reason about executable implementations of databases or local transaction libraries providing weak isolation levels. Weak isolation levels are characterized by being highly concurrent and, unlike their stronger counterpart serializability, they are not equivalent to the consistency guarantees provided by a transaction library implemented using a global lock. Industrial-strength databases almost exclusively implement weak isolation levels as their default level. This calls for formalism as numerous bugs violating isolation have been detected in these databases. In this paper, we formalize three weak isolation levels in separation logic, namely read uncommitted, read committed, and snapshot isolation. We define modular separation logic specifications that are independent of the underlying transaction library implementation. Historically, isolation levels have been specified using examples of executions between concurrent transactions that are not allowed to occur, and we demonstrate that our specifications correctly prohibit such examples. To show that our specifications are realizable, we formally verify that an executable implementation of a key-value database running the multi-version concurrency control algorithm from the original snapshot isolation paper satisfies our specification of snapshot isolation. Moreover, we prove implications between the specifications -- snapshot isolation implies read committed and read committed implies read uncommitted -- and thus the verification effort of the database serves as proof that all of our specifications are realizable. All results are mechanized in the Rocq proof assistant on top of the Iris separation logic framework.