一句话：提出以客户端观测为中心的符号编码方法，用 SMT 求解验证黑盒数据库事务的语义正确性与隔离保证。
客户端依赖数据库系统既正确实现事务语义，又为事务提供隔离保证，但对黑盒系统同时检查这两方面十分困难。本文提出一种以客户端为中心的技术：基于在数据库系统上运行事务所收集的观测，判定是否存在给定隔离级别下可能的正确执行能够产生这些观测，以此定义并检查「可观察正确性」。技术核心是两类新颖的符号编码：弱隔离下事务语义正确性的编码，以及隔离级别保证的编码；二者交由 SMT 求解器查询。作者实现工具 Troubadour，并用它验证了包括 PostgreSQL 与一个在研工业系统在内的多个数据库系统，期间帮助发现两个新 bug，同时也能找出已知的语义正确性 bug 并检测隔离相关的异常。
Clients rely on database systems to be correct, which requires the system not only to implement transactions’ semantics correctly but also to provide isolation guarantees for the transactions. This paper presents a clientcentric technique for checking both semantic correctness and isolation-level guarantees for black-box database systems based on observations collected from running transactions on these systems. Our technique verifies observational correctness with respect to a given set of transactions and observations for them, which holds iff there exists a possible correct execution of the transactions under a given isolation level that could result in these observations. Our technique relies on novel symbolic encodings of (1) the semantic correctness of database transactions in the presence of weak isolation and (2) isolation-level guarantees. These are used by the checker to query a Satisfiability Modulo Theories solver. We applied our tool Troubadour to verify observational correctness of several database systems, including PostgreSQL and an industrial system under development, in which the tool helped detect two new bugs. We also demonstrate that Troubadour is able to find known semantic correctness bugs and detect isolation-related anomalies.
@article{paperbot3207,
title = {Checking Observational Correctness of Database Systems},
author = {Lauren Pick and Amanda Xu and Ankush Desai and Sanjit A. Seshia and Aws Albarghouthi},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720504}
}