数据库中快照隔离的高效黑盒检测
Efficient Black-box Checking of Snapshot Isolation in Databases
AI总结：
提出PolySI，一种基于广义多图的高效黑盒快照隔离检测器，通过SMT求解和约束优化准确复现已知异常、发现生产云数据库新型违规并优于现有方法。
摘要：
快照隔离（SI）是一种普遍的弱隔离级别，它避免了可串行化带来的性能损失，同时防止了各种不希望出现的数据异常。然而，近期在声称提供 SI 保证的生产云数据库中发现了 SI 异常。鉴于此类数据库内部结构复杂且通常不可用，黑盒 SI 检测器是非常理想的。本文提出了 PolySI，一种新颖的黑盒检测器，能高效检测 SI 并在发现违规时提供易于理解的对抗样本。PolySI 基于使用广义多图（GPs）对 SI 的新颖刻画，我们证明了其可靠性和完备性。PolySI 采用 SMT 求解器，并利用 GPs 的紧凑约束编码和领域特定优化来剪枝约束，从而加速 SMT 求解。广泛评估表明，PolySI 成功复现了全部 2477 个已知 SI 异常，在三个生产云数据库中检测到新型 SI 违规并识别其原因，在多种工作负载下优于最先进的黑盒检测器，且可扩展至大规模工作负载。
英文摘要：
Snapshot isolation (SI) is a prevalent weak isolation level that avoids the performance penalty imposed by serializability and simultaneously prevents various undesired data anomalies. Nevertheless, SI anomalies have recently been found in production cloud databases that claim to provide the SI guarantee. Given the complex and often unavailable internals of such databases, a black-box SI checker is highly desirable. In this paper we present PolySI, a novel black-box checker that efficiently checks SI and provides understandable counterexamples upon detecting violations. PolySI builds on a novel characterization of SI using generalized polygraphs (GPs), for which we establish its soundness and completeness. PolySI employs an SMT solver and also accelerates SMT solving by utilizing the compact constraint encoding of GPs and domain-specific optimizations for pruning constraints. As demonstrated by our extensive assessment, PolySI successfully reproduces all of 2477 known SI anomalies, detects novel SI violations in three production cloud databases, identifies their causes, outperforms the state-of-the-art black-box checkers under a wide range of workloads, and can scale up to large-sized workloads.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
