一句话：在分离逻辑中形式化读未提交、读已提交与快照隔离三种弱隔离级别，并机器验证MVCC数据库实现满足快照隔离。
并发事务的弱隔离级别在工业数据库中被广泛默认使用，但已有形式化模型难以推理可执行数据库或本地事务库的实现，导致隔离违例难以发现与排除。本文在分离逻辑中形式化读未提交、读已提交和快照隔离，给出与底层事务库实现无关的模块化规约，并用并发事务的禁止执行例子检验规约。为表明规约可满足，作者形式验证一个按原快照隔离论文中多版本并发控制（MVCC）算法实现的可执行键值数据库满足快照隔离规约；同时证明快照隔离蕴含读已提交、读已提交蕴含读未提交，因此数据库验证也表明所有规约可实现。全部结果在 Rocq 证明助手与 Iris 分离逻辑框架中机器化。
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 counter part 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.
@article{paperbot3052,
title = {Reasoning about Weak Isolation Levels in Separation Logic},
author = {Anders Alnor Mathiasen and Léon Gondelman and Léon Ducruet and Amin Timany and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {ICFP},
year = {2025},
doi = {10.1145/3747515}
}