\[ \def\ran{\text{ran}} \def\FUN{\mathsf{FUN}} \]
习题 1：证明设 \(A\) 为传递集合，则 \(A^+\) 也是传递集合。
证明：由 \(A\) 的传递性可知，\(\forall a \in A, a \subseteq A\)。取任意 \(b \in A^+\)，只要证明 \(b \subseteq A^+\)。
\(A^+\) 是 \(A\) 的后继（此处右上角的 \(+\) 并不是传递闭包），即 \(A^+ = A \cup \set{A}\)。
- 若 \(b \in A\) 则 \(b \subseteq A \subseteq A^+\)；
- 若 \(b \notin A\) 则 \(b = A\)，此时 \(b \subseteq A^+\) 成立。
\(Q.E.D.\)
习题 2：证明对任意自然数 \(n\)，都有 \(0 = n\) 或 \(0 \in n\)。
\[ \def\len{\mathsf{len}} \]
习题 1：设 \(\alpha\) 为基数，\(\kappa\) 为集合 \(\set{\beta | \beta 是序数且与 \alpha 等势}\) 的最小元。证明：\(\kappa\) 是基数。
证明：对每个序数 \(\gamma < \kappa\)，即 \(\gamma \in \kappa\)，有 \(\gamma \subseteq \kappa\)，即 \(\gamma \prec \kappa\) 或 \(\gamma \sim \kappa\)。
又因为 \(\kappa\) 为集合中最小元，因此 \(\gamma \prec \kappa\)。
\(Q.E.D.\)
\[ \def\P{\mathcal{P}} \def\Tr{\mathsf{Tr}} \def\HB{\mathsf{HB}} \def\PO{\mathsf{\textcolor{black}{PO}}} \def\SO{\mathsf{\textcolor{purple}{SO}}} \def\WR{\mathsf{\textcolor{green}{WR}}} \def\WW{\mathsf{\textcolor{red}{WW}}} \def\RW{\mathsf{\textcolor{blue}{RW}}} \def\CO{\mathsf{\textcolor{orange}{CO}}} \def\ARB{\mathsf{\textcolor{orange}{ARB}}} \def\CC{\mathtt{CC}} \def\PC{\mathtt{PC}} \def\SI{\mathtt{SI}} \def\SER{\mathtt{SER}} \def\assume{\mathtt{assume}} \def\cs{\_\clubsuit} \def\CountTickets{\mathtt{CountTickets}} \def\Register{\mathtt{Register}} \def\CreateEvent{\mathtt{CreateEvent}} \def\assume{\mathtt{assume}} \]
摘要
对数据库的并发访问通常封装在事务中，以便与其他并发计算隔离并具有对故障的恢复能力。现代数据库为事务提供了各种语义，这些语义对应于一致性和可用性之间的不同权衡。由于较弱的一致性模型提供了更好的性能，因此一个重要的问题是研究给定程序所需的最弱一致性级别（以满足其规范）。作为处理此问题的一种方法，我们研究了在用较弱的一致性模型替换一致性模型时检查给定程序是否具有相同的行为集的问题。这种称为鲁棒性的属性通常意味着在削弱一致性时程序的任何规范都会得到保留。我们专注于比标准可序列化性更弱的一致性模型的鲁棒性问题，即因果一致性、前缀一致性和快照隔离。我们表明，检查这些模型之间的鲁棒性是多项式时间可归结为可序列化下的状态可达性问题。我们还使用这种归结来推导一种基于 Lipton 归结理论的实用证明技术，该技术可以证明程序是鲁棒的。我们已经将我们的技术应用于分布式系统和数据库文献中的几个具有挑战性的应用。
作者：
\[ \def\Tuples{\mathbf} \def\ReadSet{\mathsf} \def\WriteSet{\mathsf} \def\prefix{\mathsf{prefix}} \def\postfix{\mathsf{postfix}} \def\pcfg{\textrm{prefix-confilct-free-graph}} \def\R{\mathsf{R}} \def\W{\mathsf{W}} \def\U{\mathsf{U}} \def\C{\mathsf{C}} \def\t{\mathsf{t}} \def\v{\mathsf{v}} \def\T{\mathcal{T}} \def\I{\mathcal{I}} \def\P{\mathcal{P}} \]
摘要
虽然可串行化始终保证应用程序的正确性，但可以选择较低的隔离级别来提高事务吞吐量，但风险是引入某些异常。如果在指定的隔离级别下，所有可能的事务交错都是可串行化的，则一组事务对给定的隔离级别具有鲁棒性。因此，鲁棒性始终保证应用程序的正确性，同时具有较低隔离级别的性能优势。虽然鲁棒性问题在文献中受到了广泛关注，但只获得了充分条件。最值得注意的例外是 Fekete 的开创性工作，他获得了确定针对 SI 的鲁棒性的特征。在本文中，我们解决了较低 SQL 隔离级别 RU 和 RC 的鲁棒性问题，它们是根据禁止的脏写和脏读模式定义的。本文的第一个主要贡献是，我们根据特定形式（拆分和多拆分调度 ）的反例调度 的缺失以及满足各种属性的干涉图中的环的缺失来表征针对这两个隔离级别的鲁棒性。与 Fekete 的工作的一个关键区别是，本文获得的环属性必须考虑事务内操作的相对顺序，因为 RU 和 RC 不满足原子可见性要求。一个特殊的结果是后者导致了针对 RC coNP-complete 的鲁棒性问题。本文的第二个主要贡献是 coNP-hardness 证明。对于 RU，我们获得了 LOGSPACE-completeness。
作者：
摘要
摘要
明确句式结构，特别要注意主语问题。反例：
数字经济学科推荐书目为《第三次工业革命》和《第二次机器革命》，知科技前沿，晓时代发展，通中国国情。（错误）
整句话按照语法缩句为“数字经济学科知科技前沿……”，应该修改为：
\[ \def\SER{\mathsf{SER}} \def\PSI{\mathsf{PSI}} \def\SI{\mathsf{SI}} \def\PC{\mathsf{PC}} \def\CC{\mathsf{CC}} \def\RC{\mathsf{RC}} \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\so{\mathsf{\textcolor{purple}{so}}} \def\wr{\mathsf{\textcolor{green}{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\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\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\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\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 下运行时的行为相同。
作者：
摘要
事务稳健性问题围绕着决定对于给定的工作负载，低于 SER 的隔离级别是否足以保证可序列化性。本文提出了针对隔离级别（多版本）读取已提交的稳健性的新特征。它支持具有控制结构（循环和条件）以及插入、删除和谓词读取的事务程序 - 触发幻影问题的场景，众所周知，幻影问题在这种情况下很难分析。该特征是图论性的，与数据库研究人员和实践者熟悉的并发控制文献中已知的先前决策机制并无不同。我们通过实验表明，我们的特征突破了界限，允许识别比以前更复杂的工作负载。
作者：