EagleBear2002 的博客

\[ \def\read{\mathsf{read}} \def\write{\mathsf{write}} \def\reads{\mathsf{reads}} \def\writes{\mathsf{writes}} \def\Writes{\mathsf{Writes}} \def\SER{\mathsf{SER}} \def\SI{\mathsf{SI}} \def\PC{\mathsf{PC}} \def\CC{\mathsf{CC}} \def\RC{\mathsf{RC}} \def\RA{\mathsf{RA}} \def\po{\mathsf{\textcolor{red}{po}}} \def\so{\mathsf{\textcolor{purple}{so}}} \def\wr{\mathsf{\textcolor{green}{wr}}} \def\co{\mathsf{\textcolor{orange}{co}}} \def\SO{\mathsf{\textcolor{purple}{SO}}} \def\VIS{\mathsf{\textcolor{green}{VIS}}} \def\antiVIS{\mathsf{\overline{\VIS^{-1}}}} \def\AR{\mathsf{\textcolor{green}{AR}}} \def\CO{\mathsf{\textcolor{orange}{CO}}} \def\WR{\mathsf{\textcolor{green}{WR}}} \def\WW{\mathsf{\textcolor{blue}{WW}}} \def\RW{\mathsf{\textcolor{cyan}{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\Executions{\mathsf{Executions}} \def\modelOf{\mathsf{modelOf}} \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}}\def\read{\mathsf{read}} \def\write{\mathsf{write}} \def\reads{\mathsf{reads}} \def\writes{\mathsf{writes}} \def\Writes{\mathsf{Writes}} \def\SER{\mathsf{SER}} \def\SI{\mathsf{SI}} \def\PC{\mathsf{PC}} \def\CC{\mathsf{CC}} \def\RC{\mathsf{RC}} \def\RA{\mathsf{RA}} \def\po{\mathsf{\textcolor{red}{po}}} \def\so{\mathsf{\textcolor{purple}{so}}} \def\wr{\mathsf{\textcolor{green}{wr}}} \def\co{\mathsf{\textcolor{orange}{co}}} \def\SO{\mathsf{\textcolor{purple}{SO}}} \def\VIS{\mathsf{\textcolor{green}{VIS}}} \def\antiVIS{\mathsf{\overline{\VIS^{-1}}}} \def\AR{\mathsf{\textcolor{green}{AR}}} \def\CO{\mathsf{\textcolor{orange}{CO}}} \def\WR{\mathsf{\textcolor{green}{WR}}} \def\WW{\mathsf{\textcolor{blue}{WW}}} \def\RW{\mathsf{\textcolor{cyan}{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\Executions{\mathsf{Executions}} \def\modelOf{\mathsf{modelOf}} \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}} \]

摘要

对数据库的并发访问通常封装在事务中，以便与其他并发计算隔离并具有对故障的恢复能力。现代数据库为事务提供了各种语义，这些语义对应于一致性和可用性之间的不同权衡。由于较弱的一致性模型提供了更好的性能，因此一个重要的问题是研究给定程序所需的最弱一致性级别（以满足其规范）。作为处理此问题的一种方法，我们研究了在用较弱的一致性模型替换一致性模型时检查给定程序是否具有相同的行为集的问题。这种称为鲁棒性的属性通常意味着在削弱一致性时程序的任何规范都会得到保留。我们专注于比标准可序列化性更弱的一致性模型的鲁棒性问题，即因果一致性、前缀一致性和快照隔离。我们表明，检查这些模型之间的鲁棒性是多项式时间可归结为可序列化下的状态可达性问题。我们还使用这种归结来推导一种基于 Lipton 归结理论的实用证明技术，该技术可以证明程序是鲁棒的。我们已经将我们的技术应用于分布式系统和数据库文献中的几个具有挑战性的应用。

Introduction

对数据库的并发访问通常封装在事务中，以便与其他并发计算隔离并具有故障恢复能力。现代数据库为事务提供了各种语义，对应于一致性和可用性之间的不同权衡。最强的一致性级别是通过可序列化事务 [42] 实现的，其并发执行的结果与事务按某种顺序原子执行的结果相同。由于可序列化 (SER) 会严重损害可用性，现代数据库通常提供较弱的一致性模型，例如因果一致性 (CC) [38]、前缀一致性 (PC) [22, 25] 和快照隔离 (SI) [12]。因果一致性要求，如果事务 t1“影响”另一个事务 t2，例如，t1 在同一会话中在 t2 之前执行，或者 t2 读取了 t1 写入的值，则这两个事务中的更新可以被按此顺序的任何其他事务观察到。并发事务彼此之间没有因果关系，因此可以以不同的顺序观察到这些事务，从而导致 SER 下不可能出现的行为。前缀一致性要求所有事务之间存在一个总提交顺序，以便每个事务都能观察到此序列前缀中的所有更新（PC 强于 CC）。 两个事务可以观察到相同的前缀，从而导致 SER 不允许的行为。快照隔离进一步要求，如果两个不同的事务都写入一个公共变量，则它们会观察到不同的前缀。

\[ \def\read{\mathsf{read}} \def\write{\mathsf{write}} \def\reads{\mathsf{reads}} \def\writes{\mathsf{writes}} \def\Writes{\mathsf{Writes}} \def\SER{\mathsf{SER}} \def\SI{\mathsf{SI}} \def\PC{\mathsf{PC}} \def\CC{\mathsf{CC}} \def\RC{\mathsf{RC}} \def\RA{\mathsf{RA}} \def\po{\mathsf{\textcolor{red}{po}}} \def\so{\mathsf{\textcolor{purple}{so}}} \def\wr{\mathsf{\textcolor{green}{wr}}} \def\co{\mathsf{\textcolor{orange}{co}}} \def\SO{\mathsf{\textcolor{purple}{SO}}} \def\VIS{\mathsf{\textcolor{green}{VIS}}} \def\antiVIS{\mathsf{\overline{\VIS^{-1}}}} \def\AR{\mathsf{\textcolor{green}{AR}}} \def\CO{\mathsf{\textcolor{orange}{CO}}} \def\WR{\mathsf{\textcolor{green}{WR}}} \def\WW{\mathsf{\textcolor{blue}{WW}}} \def\RW{\mathsf{\textcolor{cyan}{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\Executions{\mathsf{Executions}} \def\modelOf{\mathsf{modelOf}} \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}} \]

摘要

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

Introduction

为了实现可扩展性和可用性，现代互联网服务通常依赖于大型数据库，这些数据库在大量节点和/或广阔的地理跨度上复制和分区数据（例如，[14、20、26、3、6、4、5、11、22、27、10]）。数据库客户端在任何节点上调用数据事务，节点之间使用消息传递相互传达更改。理想情况下，我们希望这个分布式系统能够提供关于事务处理的强保证，例如可序列化性 [8]：如果这些事务按某种顺序串行执行，则可以获得并发执行一组事务的结果。可序列化性很有用，因为它允许应用程序程序员轻松建立所需的正确性属性。例如，要检查应用程序的事务是否保留给定的数据完整性约束，程序员只需检查每个事务在单独执行时是否都保留了约束，而不必担心并发性。不幸的是，实现可串行化需要数据库节点之间进行过多的同步，这会减慢数据库的速度，甚至在副本之间的网络连接失败时导致数据库不可用 [17, 1]。因此，如今的大型数据库通常提供弱一致性保证，这允许非串行化行为，称为异常。

\[ \def\read{\mathsf{read}} \def\write{\mathsf{write}} \def\reads{\mathsf{reads}} \def\writes{\mathsf{writes}} \def\Writes{\mathsf{Writes}} \def\SER{\mathsf{SER}} \def\SI{\mathsf{SI}} \def\PC{\mathsf{PC}} \def\CC{\mathsf{CC}} \def\RC{\mathsf{RC}} \def\RA{\mathsf{RA}} \def\po{\mathsf{\textcolor{red}{po}}} \def\so{\mathsf{\textcolor{purple}{so}}} \def\wr{\mathsf{\textcolor{green}{wr}}} \def\co{\mathsf{\textcolor{orange}{co}}} \def\SO{\mathsf{\textcolor{purple}{SO}}} \def\VIS{\mathsf{\textcolor{green}{VIS}}} \def\antiVIS{\mathsf{\overline{\VIS^{-1}}}} \def\AR{\mathsf{\textcolor{green}{AR}}} \def\CO{\mathsf{\textcolor{orange}{CO}}} \def\WR{\mathsf{\textcolor{green}{WR}}} \def\WW{\mathsf{\textcolor{blue}{WW}}} \def\RW{\mathsf{\textcolor{cyan}{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\Executions{\mathsf{Executions}} \def\modelOf{\mathsf{modelOf}} \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}} \]

摘要

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

作者：

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

摘要

分布式存储系统和数据库被各种类型的应用程序广泛使用。对这些存储系统的事务访问是一种重要的抽象，它允许应用程序程序员将操作块（即事务）视为原子执行。出于性能原因，现代数据库实现的一致性模型比标准可序列化模型弱，后者对应于在顺序一致内存上执行的事务的原子性抽象。例如，因果一致性就是在实践中广泛使用的此类模型之一。

在本文中，我们研究了因果一致性的几种变体之间的特定于应用程序的关系，并解决了自动验证给定事务程序是否对因果一致性具有鲁棒性的问题，即在任意因果一致数据库上执行时，其所有行为都是可序列化的。我们表明，没有 ww 竞争的程序在所有这些变化下都具有相同的行为集，并且我们表明，检查鲁棒性是多项式时间可归结为顺序一致共享内存上事务程序的状态可达性问题。后一个结果的一个令人惊讶的推论是，允许不可比较的行为集的因果一致性变体允许可比较的稳健程序集。这种简化还为利用现有的并发程序验证方法和工具（假设顺序一致性）来推理在因果一致的数据库上运行的程序打开了大门。此外，它允许确定当在不同站点执行的程序是有限状态时，检查稳健性的问题是可判定的。

作者：

• Sidi Mohamed Beillahi, Université de Paris, IRIF, CNRS, F-75013 Paris, France
• Ahmed Bouajjani, Université de Paris, IRIF, CNRS, F-75013 Paris, France
• Constantin Enea, Université de Paris, IRIF, CNRS, F-75013 Paris, France

\[ \def\read{\mathsf{read}} \def\write{\mathsf{write}} \def\reads{\mathsf{reads}} \def\writes{\mathsf{writes}} \def\SER{\mathsf{SER}} \def\SI{\mathsf{SI}} \def\PC{\mathsf{PC}} \def\CC{\mathsf{CC}} \def\RC{\mathsf{RC}} \def\RA{\mathsf{RA}} \def\po{\mathsf{\textcolor{red}{po}}} \def\so{\mathsf{\textcolor{purple}{so}}} \def\wr{\mathsf{\textcolor{green}{wr}}} \def\co{\mathsf{\textcolor{orange}{co}}} \def\SO{\mathsf{\textcolor{purple}{SO}}} \def\VIS{\mathsf{\textcolor{green}{VIS}}} \def\CO{\mathsf{\textcolor{orange}{CO}}} \def\WR{\mathsf{\textcolor{green}{WR}}} \def\WW{\mathsf{\textcolor{blue}{WW}}} \def\RW{\mathsf{\textcolor{cyan}{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

摘要

流行的隔离级别多版本读已提交 (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

摘要

图片来自：【图解电视】《大明王朝 1566》第一集|徐阶|高拱|严嵩|张居正_网易订阅 (163.com)

第一集：出场人物

周云逸：钦天监监正

周云逸，钦天监监正，正五品。职能为掌观察天象，推算节气，制定历法。

摘要

流行的隔离级别多版本读已提交（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