Step 1

题目摘要引言

Title

IPA, Invariant-Preserving Applications 不变式保护应用

针对弱一致性备份数据库

Abstract

High availability -> Weakly consistent replication -> concurrent updates lead to states where application invariants do not hold -> difficulty in identifying conflict operations.

A new approach: preserve application invariants without coordinatig the execution of operations

How to modify

• No conflicting updates -> original semantics
• Otherwise -> sensible and deterministic conflict resolution policies

实现方法

Develop a static analysis, IPA, that identifies conflicting operation and proposes

Introduction

Systems replicated in geographical regions often adopt weak consistency.

不过这种方法会向客户暴露临时的状态差异（temporary state divergence）从而使应用开发变得更加困难。一些改进方法：

• CRDTs: conflict-free replicated date types
• Causal Consistency: 根据 happen-before 关系，操作是可见的
• highly available transactions: 高可用 transaction，将多个操作 group 到一起立即实施

尽管有这些办法，但开发保证 weak consistency 的应用仍然很困难。

仍然以游戏中并发（concurrent）的执行 enroll 和 removetournament 为例。

一些系统提供了用于同步执行操作的原语（这里提到了诚哥 OSDI 12' 的文章 ），仅在需要时进行 coordination。但是很难确定有问题的执行，使得程序员往往为了保持正确性而过多地限制并发性，从而影响性能。

A new approach:

key idea: extend operations with updates that preventively guarantee the preservation of invariants in the presence of concurrent updates

这些 extend operation 在非并发执行时不应该有任何可见效果，保持操作的语义等同于线性执行，而在需要纠正并发执行的不良语义时生效。

在之前游戏并发 enroll 和 removetournament 的示例中，可通过恢复 remove 操作来维护引用的完整性（这应该算是 invariant？）enroll 会附加组织并发删除 tournament 的更新。

为了帮助程序员采用我们的方法，我们提出了一种修改应用程序的方法。该方法的关键元素是我们的不变量保持分析(IPA)和静态分析工具，它依赖于应用程序的信息，包括变量和操作，以识别哪些操作可能导致不变量违反，并建议对操作进行修改，以防止这些违反发生。以前的工作利用静态分析来优化在弱一致性下运行的应用程序中的协调使用（这里提到了 EuroSys 15'）。对比而言，本文提出的方法不需要通过 resort（或额外机制）来避免冲突操作的并发执行，而是允许操作的并发执行，并利用冲突解决策略来保证结果是确定的（对于给定的并发操作而言）并保证不变性。

方法 Threefold:

（补充 OLTP: Online transaction processing ）

• First：分析一些 benchmark 和 OLTP 应用，通过文章的方法可以确定最常见的关系型数据库不变量冲突，并且在建议的修改在并发环境下显现出正确、确定性语义。
• Second：需要修改后的操作在没有冲突并发执行时，语义等同于原始执行
• Third： 实验结果表明，小负担的修改提供了比最先进解决方法更快速高效的表现

Contribution

1. （提出方法，IPA 原理）a novel approach to preserve invariants under weak consistency without resorting to coordination which combines the extension of operations an algorighm that use of appropriate conflict resulution policies 提出一种不进行 resorting 而是更新操作的解决弱一致性下并发操作冲突的方法
2. （设计算法，IPA 实现）an algorithm that takes information about operations and application invariants and proposes modifications to operations and conflict resolution policies to preserve invariants while keeping the original semantics of the operations in the absence of conflicts. 提供一种算法有用以从操作和应用不变量中提取信息，并提出对操作进行修改和冲突解决策略，以保证不变式，同时在不存在冲突的情况下保持操作的原始语义。
3. the design of new CRDTs(conflict-free replicated date types) that support the conflict resolution policies necessary for adopting our approach 结合文中方法支持冲突解决策略的新的 CRDTs 设计
4. an implementation and evalutaion of the proposed approach 针对所提出方法的实现与评估

基本理论概况

结论部分

Supporting correct and highly available applications on top of weak consistency.

通过拓展操作（带有额外效果）可以保证任何时候不变量都可以保持且有明确的语义。IPA 分析和工具帮助程序员通过静态分析的方式确定哪些操作会在并发执行时产生冲突，并且给出修改操作的建议。

回答基本问题

1. 类别

   对现有系统（Weak Consistency下的OLTPs）的改进

2. 内容

   与之相关的 Explicit Consistency, RedBlue Consistency.

3. 正确性

   离线静态分析是高效的

4. 创新点

5. 清晰度

阅读选择

继续阅读

Step 2

细读笔记

问题记录

未读（且值得读）文献记录

Step 3

思路复现

证明与推理复现

实验验证复现