EagleBear2002 的博客

摘要

本文梳理了并发程序一致性的基础知识，以供数据库一致性参考。

$$
\def\po{\mathsf{\textcolor{red}{po}}}
\def\so{\mathsf{\textcolor{purple}{so}}}
\def\wr{\mathsf{\textcolor{teal}{wr}}}
\def\ww{\mathsf{\textcolor{red}{ww}}}
\def\rw{\mathsf{\textcolor{blue}{rw}}}
\def\vis{\mathsf{\textcolor{orange}{vis}}}
\def\arb{\mathsf{\textcolor{pink}{arb}}}
\def\Write{\mathsf{Write}}
\def\Read{\mathsf{Read}}
\def\View{\mathsf{View}}
\def\RelWrites{RelWrites}
\def\MaxRelWrites{MaxRelWrites}
\def\EffWrite{EffWrite}
\def\wk{\mathsf{wk}}
\def\st{\mathsf{st}}
\def\total{\mathsf{total}}
\def\read{read}
\def\write{write}
\def\thru{thru}
\def\back{back}
\def\ANY{\mathtt{ANY}}
\def\ONE{\mathtt{ONE}}
\def\QUORUM{\mathtt{QUORUM}}
\def\ALL{\mathtt{ALL}}
\def\O{\mathcal{O}}
\def\RelTerms{RelTerms}
\def\VisBasic{VisBasic}
$$

摘要

分布式数据存储的开发人员必须牺牲一致性来换取性能和可用性。此类系统实际上可能实现弱一致性模型，例如因果一致性或最终一致性，这对应于不同的成本和对客户端的保证。我们考虑分布式系统的情况，它不仅为客户端提供单一级别的一致性，而且提供多种级别的一致性。这对应于许多实际情况。例如，流行的数据存储（如 Amazon DynamoDB 和 Apache 的 Cassandra）允许应用程序在同一会话中使用单独的一致性级别标记每个查询。在本文中，我们为多级一致性规范提供了一个正式框架，并解决了检查计算是否符合此类规范的问题。我们为这个问题提供了一种原则性的算法方法，并将其应用于具有多级一致性的模型的几个实例。

作者：

Ahmed Bouajjani^1^, Constantin Enea^1^, Madhavan Mukund^2,3^, Gautham Shenoy R.^2^, and S. P. Suresh ^2,3^

教材 P239，11 题

综合实验：用 Find Security Bugs （http://find-sec-bugs.github.io）工具静态分析 WebGoat。WebGoat 是 OWASP 组织研制出的用于进行 Web 漏洞实验的应用平台，官方网址是 http://www.owasp.org.cn/owasp-project/webscan-platform。WebGoat 运行在带有 Java 虚拟机的平台之上，当前提供的训练课程有 30 多个，其中包括：跨站点脚本攻击（XSS）、访问控制、线程安全、操作隐藏字段、操纵参数、弱会话 Cookie、SQL 盲注、数字型 SQL 注入、字符串型 SQL 注入和 Web 服务等。完成实验报告。

Clone WebGoat 源码

1

git clone git@github.com:WebGoat/WebGoat.git

下载 Find Security Bugs 插件

教材 P239，15 题

综合实验：使用 American Fuzzy Lop（http:/lcamtuf.coredump.cx/afl/）工具挖掘 C/C++程序漏洞。完成实验报告。

实验环境：WSL2

配置 American Fuzzy Lop

1
2
3
4
5
6

wget http://lcamtuf.coredump.cx/afl/releases/afl-2.52b.tgz
tar -zxvf afl-2.52b.tgz
cd afl-2.52b/
make
sudo make install
afl-fuzz

RAG-arXiv 实验开源地址：https://github.com/EagleBear2002/RAG-arXiv

Agent-course 实验开源地址：https://github.com/EagleBear2002/Agent-course

$$
\def\ReadSet{\mathsf{ReadSet}}
\def\WriteSet{\mathsf{WriteSet}}
\def\Attr{\mathsf{Attr}}
\def\Account{Account}
\def\Savings{Savings}
\def\Checking{Checking}
\def\Balance{Balance}
\def\Amalgamate{Amalgamate}
\def\Var{\mathsf{Var}}
\def\Tuples{\mathsf{Tuples}}
\def\prefix{\mathsf{prefix}}
\def\postfix{\mathsf{postfix}}
\def\ww{\mathsf{ww}}
\def\rw{\mathsf{rw}}
\def\wr{\mathsf{wr}}
\def\pcfg{\mathsf{prefix-conflict-free-graph}}
\def\R{\mathsf{R}}
\def\W{\mathsf{W}}
\def\U{\mathsf{U}}
\def\t{\mathsf{t}}
\def\v{\mathsf{v}}
\def\T{\mathcal{T}}
\def\P{\mathcal{P}}
\def\D{\mathrm{D}}
\def\C{\mathrm{C}}
$$

摘要

众所周知，许多数据库系统提供的隔离级别多版本读取已提交 (RC) 会牺牲一致性来换取更高的事务吞吐量。有时，事务工作负载可以在 RC 下安全执行，以较低的 RC 成本获得完美的可序列化隔离。为了识别这种情况，我们引入了一个事务程序的表达模型，以更好地推理事务工作负载的可序列化性。**我们开发了易处理的算法来决定在 RC 下执行的工作负载的任何可能调度是否可序列化（称为稳健性问题）。**我们的方法产生的稳健子集比以前的方法识别的子集更大。我们提供实验证据表明，与更强的隔离级别相比，在 RC 下可以更快地评估对 RC 具有稳健性的工作负载。我们讨论了通过将选择性读取操作提升为更新来使工作负载对 RC 具有稳健性的技术。根据场景的不同，性能改进可能相当可观。因此，在较低的隔离级别 RC 下进行稳健性测试和安全地执行事务可以提供一种直接的方法来增加事务吞吐量，而无需更改 DBMS 内部结构。

作者：

• 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

$$
\def\put{\mathrm{put}}
\def\get{\mathrm{get}}
\def\rem{\mathrm{rem}}
\def\inv
\def\ret
\def\hb
\def\lin
$$

摘要

多线程程序通常依赖高效且线程安全的并发对象，如集合、键值映射和队列。虽然一些并发对象的操作被设计为原子性行为，见证其在线性化顺序中的前驱操作的原子效果，但其他操作为了避开复杂的控制和同步瓶颈而放弃了这种强一致性。例如，键值映射的 contains(value) 方法可能在不阻塞并发更新的情况下遍历键值条目，以避免不必要的性能瓶颈，因此可能会忽略某些在线性化顺序上的前驱操作的效果。尽管这些弱一致性的操作可能不具备原子性，但它们仍然提供了一些保证，比如只观察到已经存在的值。

在这项工作中，我们开发了一种方法来证明并发对象实现遵循弱一致性规范。特别是，我们考虑了对放宽可见性规范的（前向）模拟证明，允许指定的操作忽略它们的一些线性化顺序上的前驱操作，即表现得好像这些操作从未发生过一样。除了标注实现代码以识别逻辑效应发生的点（即操作的线性化点），我们还标注代码以识别可见操作，即那些效果被观察到的操作；实际上，这种标注可以通过跟踪每个访问内存位置的写入者自动完成。我们在一个通用的状态转换系统概念上形式化了我们的方法论，该概念独立于任何特定的编程语言或内存模型，并展示了其应用。

Introduction

$$
\def\po{\mathsf{\textcolor{red}{po}}}
\def\so{\mathsf{\textcolor{purple}{so}}}
\def\soo{\mathsf{\textcolor{purple}{soo}}}
\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\SO{\mathsf{\textcolor{purple}{SO}}}
\def\WR{\mathsf{\textcolor{teal}{WR}}}
\def\CM{\mathsf{\textcolor{orange}{CM}}}
\def\CO{\mathsf{\textcolor{brown}{CO}}}
\def\AR{\mathsf{\textcolor{pink}{AR}}}
\def\vis{\mathsf{\textcolor{orange}{vis}}}
\def\VIS{\mathsf{\textcolor{orange}{VIS}}}
\def\hb{\mathsf{\textcolor{pink}{hb}}}
\def\hbo{\mathsf{\textcolor{pink}{hbo}}}
\def\A{\mathsf{A}}
\def\E{\mathsf{E}}
\def\cc{\mathsf{cc}}
\def\ec{\mathsf{ec}}
\def\sc{\mathsf{sc}}
\def\rc{\mathsf{rc}}
\def\mav{\mathsf{mav}}
\def\rr{\mathsf{rr}}
\def\sameobj{\mathsf{sameobj}}
\def\oper{\mathsf{oper}}
\def\txn{\mathsf{txn}}
\def\sametxn{\mathsf{sametxn}}
\def\withdraw{\mathtt{withdraw}}
\def\deposit{\mathtt{deposit}}
\def\getBalance{\mathtt{getBalance}}
\def\heta{\hat{\eta}}
\def\RYW{\mathbf{RYW}}
\def\MR{\mathbf{MR}}
\def\MW{\mathbf{MW}}
\def\WFR{\mathbf{WFR}}
$$

摘要

面向用户的在线服务采用地理分布的数据存储来减少延迟并容忍部分故障，以提供快速且始终可用的体验。然而，地理分布并非没有代价；应用程序开发者需要处理弱一致性行为，并且缺乏构建高级复制数据类型的抽象机制，这导致了复杂的应用程序逻辑，并不可避免地将不一致性暴露给用户。一些商业分布式数据存储和多个学术提案提供了一致性级别的层次结构，更强的一致性保证会带来更高的延迟和吞吐量成本。然而，正确为操作分配合适的一致性级别需要细致的推理，并且通常是一个容易出错的任务。

在本文中，我们提出了 QUELEA，一种针对最终一致性的数据存储（ECDS）的声明式编程模型，它配备了一种契约语言，能够指定细粒度的应用层一致性属性。一个契约执行系统分析这些契约，并自动生成受保护方法所需的一致性协议。我们在一个现成的支持无协调事务的 ECDS 之上实现了 QUELEA。通过包括两个大型网络应用在内的几个基准测试，展示了我们的方法的有效性。

**关键词：**最终一致性、可用性、CRDT、公理合约、合约分类、分布式事务、SMT 求解器、可判定逻辑、Quelea、Cassandra、Haskell

$$
\def\po{\mathsf{\textcolor{red}{po}}}
\def\so{\mathsf{\textcolor{purple}{so}}}
\def\hbs{\mathsf{hbs}}
\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\SO{\mathsf{\textcolor{purple}{SO}}}
\def\WR{\mathsf{\textcolor{teal}{WR}}}
\def\CM{\mathsf{\textcolor{orange}{CM}}}
\def\CO{\mathsf{\textcolor{brown}{CO}}}
$$

摘要

有效的软件规格说明能够支持模块化推理，允许客户端在不了解模块实现细节的情况下建立程序属性。虽然一些模块的操作表现得像原子操作一样，但其他模块为了提高性能而采用了较弱的一致性。由于当前的方法无法捕捉到具有不同非原子一致性水平的操作所提供的保证，因此规格说明变得无效，失去了为调用非原子操作的程序建立属性的能力。

在这项工作中，我们开发了一种方法来指定那些操作满足多个不同一致性级别的软件模块。特别是，我们开发了一个简单的注释语言，通过可见性放松来指定弱一致性操作，在这种注释中对操作之间的可见性施加了不同的约束。为了与现代软件平台集成，我们识别了一种新的称为“顺序发生前一致性”的一致性特性，它允许有效验证。实验上，我们通过推导和验证 Java 并发对象的放松可见性规格说明，展示了我们方法的有效性。此外，我们还通过实验证明了我们的注释语言是优化的，即使更细粒度的语言也不能为 Java 对象提供更强的规格说明。

作者：

摘要

本文记录了南京大学师生免费领取华为云云主机的步骤，以供参考。

领取步骤

1. 手机下载“华为云 APP”并注册、登录；
2. 使用“华为云 APP”扫描文档中的二维码（本文不提供二维码）；
3. 自动跳转云主机领取配置页面（这一步骤需要时间，请耐心等待）；