论文标题
ELLE：从实验观测中推断出隔离异常
Elle: Inferring Isolation Anomalies from Experimental Observations
论文作者
论文摘要
关心数据存储的用户在数据库中（至少原则上）保证某种形式的交易隔离。但是，经验表明[Kleppmann 2019，Kingsbury和Patella 2019a]，许多数据库没有提供他们声称的隔离保证。随着新的分布式数据库的最新扩散，对棋子的需求已经增长，这些检查者可以通过产生客户工作量并注入故障，产生异常，以见证违反规定的担保。理想的检查器将是合理的（没有误报），有效的（在历史长度和并发方面多项式），有效（在实际数据库中找到违规），一般（分析许多交易模式）和信息性（证明存在具有可理解的反例的异常现象的合理性）。可悲的是，我们知道没有满足这些目标的棋子。 我们提出Elle：一个新颖的检查器，它渗透了客户观察到的交易之间的ADYA风格依赖图。它通过在生成历史记录时仔细选择数据库对象和操作来做到这一点，从而确保数据库读取的结果显示有关其版本历史记录的信息。 Elle可以检测Adya等人的形式主义中的每一个异常[Adya等。 2000]（除谓词除外），区分它们，并提供对每个的简洁解释。本文做出了以下贡献：我们提出Elle，证明其健全性，衡量其对当前最新状态的效率，并通过对四个真实数据库的案例研究提供了其有效性的证据。
Users who care about their data store it in databases, which (at least in principle) guarantee some form of transactional isolation. However, experience shows [Kleppmann 2019, Kingsbury and Patella 2019a] that many databases do not provide the isolation guarantees they claim. With the recent proliferation of new distributed databases, demand has grown for checkers that can, by generating client workloads and injecting faults, produce anomalies that witness a violation of a stated guarantee. An ideal checker would be sound (no false positives), efficient (polynomial in history length and concurrency), effective (finding violations in real databases), general (analyzing many patterns of transactions), and informative (justifying the presence of an anomaly with understandable counterexamples). Sadly, we are aware of no checkers that satisfy these goals. We present Elle: a novel checker which infers an Adya-style dependency graph between client-observed transactions. It does so by carefully selecting database objects and operations when generating histories, so as to ensure that the results of database reads reveal information about their version history. Elle can detect every anomaly in Adya et al's formalism [Adya et al. 2000] (except for predicates), discriminate between them, and provide concise explanations of each. This paper makes the following contributions: we present Elle, demonstrate its soundness, measure its efficiency against the current state of the art, and give evidence of its effectiveness via a case study of four real databases.
