AI 中文总结
研究如何验证数据库实现的隔离级别，核心方法是从分离逻辑规范结构推导隔离级别，考虑所有程序执行情况，主要贡献是得出自由定理，提高了数据库健壮性标准。
AI 中文摘要
现代数据库高度并发，通过事务将多个数据库操作分组为原子应用单元。数据库供应商和软件工程师用隔离级别描述事务的一致性保证。流行的隔离级别为优化应用性能提供了弱保证且语义复杂。确保数据库实现符合应用开发者所依赖的隔离级别保证这一问题受测试社区广泛关注。此前尚无方法正式验证数据库实现是否真的实现了供应商宣称的隔离级别。本文提出一种验证数据库实现隔离级别的方法：直接从分离逻辑规范的结构中推导出如数据库社区在事务一致性模型中形式化的隔离级别。这样考虑了数据库及其任意客户端可能产生的所有程序执行情况。结果是一个所谓的自由定理，即任何根据特定分离逻辑规范集验证操作的数据库实现实际上都实现了其隔离级别。由于本文所有证明都在Rocq证明助手 中机械化，并基于程序执行的详细语义模型，我们相信这一贡献提高了数据库可实现的健壮性标准。
英文摘要
Modern databases are highly concurrent and provide transactions as a mean of grouping several database operations into atomically applied units. Database vendors and software engineers use isolation levels to describe the consistency guarantees of transactions. The popular isolation levels give weak guarantees, with intricate semantics, to optimize performance of applications. The problem of assuring that database implementations actually implement the isolation level guarantees that application developers build their systems upon has received a great deal of attention from the testing community. But until now, there exists no method for formally verifying that a database implementation actually implements the isolation level that database vendors says it provides. In this paper, we present a method for verifying that a database implements an isolation level: we derive isolation levels directly, as formalized in transactional consistency models by the database community, from the structure of separation logic specifications. By doing so, we consider all program executions that a database and arbitrary clients of the database could produce. The result is a so-called free theorem meaning that any database implementation, whose operations are verified against a specific set of separation logic specifications, actually implements its isolation level. As all proofs in this paper are mechanized in the Rocq proof assistant and build upon a detailed semantic model of program execution, we believe this contribution raises the bar for the achievable robustness of databases.
