EagleBear2002 的博客

\[ \def\prefix{\mathsf{prefix}} \def\postfix{\mathsf{postfix}} \def\T{\mathcal{T}} \def\I{\mathcal{I}} \def\C{\mathsf{C}} \def\W{\mathsf{W}} \def\R{\mathsf{R}} \def\Obj{\mathsf{Obj}} \]

摘要

虽然可串行化始终保证应用程序的正确性，但可以选择较低的隔离级别来提高事务吞吐量，但风险是引入某些异常。如果在指定的隔离级别下，所有可能的事务交错都是可串行化的，则一组事务对给定的隔离级别具有鲁棒性。因此，鲁棒性始终保证应用程序的正确性，同时具有较低隔离级别的性能优势。虽然鲁棒性问题在文献中受到了广泛关注，但只获得了充分条件。最值得注意的例外是 Fekete 的开创性工作，他获得了确定针对 SI 的鲁棒性的特征。在本文中，我们解决了较低 SQL 隔离级别 RU 和 RC 的鲁棒性问题，它们是根据禁止的脏写和脏读模式定义的。本文的第一个主要贡献是，我们根据特定形式（拆分和多拆分调度 ）的反例调度 的缺失以及满足各种属性的干涉图中的环的缺失来表征针对这两个隔离级别的鲁棒性。与 Fekete 的工作的一个关键区别是，本文获得的环属性必须考虑事务内操作的相对顺序，因为 RU 和 RC 不满足原子可见性要求。一个特殊的结果是后者导致了针对 RC coNP-complete 的鲁棒性问题。本文的第二个主要贡献是 coNP-hardness 证明。对于 RU，我们获得了 LOGSPACE-completeness。

作者：

• Bas Ketsman, Vrije Universiteit Brussel, Belgium
• Christoph Koch, École Polytechnique Fédérale de Lausanne, Switzerland
• Frank Neven, UHasselt, Data Science Institute, ACSL, Belgium
• Brecht Vandevoort, UHasselt, Data Science Institute, ACSL, Belgium

摘要

语法问题

明确句式结构，特别要注意主语问题。反例：

数字经济学科推荐书目为《第三次工业革命》和《第二次机器革命》，知科技前沿，晓时代发展，通中国国情。（错误）

整句话按照语法缩句为“数字经济学科知科技前沿……”，应该修改为：

\[ \def\SER{\mathsf{SER}} \def\PSI{\mathsf{PSI}} \def\SI{\mathsf{SI}} \def\PC{\mathsf{PC}} \def\CC{\mathsf{CC}} \def\RA{\mathsf{RA}} \def\read{\mathtt{read}} \def\write{\mathtt{write}} \def\Event{\mathsf{Event}} \def\Obj{\mathsf{Obj}} \def\hist{\mathsf{hist}} \def\level{\mathsf{level}} \def\before{\mathsf{before}} \def\po{\mathsf{\textcolor{red}{po}}} \def\wr{\mathsf{\textcolor{teal}{wr}}} \def\ww{\mathsf{\textcolor{red}{ww}}} \def\rw{\mathsf{\textcolor{blue}{rw}}} \def\co{\mathsf{\textcolor{orange}{co}}} \def\CO{\mathsf{\textcolor{brown}{CO}}} \def\Int{\mathtt{Int}} \def\Ext{\mathtt{Ext}} \def\Prefix{\mathtt{Prefix}} \def\Conflict{\mathtt{Conflict}} \def\SerTotal{\mathtt{SerTotal}} \def\lthb{\lt_\mathsf{hb}} \def\ltar{\lt_\mathsf{ar}} \def\ltpo{\lt_\mathsf{po}} \def\DDG{\mathsf{DDG}} \def\SDG{\mathsf{SDG}} \def\I{\mathcal{I}} \]

摘要

为了实现可扩展性，现代互联网服务通常依赖于分布式数据库，其事务一致性模型比可序列化性要弱。目前，应用程序员通常缺乏确保这些一致性模型的弱点不会违反应用程序正确性的技术。我们提出了一些标准来检查依赖于仅提供弱一致性的数据库的应用程序是否具有鲁棒性，即其行为是否像使用提供可序列化的数据库一样。在这种情况下，应用程序员可以获得弱一致性的可扩展性优势，同时能够轻松检查所需的正确性属性。我们的结果系统而统一地处理了最近提出的几种弱一致性模型，以及一种增强应用程序各部分一致性的机制。

本文的研究对象的是分布式数据库及其一致性。

作者：

\[ \def\read{\mathsf{read}} \def\write{\mathsf{write}} \def\Writes{\mathsf{Writes}} \def\SER{\mathsf{SER}} \def\SI{\mathsf{SI}} \def\po{\mathsf{\textcolor{red}{po}}} \def\so{\mathsf{\textcolor{purple}{so}}} \def\wr{\mathsf{\textcolor{teal}{wr}}} \def\VIS{\mathsf{\textcolor{orange}{VIS}}} \def\antiVIS{\mathsf{\overline{\VIS^{-1}}}} \def\AR{\mathsf{\textcolor{pink}{AR}}} \def\WR{\mathsf{\textcolor{teal}{WR}}} \def\WW{\mathsf{\textcolor{red}{WW}}} \def\RW{\mathsf{\textcolor{blue}{RW}}} \def\T{\mathcal{T}} \def\X{\mathcal{X}} \def\Executions{\mathsf{Executions}} \def\modelOf{\mathsf{modelOf}} \]

摘要

现代分布式系统通常依赖于所谓的弱一致性数据库，这种数据库通过削弱分布式事务处理的一致性保证来实现可扩展性。这种数据库的语义已被形式化为两种不同的风格，一种基于抽象执行，另一种基于依赖图。这两种风格的选择是根据预期应用做出的。前者用于指定和验证数据库的实现，而后者用于证明数据库客户端程序的属性。在本文中，我们提出了一组新的代数定律（不等式），将这两种规范风格联系起来。这些定律将基于抽象执行的规范中使用的二元关系与基于依赖图的规范中使用的二元关系联系起来。然后我们表明，这种代数联系产生了所谓的鲁棒性标准：确保弱一致性数据库的客户端程序不会因弱一致性而表现出异常行为的条件。这些标准使得推理这些客户端程序变得容易，并可能成为动态或静态程序分析的基础。对于某一类一致性模型规范，我们证明了连接两种规范风格的完整抽象结果。

作者：

• Andrea Cerone, IMDEA Software Institute
• Alexey Gotsman, IMDEA Software Institute
• Hongseok Yang, University of Oxford, UK

\[ \def\read{\mathsf{read}} \def\write{\mathsf{write}} \def\SER{\mathsf{SER}} \def\SI{\mathsf{SI}} \def\po{\mathsf{\textcolor{red}{po}}} \def\SO{\mathsf{\textcolor{purple}{SO}}} \def\VIS{\mathsf{\textcolor{orange}{VIS}}} \def\CO{\mathsf{\textcolor{orange}{CO}}} \def\WR{\mathsf{\textcolor{green}{WR}}} \def\WW{\mathsf{\textcolor{red}{WW}}} \def\RW{\mathsf{\textcolor{blue}{RW}}} \def\H{\mathcal{H}} \def\T{\mathcal{T}} \def\X{\mathcal{X}} \def\G{\mathcal{G}} \def\P{\mathcal{P}} \def\Int{\mathtt{Int}} \def\Ext{\mathtt{Ext}} \def\Session{\mathtt{Session}} \def\Prefix{\mathtt{Prefix}} \def\NoConflict{\mathtt{NoConflict}} \def\TotalVis{\mathtt{TotalVis}} \def\PreExecSI{\mathsf{PreExecSI}} \def\ExecSI{\mathsf{ExecSI}} \def\ExecSER{\mathsf{ExecSER}} \def\HistSI{\mathsf{HistSI}} \def\HistSER{\mathsf{HistSER}} \def\GraphSER{\mathsf{GraphSER}} \def\GraphSI{\mathsf{GraphSI}} \def\graph{\mathsf{graph}} \def\splice{\mathsf{splice}} \def\DCG{\mathsf{DCG}} \]

摘要

快照隔离（SI）是一种广泛使用的事务处理一致性模型，由大多数主流数据库和一些事务内存系统实现。不幸的是，它的经典定义是以低级操作方式给出的，通过理想化的并发控制算法，这使得对在 SI 下运行的应用程序的行为的推理变得复杂。我们给出了 SI 的替代规范，该规范根据 Adya 等人的事务依赖图对其进行了描述，概括了序列化图。与以前的工作不同，我们的描述不需要在依赖图中添加有关事务开始点和提交点的额外信息。然后，我们利用我们的规范来获得两种静态分析。第一个检查在 SI 下运行的一组事务何时可以分成更小的部分而不引入新的行为，以提高性能。另一个分析检查在 SI 减弱的情况下运行的一组事务是否与在 SI 下运行时的行为相同。

作者：

• Andrea Cerone, IMDEA Software Institute
• Alexey Gotsman, IMDEA Software Institute

摘要

事务稳健性问题围绕着决定对于给定的工作负载，低于 SER 的隔离级别是否足以保证可序列化性。本文提出了针对隔离级别（多版本）读取已提交的稳健性的新特征。它支持具有控制结构（循环和条件）以及插入、删除和谓词读取的事务程序 - 触发幻影问题的场景，众所周知，幻影问题在这种情况下很难分析。该特征是图论性的，与数据库研究人员和实践者熟悉的并发控制文献中已知的先前决策机制并无不同。我们通过实验表明，我们的特征突破了界限，允许识别比以前更复杂的工作负载。

作者：

• Brecht Vandevoort, UHasselt, Data Science Institute, ACSL, Belgium
• Bas Ketsman, Vrije Universiteit Brussel, Belgium
• Christoph Koch, École Polytechnique Fédérale de Lausanne, Switzerland
• Frank Neven, UHasselt, Data Science Institute, ACSL, Belgium

INTRODUCTION

摘要

流行的隔离级别多版本读已提交 (RC) 牺牲了一些强大的可串行化保证，以换取更高的事务吞吐量。有时，事务工作负载可以在 RC 下安全地执行，从而以较低的 RC 成本获得可串行化。这种工作负载被称为对 RC 具有鲁棒性。先前的研究已经产生了一种可处理的程序，用于确定由事务程序建模为事务模板生成的工作负载对 RC 的鲁棒性。这项工作的一个重要见解是，通过更准确地建模事务程序，我们能够将更大的工作负载集识别为鲁棒的。在这项工作中，我们通过为事务模板扩展功能约束来提高其建模能力，这对于捕获外键等数据依赖关系非常有用。我们表明，加入功能约束可以将更多原本不具有鲁棒性的工作负载识别为鲁棒的。尽管我们确定鲁棒性问题在其最一般的形式下变得不可判定，但我们表明，对功能约束的各种限制会导致可判定甚至可处理的片段，这些片段可用于为现实场景建模和测试对 RC 的鲁棒性。

作者：

• Brecht Vandevoort, UHasselt, Data Science Institute, ACSL, Belgium
• Bas Ketsman, Vrije Universiteit Brussel, Belgium
• Christoph Koch, École Polytechnique Fédérale de Lausanne, Switzerland
• Frank Neven, UHasselt, Data Science Institute, ACSL, Belgium

摘要

流行的隔离级别多版本读已提交（RC）用牺牲强大的可串行化保证来换取事务吞吐量的提高。尽管如此，事务工作负载有时可以在 RC 下执行，同时仍能以较低的成本保证可串行化。这样的工作负载被称为对 RC 具有鲁棒性。本文概述了确定对 RC 的鲁棒性。特别是，我们讨论了如何通过事务模板的形式化来获得合理完整的测试。然后，我们通过使用功能约束来扩展事务模板，从而提高其建模能力，这些功能约束可用于捕获外键等数据依赖关系。我们表明，加入功能约束可以将更多的工作负载识别为鲁棒的，而不是其他情况。即使鲁棒性问题在其最一般的形式下变得不可判定，我们仍确定对功能约束的各种限制会导致可判定甚至可处理的结果，这些结果可用于对实际场景的 RC 鲁棒性进行建模和测试。

作者：

• Brecht Vandevoort, UHasselt, Data Science Institute, ACSL, Belgium
• Bas Ketsman, Vrije Universiteit Brussel, Belgium
• Christoph Koch, École Polytechnique Fédérale de Lausanne, Switzerland
• Frank Neven, UHasselt, Data Science Institute, ACSL, Belgium

INTRODUCTION

摘要

事务处理是大多数数据库应用程序的核心部分。虽然可序列化性仍然是理想事务语义的黄金标准，但许多数据库系统通过选择较低的隔离级别来提高事务吞吐量，但代价是引入潜在的异常。事务通常不是任意的，而是受到在应用程序级别定义的一组事务程序的约束（例如 TPC-C 的情况），这意味着并非所有潜在异常都能有效实现。本文的核心问题是：在特定事务程序的上下文中，何时隔离级别低于可序列化性，才能提供与可序列化性相同的保证？我们将后者称为稳健性问题。本文调查了针对（多版本）读取提交的稳健性测试的最新结果，重点关注完整条件而非充分条件。我们展示了如何将稳健性测试提升到事务模板和程序以增加实际适用性。我们讨论了未解决的问题并强调了未来研究的有希望的方向。

作者：

• Brecht Vandevoort, UHasselt, Data Science Institute, ACSL, Belgium
• Bas Ketsman, Vrije Universiteit Brussel, Belgium
• Christoph Koch, École Polytechnique Fédérale de Lausanne, Switzerland
• Frank Neven, UHasselt, Data Science Institute, ACSL, Belgium

INTRODUCTION

摘要

快照隔离 (SI) 是一种多版本并发控制算法，最早由 Berenson 等人 [1995] 描述。SI 之所以有吸引力，是因为它提供了一种可以避免许多常见并发异常的隔离级别，并且已由 Oracle 和 Microsoft SQL Server 实现（有一些细微的差别）。SI 并不保证在所有情况下都可序列化，但例如，TPC-C 基准测试应用程序 [TPC-C] 在 SI 下执行时不会出现序列化异常。所有主要数据库系统产品都提供默认的非序列化隔离级别，这些级别通常比 SI 更常遇到序列化异常，我们怀疑许多大型站点每天都会因此发生大量隔离错误，导致数据仓库应用程序中有时会出现损坏的数据。较低隔离级别的经典理由是，当应用程序被证明不会导致严重错误时，可以在这些级别下运行以提高效率，但供应商很少或根本没有向应用程序程序员和 DBA 提供有关如何避免此类错误的指导。本文提出了一种理论，用于描述在 SI 下何时会出现应用程序的非序列化执行。在文章的最后，我们将应用该理论来证明 TPC-C 基准测试应用程序在 SI 下没有序列化异常，然后讨论如何将此证明推广到其他应用程序。我们还讨论了如何修改在 SI 下不可序列化的应用程序的程序逻辑，以保证可序列化性。

作者：

• ALAN FEKETE, University of Sydney
• DIMITRIOS LIAROKAPIS, ELIZABETH O’NEIL, and PATRICK O’NEIL, University of Massachusetts
• DENNIS SHASHA, Courant Institute

MOTIVATION AND PRELIMINARIES