问题与系统定义

（选择这篇的理由是，它描述了一个“从底层硬件的公设出发推导出读写序列的Serializability”的过程。在分布式系统中，同样也是通过一些底层的访问控制、执行的约束来保证最终结果的一致性。同时，这篇文章的问题构造与证明中，出现了大量的“序”关系。这也是理解分布式系统执行的关键。）

这份工作的动机是硬件设计中，如何解决对寄存器的异步并发访问的问题。只有基于寄存器行为的一些假设，才能证明其所允许的并发访问的正确性。然而直接从寄存器的物理电气特性去分析行为非常复杂。因此这份工作提出了一个研究寄存器的公理基础，即如果一个寄存器满足特定的公理，就可以称之为一个“serial device”（对其的操作是一个动作组成的序列）。因此有关寄存器的正确性的问题就被大大简化了。这份工作同样证明了他们提出的公理是满足这一要求所需的最弱的条件。在与硬件设计者讨论后，他们认为满足这些要求的设备是物理上可实现的。

在并发系统的研究当中，常常会假设内存的引用是非并发的。两个同时发生的操作会以任意的一个顺序执行，造成结果的不确定性。对寄存器的非并发访问可以通过锁来实现，使得一个写操作不能与任何其他操作并发。在底层硬件中，flip-flop 是一种可以存储一个 bit 的单元。而想要锁定这个寄存器则必须再实现一个基于 flip-flop 的 lock bit，开销过大并且降低了系统的并发度。于是这份工作考虑去设计一种寄存器，使得并发访问对外显得非并发，而非并发访问会保留它们的顺序。

定义 valid schedules：

A sequence of operations whose effect is equivalent to some sequential (nonconcurrent) executions of these operations

其影响与结果相当于这些操作的某个顺序执行

Section 3 Axioms for register

Section 4 Axioms define only valid schedules (and are the weakest)

​ (给定调度有效性的简单的充要条件)

Axioms <=> Validity Conditions <=> Valid

基本概念

操作：读或写。每个操作对应一个值。约定所有写操作的值都是可区分的，这样我们可以知道哪个值是由哪次写操作产生的，并且可以将读取到一个值的读操作与产生它的写操作对应起来。

每个操作都分为 start 和 end 事件。用 |op:x 和 op:x| 来标注。

调度：

一个 start 和 end 的序列，对于每一个 |op 都存在唯一的 op| 与之对应，反之亦然。

precedes 关系：

事件在另一事件前发生。|op1:x precesed |op2:y 指 op1 比 op2 先开始。

op1 precedes op2 指 op1| precedes |op2。即操作整体在先

concurrent：

neither op1 precedes op2 nor op2 precedes op1

nonconcurrent: otherwise

valid schedule:

对于一个调度S，能够通过重新安排操作，使得所有的操作都是非并发的，所有的S中的非并发操作保留它们原有的 precedes 序关系，且读操作的返回值与写操作一致。

形式地说，S 是一个有效调度，当且仅当存在 S 的排列 S’ 使得下列 validity conditions 成立：

VC1. 对于所有 S‘ 中的操作， |op precedes op| （合法）

VC2. 任一对 S’ 中的操作非并发

VC3. 如果 op1 precedes op2 in S, then op1 precedes op2 in S’

VC4. 在 S’ 中，每个读操作存在一个在前的写操作。并且如果 w:x 是 r:y 的最近的一次写操作，则 y = x

寄存器操作的公理

在没有歧义的时候，用 |op 和 op| 来表示 op 开始和结束的时间点。

当我们说 时间点 t within op 时，意味着 |op \leqslant t \leqslant op|

Axioms

A1. 对于每个 r:x 存在某个时间点 within r，寄存器的值是 x

A2. 如果时间点 t 时寄存器的值为 x，并且一个写操作 w:y 在 t 后开始，在 t’ 前结束（t < t’），那么 t’ 时寄存器的值一定不是 x （它可能是未定义的）

A3. 如果时间点 t’ 时寄存器的值为 x，那么存在某个时间点 t （t\leqslant t’），使得 t within w:x 且 在
t 时，寄存器的值为 x

A4. 如果时间点 t 和 t‘ 时寄存器的值为 x，那么 x 的值在 t 和 t’ 之间一直都是 x

可以看出这四条公理都是非常直观的：

A1 相当于在说读取操作一定是有寄存器当中的依据的

A2 表示一个写操作一定会对寄存器的值产生影响

A3 在说寄存器中的值一定由某个写操作产生

A4 是说一个值不可能在不连续的两段时间里出现。也就是说，写操作只会尝试写一次

Notation. 在一个调度中使用 (x) 来表示在某个时间点，寄存器的值为 x，直到调度中有某个 (y) 出现

有效调度的性质

对于任意调度 S，对操作的值定义关系 before：

(1) x before x, 如果存在 r:x precedes w:x 或不存在 w:x

(2) x before y, y \neq x，如果对于某两个 op1, op2, op1:x precedes op2:y

(3) x before z, 如果对于某个 y，x before y 且 y before z

在这篇文章中，作者将集合上的偏序关系重新定义为：反自反，反对称，传递的关系。

反自反是为了保证对于调度 S，不存在 r:x 先于 w:x 这样的顺序。

Theorem 1. 一个调度有效，当且仅当与它相关的 before 关系是一个偏序关系

\Rightarrow: 从偏序关系，构造任意全序，证明 VC1 - VC4

\Leftarrow: 对于有效调度 S，存在某个排列 S‘ 满足 VC1-4，其中关于某个值 x 的操作一定是连续的。它规定了值之间的“全序”关系 before。这个全序必须和 S 上的偏序一致，故 S 上的 before 一定是偏序关系，否则不存在与之一致的全序。

对于任意在满足 A1-A4 的寄存器的调度 S 上的 x 定义：

Rx = {t | 时间点 t 寄存器的值为 x}，这里将其成为 x 的时域

Observetion1 Rx 是一段连续的时间。如果 t1, t2 \in Rx, 那么 \forall t, t1 < t < t2, t \in Rx (A4)

Observation2 如果 Rx 非空，那么对于每一个 op:x 中都有某个时间点 within op，寄存器的值为 x (A1, A3)

Theorem 2. 任何满足 A1, A2, A3 和 A4 的调度都是有效的

为了证明调度有效，我们要从四条公理证明调度上的 before 关系是偏序的。

从 A1，A3 可以得到 irreflexive；

由 Observation1、2 可知 antisymmetric；

由 before 的定义可知 transitive。

Theorem 3. 对于一个有效调度，总能在某些特定的时间点对寄存器赋值，从而使得 A1, A2, A3, A4 被满足。

这里用的是先构造，再证明的方法。其构造方式大致如下：

找到 S 的满足 VC 的排列 S’, 将操作从 1-n 编号为 op_i，其对应值为 v_i （可能重复）。然后按如下规则进行赋值：

(1) (v1) 在 |op1 后立刻赋值

(2) (vi), i > 1，在 |op_i 或 (v_{(i - 1)}) 后立即赋值（取较晚的那个）

至此，四条公理已被证明是调度有效的充要条件。

最后，文章又通过构造满足四条公理之三而不满足另外一条，导致调度无效的反例来证明四条公理并无相互蕴含的关系，保证了结果是最简的。