POPL16——Reasoning-about-Consistency-Choices-in-Distributed-Systems

Step 1

题目摘要引言

Title

Reasoning about Consistency Choices in Distributed Systems

针对分布式系统（Replicated Database）中的一致性选择（操作）进行推理。

数学建模，形式描述，并推理哪些需要强一致性保证，哪些不需要。

Abstract

Proof rule -> choice of consistency guarentees

modular: reasoning about the behaviour of every operation seperately under some assumption (on the behaviour of other operations)

SMT-based tool

Introduction

  • Strong Consistency
    • 容易理解，因为行为表现与一台中心节点无异。
    • synchronisation burden
  • Eventually Consistency
    • eschew synchronisation
    • propagate effect eventually
    • lead to anomalies
  • Causal Consistency
    • all replica see causally dependent events (the same order)
    • allow concurrent posts show in different order

all about order: ordering of actions

a list of related research and commercial databases provide Hybrid consistency model.

take the banking application as an example, 为了保护 integrity invariant （在这里是账户余额非负）

  • withdrawal operations - strong consistency (with synchronise)
  • deposit operations - causal consistency (without synchronise)

为了达到混合一致性中强弱的巧妙平衡，增加了程序员的人工负担，需要根据程序的语义进行推理。考虑

  • 特定一致性下所禁止的 anomalies
  • 以及禁止某些 anomalies 能否保证正确性

并发使得困难更加复杂——必须考虑并发执行的操作之间大量可能的交互。

基本理论概况

解决方案：proof rule and tool

contribution：

  • generic hybrid consistency
    • causal consistency by default
    • add op pairs constriction, which pairs of ops may not execute without synchronisation by means of conflict relation
    • Exp. any pair of withdrawal ops in the banking application

！这种形式化描述，每一个 conflict relation 对应了上文中提到的一种增强一致性模型（本人注：如果这个关系是满的，则对应了强一致性，即任意两操作都要求同步）

而文中提出的 proof rule 是针对用 conflict relation 来描述的 general consistency model。

Section 3 形式化描述 general model，Section 4 描述 proof rule.

Section 5 介绍了 proof rule 的模块化性质，允许处理单个 replica？

Section 6 介绍了一个工具出行，使用 SMT 来检查。

结论部分

我们提出了第一个证明规则，该规则确定在复制的数据库中给定的一致性选择足以保留给定的完整性不变性。模块化、易于使用，并使用 SMT checks 来约简验证条件。

实验结果，为大规模推理验证 replicated database 提供了基础。

Future work

  • 没有现有数据库实现文章提出的 generic consistency model，文章只是用通用形式匹配了现有的实现形式。这个通用模型，可能会成为探索其他可能存在的 hybrid consistency model 的基础。
  • proof rule 的健全性建立在至少保证 causal consistency。未来可能探索不保证 causal 的更弱模型。拓展到更多 expressive correctness properties
  • event-based proof -> state-based one 相关？（不太理解）

回答基本问题

  1. 类别

    对现有系统进行分析

  2. 内容

    并没有

  3. 正确性

    待定

  4. 创新点

    针对分布式系统一致性模型提出一个通用模型进行匹配，并给出针对性的推理规则。

  5. 清晰度

    比较清晰。

阅读选择

继续阅读，了解至形式化描述 general consensus model 和 proof rule。

Step 2

细读笔记

Consistency Model, Informally

Causal Consistency and Its Implementation

\(\mathsf{State}\)表示为数据库可能状态的集合。应用定义了一组操作\(\mathsf{Op} = \{o,\cdots\}\)。为了简化，操作总会种植并且返回但值，并约定无返回值\(\bot \in \mathsf{Val}\)。

操作语义的描述，given by a function

\[\mathcal{F} \in \mathsf{Op} \rightarrow (\mathsf{State} \rightarrow ( \mathsf{Val} \times (\mathsf{State} \rightarrow \mathsf{State})))\]

好吧我开始晕了。。。注一下，这个右边是个整体。该函数接受一个具体操作，一个当前状态，获得一个返回值和一个，状态转移函数（这里很有趣，为什么不直接写成后状态而保留这个转移呢）。

为了方便阅读\(o \in \mathsf{Op}\)，我们用\(\mathcal{F}_o\) 写法代替 \(\mathcal{F}(o)\)，这样淡化了第一个参数，表明是\(o\)操作的“效果”。并发导致困难复杂——必须考虑并发执行的操作之间大量可能的交互。

\[\forall o, \sigma . \mathcal{F}_o(\sigma) = ( \mathcal{F}_o^{\mathsf{val}}(\sigma) , \mathcal{F}_o^{\mathsf{eff}}(\sigma) )\]

对于一个给定状态，\(\mathcal{F}_o^{\mathsf{val}}(\sigma) \in \mathsf{Val}\)，表示的操作后的返回值，而\(\mathcal{F}_o^{\mathsf{eff}}(\sigma) \in \mathsf{State} \times \mathsf{State}\)表示其影响。

函数效果对发出消息的 replica 是立即的，而对于其他 replica 是接受消息后产生影响。这一点很关键。

这里用一个很关键的例子（两种 interest 的语义）来引出交换性。

Strengthening Consistency

针对非负的 invariant 语义要求

\[I = \{ \sigma | \sigma \ge 0\}\]

试想 withdraw 操作加入检测

\[\mathcal{F}_{\mathsf{withdraw\mathnormal{(a)}}} (\sigma) = \mathrm{if} ~\sigma \ge a~ \mathrm{then}~ (\checkmark, (\lambda \sigma'.\sigma' - a)) ~\mathrm{else}~(\times,\mathsf{skip})\]

当所有操作都在同一台机器上进行时，这一限制足够，但是多 replica 的情形下却不行（该条件检测判断的是当前状态，并不能预知其他 replica 所携带的金额变动信息）。并发操作可能在彼此没有意识到情况下对数据库进行更新，从而破坏不变式。

明确指定哪些操作不能以并发方式执行，模型中加入 token system，\(\mathcal{T} = (\mathsf{Token}, \bowtie)\)，包含一组 tokens 以及建立在上面的对称关系 conflict relation \(\bowtie \subseteq \mathsf{Token} \times \mathsf{Token}\)

在加入 Token 后也需要相应的对操作的函数语义进行修改，最后获得为三元组（相应的，语义表达上笛卡尔积叉乘 Token 的幂集）如下：

\[\mathcal{F} \in \mathsf{Op} \rightarrow (\mathsf{State} \rightarrow ( \mathsf{Val} \times (\mathsf{State} \rightarrow \mathsf{State}) \times \mathcal{P}(\mathsf{Token})))\]

使得

\[\forall o, \sigma . \mathcal{F}_o(\sigma) = ( \mathcal{F}_o^{\mathsf{val}}(\sigma) , \mathcal{F}_o^{\mathsf{eff}}(\sigma) , \mathcal{F}_o^{\mathsf{tok}} )\]

在银行应用中，withdrawl，会接受一个 token \(\tau\)与自身相冲突，其他操作都不接受 token，所以操作的语义最后一项是个空集.

这里的 token，很想共享内存并发中的互斥锁。后续 Section 4 会证明用 token 的方式保证不变式的高效性。

？？这里不太明白，为什么可以弱化对 2.1 节交换性的要求。形式化表达中多了一个或？或 token 的。。这里先 Pass

Formal Semantics

问题记录

2.1 节末尾，为什么 Causal Consistency 不允许图 1a 的情形，而允许图 1b 的情形。

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

Step 3

思路复现

证明与推理复现

实验验证复现