# 2-1 Linearizability

:::info
理解和區分線性一致性(Linearizability)與可串聯性(Serializability)，需注意許多操作不是原子性的（或稱為延遲存在）。也就是說，不能將操作、事務或事件視為瞬間完成的點，而應將其視為具有起點和終點的時間段。因此，線性一致性考量的是在未使用並行控制的情況下，達成與串行執行相一致的結果。
:::
:::warning
#### Linearizability:
如果並行計算在某種正式定義的意義上"等同"於一個合法的順序計算，則該計算是線性一致的。
如下圖，"W(0)A" 代表 Process $A$ 寫入了 0，R(0)B 代表了 Process $B$ 讀到了 0。
橫線代表了這個 process 執行的長度，寫入變數的時刻可能發生在執行中的某處。
所以以上執行順序可以解釋成 W(0)A -> W(1)B -> R(1)A -> W(0)C -> R(0)B。
因為寫入變數的時刻可能發生在執行中的某處，所以只要能夠找到一個順序來解釋，就代表他是 Linearizable。

#### Sequential Consistence:
1. 對於每個獨立的處理單元，執行時都維持程式的順序 (Program Order)
2. 整個程式以某種順序在所有處理器上執行

如果一個系統，可以將並行的事物按照某種調度，使其可以被解釋成某種序列執行的結果，那就是可串聯性的。
例如(a)中，P3, P4 發現讀 x 會是先 b 再 a，那就可以解釋成 $W_{P2}(x)b \to R_{P3}(x)b / R_{P4}(x)b \to W_{P1}(x)a \to R_{P3}(x)a / R_{P4}(x)b$
的執行順序。
但是在(b)中，你找不到合理的執行順序來解釋他們讀到 x 之順序的行為。

**兩者最大的差別在於 Lineraizability 把事件看成一段時間，其中關鍵的操作(如寫入變數)會發生在其中某處，你需要在保持 process 間非並行事件的順序的同時，去找出能夠解釋結果的排法。
而 Sequential Consistence 則把事件看成一個單位，只要重排 process 之際的事件能夠解釋就好。(所以有可能打亂 process 間事件的順序)**
#### serializability:
可串行性(serializable)意味對於存在共同操作對象的多個並發執行的相同事務串行執行結果（如：生成資料庫狀態、數據值）「等價」於某個「串行化調度」（即連續的受時間上沒有事務重疊影響）。

:::

## 1. INTRODUCTION
> 一個並行處理系統是由一些能夠以共享物件互相溝通的循序式行程(sequential process)所組成的。

如果並行計算在某種正式定義的意義上"等同"於一個合法的順序計算，則該計算是線性一致的。

**線性一致性是一個局部性質**：如果每個獨立的對象都是線性一致的，則整個系統是線性一致的。局部性增強了模塊化和並發性，因為對象可以獨立實現和驗證，而且運行時調度可以完全去中心化。

**線性一致性也是一個非阻塞性質**：調用完全定義的操作的行程永遠不會被迫等待。非阻塞增強了並行性，並意味著線性一致性是對於需要實時響應的系統的適當條件。線性一致性是一個簡單且直觀吸引人的正確性條件，它概括和統一了文獻中的許多隱含和明確的正確性條件。

## 2. SYSTEM MODEL AND DEFINITION OF LINEARIZABILITY
### 2.1 Histories
一個並行系統地執行可以被解釋成*歷史(history)*。
歷史為一系列*調用(invocation)* 與 *回應(response)* 的事件所組成的列表。
:::info
$\langle x\ op(args*)\ A\rangle$
$\langle x\ term(res*)\ A\rangle$
:::spoiler
一個操作的調用可以被表示成$\langle x\ op(args*)\ A\rangle$
其中：
- x 是物件名稱
- op 是操作名稱
- args* 是一系列引數值
- A 是 process 的名子

一個操作的回應可以被表示成$\langle x\ term(res*)\ A\rangle$
- x 是物件名稱
- term 是終止條件
- res* 是一系列回傳值
- A 是 process 的名子
:::

:::info
:::spoiler **Sequential History**
一個歷史 $H$ 可以被說是循序的(sequential)，如果：
1. 第一個事件是*調用*
2. 每一個調用(可能除了最後一個)都直接跟著該調用的回覆

**否則就是並行的**
:::

:::info
:::spoiler **process subhistory** & **object subhistory**
**process subhistory**
一個 history $H$ 的 process subhistory $H|P$ (念作 H at P)，是由 H 中所有 process P 有關的事件所集合而成的。
**object subhistory**
一個 history $H$ 的 object subhistory $H|x$ ，是由 H 中所有物件 x 有關的事件所集合而成的。
:::

:::info
一個*操作(operation)* $e$ ，是由歷史中一對屬於 $e$ 的調用 $inv(e)$ 跟回應 $res(e)$ 所組成的。
我們透過 $[q\ inv/res\ A]$ 的方法來描述一個*操作*，其中 $q$ 是物件、 $A$ 是 process。
:::

**圖1：**
例如上圖中是以下 FIFO queue $q$ 的歷史：

:::info
$complete(H)$ 是指把 $H$ 中所有處於未決狀態(pending)的調用移除後的 subhistory
有點像是在清理這個歷史，變成一個所有調用都有回覆的子歷史。
:::

### 2.2 Definition of Linearizability
:::info
一個歷史 $H$ 催生出了一個非自反的偏序關係 $\lt_H$，用來描述操作：
$e_0 \lt_H e_1\ if \ res(e_0)\ precedes\ inv(e_1)\ in\ H$
:::
如果操作不能套用 $\lt_H$ ，那就是並行的。
如果 $H$ 是循序的，那 $\lt_H$ 就升級為全序的。
:::success
一個歷史 $H$ 是 *linearizable* ，如果他可以被延伸(新增0或多個回覆事件)成 $H'$ 使得：
**L1:** $complete(H')$ 等價於某些循序歷史 $S$
**L2:** $\lt_H\ \subseteq\ \lt_S$
:::
非正式地說，把 $H$ 延伸成 $H'$ 隱喻了某些未決狀態(pending)的關鍵操作已經發會效用了，即使那些操作的回覆還在路上。

我們把 $S$ 稱作 $H$ 的 linearization；不確定性伴隨著 linearizability 而來：
1. 對每個 $H$ ，有可能有多個延伸 $H'$ 同時滿足 **L1, L2**。
2. 對每個 $H'$ ，可能有多個 linearization $S$

### 2.3 Queue Examples Revisited
:::info
設 "$\cdot$" 為把事件連接的運算子。
:::
上面圖1中的 $H_1$ 是 linearizable，因為 $H_1 \cdot \langle q\ Ok()\ A \rangle$ 等價於以下循序歷史

## 3. PROPERTIES OF LINEARIZABILITY

### 3.1 Locality
性質 $P$ 可以被說是 *局部(local)* ，如果一個系統符合 $P$ ，且其內的各個物件個體也滿足 $P$。**Linearizability** 滿足*局部*特性

:::success
**THEOREM 1** $H$ 是 $linearizable$ 若且維若 $\forall object\ x, H|x$ 是 $linearizable$
:::

### 3.2 Blocking versus Nonblocking
Linearizability 是一個*非阻塞(nonblocking)* 的性質：一個未決狀態(pending)的調用不需要等其他 pending 的調用完成。
:::success
**THEOREM 2.** 如果 $\langle x\ inv\ P\rangle$ 是一個 linearizable 歷史 H 中的一個未決狀態之調用，則存在一個 $\langle x\ res\ P\rangle$ 使得 $H \cdot \langle x\ res\ P\rangle$ 為 linearizable。
:::

### 3.3 Comparison to Other Correctness Conditions
- sequential consistency
此關係弱於 linearizability，因為不要求保留原本在歷史中的順序。(但是要求保持 process 中的順序)
例如下面 $H_7$ 是 sequential consistent 但不是 linearizable。

    (History H_7)
    q Enq(x) A
    q Ok() A
    q Enq(y) B
    q Ok() B
    q Deq() B
    q Ok(y) B 

因為對 sequential 來說，不同 process 間的事件可以重排順序，所以會變成

    (History H_7)
    q Enq(y) B
    q Ok() B
    q Enq(x) A
    q Ok() A
    q Deq() B
    q Ok(y) B 

但是 linearization 要求非並行事件要保留順序，所以 $H_7$ 不能 linearize。

而且 sequential consistence 不滿足 *局部(local)* 特性
例如以下 $H_8$ 中，$H_8|p$ 與 $H_8|q$ 都滿足 sequential consistent，但 $H_8$ 本身不滿足。

    (History H_8)
    p Enq(x) A
    p Ok() A
    q Enq(y) B
    q Ok() B
    q Enq(x) A
    q Ok() A
    p Enq(y) B
    p Ok() B
    p Deq() A
    p Ok(y) A
    q Deq() B
    q Ok(x) B

因為你無法在重排 $H_8|p$ 與 $H_8|q$ 的同時保持 process A, B 的事件順序

    (History H_8)
    ┌-->p Enq(x) A
    |   p Ok() A
    |       q Enq(y) B  <--┐
    |       q Ok() B       |
    |       q Enq(x) A     |
    |       q Ok() A       |
    └-->p Enq(y) B      <--┘
        p Ok() B
        p Deq() A
        p Ok(y) A
            q Deq() B
            q Ok(x) B

如上重排 $H_8|p$ 的時候， process B 內部的事件順序卻變了。
- serializability
可串行性(serializable)意味對於存在共同操作對象的多個並發執行的相同事務串行執行結果（如：生成資料庫狀態、數據值）「等價」於某個「串行化調度」（即連續的受時間上沒有事務重疊影響）。

## 4. VERIFYING THAT IMPLEMENTATIONS ARE LINEARIZABLE
### 4.1 Definition of Correctness
:::info
*implementation* 是由以下兩個物件交織組成的歷史集合
- representation(REP): 指的是資料結構或系統的具體實現介面
- abstraction(ABS): 代表系統應當遵守的標準或者介面

其中：
1. 子歷史 $H|REP$ 和 $H|ABS$ 都必須是良好組成條件(well-formedness condition)的，意即所有操作都要有頭有尾(有*調用invocation*有*回復response*)。
2. 對每個 process P, 每個 $H|P$ 中的 REP 都要被包含在 $H|P$ 中的一個 ABS
:::
==如果一個遵循某 ABS 規範的 implementation 中的所有歷史 $H$ ，它的 $H|ABS$ 為 linearizable，那該 implementation 就是正確的。==

### 4.2 Representation Invariant and Abstraction Function
- **Representation Invariant**: 資料應滿足的布林條件，用來確保資料在使用過程中有沒有遭到汙染，可以用來界定資料狀態是否合法。
- **Abstraction Function**: 這個函數用於說明一個合法的表示狀態在抽象層次上的意義。該函數能夠將內部狀態（即數據在記憶體中的具體存儲方式）轉化為應當展現的抽象行為。

文中用了一個 queue 為例：
其中給定

rep = record {back: int, items: array [item]}

* **Enq** 將 back +1，代表配置新的空間，再將新元素放進新的空間
* **Deq** 從 1 到 back - 1，逐一走訪搜尋第一個非 NULL 元素。

但是因為 Enq 非 atomic，所以可能會發生一些情況：

Enq(x) A 
Enq(y) B 
  INC(q.back) A
  OK(l) A 
  INC(q.back) B 
  OK(2) B 
  STORE(q.items[2], y) B
  OK() B
OK() B

令 $r$ 為上述歷史之後的 rep 值，因為 B 的 Enq 操作已經得到回覆，abstraction funciton A\(r) 應該要反應出 B 的 Enq，但是 A\(r) 可能會也可能不會反應 A 的 Enq 操作，所以 A\(r) 可能是 [y], [y,x], [x,y]。

現在有個矛盾的地方，如果現在有另一個 process C 執行了 Deq：
假設 A\(r) 是 [x,y]，那因為 Deq 會回傳 y，跟 A\(r) 是 [x,y] 的假設衝突。
假設 A\(r) 是 [y] 或 [y,x]，但如這時 process A 完成了插入值進陣列的動作，那 process C 會拿到 x ，跟 A\(r) 是 [y] 或 [y,x] 衝突。

會發生這種情況主要是因為 race condition，如果 process A 在 process C 之前插入，那順序看起來就會像 A->B->C，反之會像是 B->A->C，但是這種順序的不確定性沒有太大的關係，因為歷史都是 linearizable。

為此我們重新定義 abstraction function 成 abstract values 的集合。
$A: REP \to 2^{ABS}$
這代表了所有可能性的集合。

### 4.3 Verification Method
給定一個歷史 H ，其可能有多個 linearized 的結果。
:::info
我們定義 $Lin(H)$ 為所有 H 的 linearized 結果的集合。
也就是對外部觀察者來說，它在所有平行時空的結果的集合。
:::
如下：

我們的驗證方法集中在展示下面特性

$For\ all\ r\ in\ Lin(H|REP),I(r)\ holds\ and\ A(r) \subseteq\ Lin(H|ABS)$

也就是對於所有 $H|REP$ 的 linearized 結果，都要被 $H|ABS$ linearized 結果給包含住。
也就是給定下圖， $A(Lin(H|REP))$ 的每一項都要 $\subseteq Lin(H|ABS)$ 的對應項。

## 5. REASONING ABOUT LINEARIZABLE OBJECTS
### 5.1 Concurrent Registers
以下給出了對於物件 r 的讀寫操作公理：
:::info
**THEOREM 3.**
如果 $r$ 是一個 $H$ 中的 $Read()/Ok(v)$ 操作，那麼存在一個 $w = Write(v)/Ok()$，使得 $r$ 非 $w$ 的前繼(precede)，且在 $w$ 跟 $r$ 之間不存在其他寫入操作 $w'$
:::
:::info
**THEOREM 4.**
如果一個區間沒有跟寫入操作重疊，那麼該區間中的所有讀取操作都會回傳相同的值
:::

### 5.2 Concurrent Queues
:::info
**LEMMA 5.**
在任意循序歷史 H 中，如果 x enqueue 得比 y 早，那 x 就不會在 y 之前被 dequeue
:::
:::info
**THEOREM 6.**
如果 Enq x, Enq y, Deq x, Deq y 都是 H 中的完整操作(有的操作)，且 Enq x 先於 Enq y，那麼 Deq y 就不會先於 Deq x
:::
:::info
**THEOREM 7.**
如果 Enq x 先於 Enq y，且 y 已經被 dequeued，那麼要麼 x 也已被 dequeued、要麼現在還有一個未決狀態(pending)的 Deq 與 Deq y 並行
:::
:::info
**THEOREM 8.**
如果 x 被 dequeued ，那他曾被 enqueued 然後 Deq 操作不先於 Enq
:::

## 6. DISCUSSION

這部分討論了 sequential 與 concurrent 在規範和驗證方面的公理方法發展史，指出以往的研究主要聚焦於控制結構。而本文的研究則專注於針對併發對象的數據進行規範和驗證，通過利用數據類型的語義來提高並行度，從而更適合於並行程式的需求。
此外，還解釋了 linearizability 在規範、實現以及驗證多處理器系統中並行對象方面的重要性。linearizability 通過創造一種假象，使得每個操作似乎在調用(invocation)和回復(response)之間的某一瞬間立即生效，這樣就能將並行計算的複雜問題轉化為更簡單的序列計算問題，而不直接處理並行計算的複雜性。