EagleBear2002 的博客

摘要

现代数据库采用弱隔离级别来满足高可用性事务。然而，最近许多生产数据库中都出现了弱隔离错误。这引发了人们对数据库实现是否在实践中真正实现其承诺的隔离保证的担忧。在本文中，我们介绍了 Plume，这是第一个高效、完整的弱隔离级别黑盒检查器。Plume 建立在模块化、细粒度、事务异常模式的基础上，我们利用这些模式建立了代表性弱隔离级别的合理和完整特征，包括读取提交、读取原子性和事务因果一致性。Plume 利用两种技术（向量和树时钟）的新颖组合来加速隔离检查。我们广泛的评估表明，Plume 可以在大量异常数据库执行历史中重现所有已知违规行为，在三个生产数据库中检测新的隔离错误以及信息反例，比最先进的检查器发现更多的弱隔离异常，并在各种工作负载下有效地验证隔离保证。

作者：

• SI LIU, ETH Zurich, Switzerland
• LONG GU, State Key Laboratory for Novel Software Technology, Nanjing University, China
• HENGFENG WEI*, State Key Laboratory for Novel Software Technology, Nanjing University, China
• DAVID BASIN, ETH Zurich, Switzerland

摘要

本文整理了南京大学本科生学号和研究生学号组成规则，并整理了院系专业代码、本科招生专业代码和新生学院各书院之间的对应关系。依照本文的规则，可根据学号判断学生信息。

本科生学号组成

本科生学号由 9 位阿拉伯数字组成。其中：

1. 第 1-2 位表示入学年份，例如 24 表示 2024 年入学；
2. 第 3 位是录取类型代码，其中 1 表示统招，2 表示第二学位，5 表示留学生；
3. 第 4-6 位是招生专业（或大类）代码，其中第 4-5 位是院系代码；
4. 第 7-9 位是流水号，不同书院不同年份可能参考性别、生源地、高考分数、出生日期、录取时间等因素进行排序。

摘要

课程资源概览

• 课程视频资源：https://space.bilibili.com/479141149/channel/collectiondetail?sid=1720732
• 课程幻灯片：https://github.com/courses-at-nju-by-hfwei/cpl-lectures/tree/main
• 教材：《C 语言程序设计：现代方法（第 2 版·修订版）》（ISBN: 9787115565198）
• 课程 oj：校内访问：https://oj.cpl.icu/、校外访问：https://public.oj.cpl.icu/
• 课程讲义：https://ymv59wdgrr.feishu.cn/wiki/A1HzwviAgiFnQwkfRUWcVjqunLf

课程资源结构

摘要

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

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

作者：

摘要

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

作者：

• 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

摘要

虽然可串行化始终保证应用程序的正确性，但可以选择较低的隔离级别来提高事务吞吐量，但风险是引入某些异常。如果在指定的隔离级别下，所有可能的事务交错都是可串行化的，则一组事务对给定的隔离级别具有鲁棒性。因此，鲁棒性始终保证应用程序的正确性，同时具有较低隔离级别的性能优势。虽然鲁棒性问题在文献中受到了广泛关注，但只获得了充分条件。最值得注意的例外是 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

摘要

语法问题

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

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

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

摘要

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

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

作者：

摘要

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

作者：

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

摘要

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

作者：

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