# 2-1. Linearizability: A Correctness Condition for Concurrent Objects
:::warning
* **sequential consistency(序列一致性)：** 只要在同個process上所有行為都是符合順序就可以，須符合下列兩點:
* 事件在歷史上各個process來看都是一致的。
* 單一process的事件歷史在全局歷史上符合program order。
從圖B中我們可能以為P2、P3讀出來的x順序和物理時間不一致，但只要P0、P1、P2、P3全部process都認為x是先被P1寫入2再被P0寫入1, 那麼我們認為這種情況仍然是一致的。
而下圖這張因為P2和P3讀出來不一致，違反sequential consistency的第一個條件。
* **Linearizability(線性一致姓)：** 可以稱做strong consistency或是atomic consistency。為單一物件（例如分散式暫存器或資料項目）上的一組單一操作（通常是讀取和寫入）的行為提供即時保證，**寫入看起來要是瞬時的**，也就是說一旦寫入完成，所有後續讀取（其中「稍後」由掛鐘開始時間定義）都應傳回該寫入的值或稍後寫入的值。一旦讀取返回特定值，所有後續讀取都應傳回該值或後續寫入的值。
假設一個分散式計數器服務，支持增加和讀取計數器的值，如果採用線性一致性模型，當一個節點增加了計數器之後，所有其他節點上隨後的讀取操作都應該立即看到這次增加的結果，就好像這些操作是按照它們發生的時間順序一個接一個執行的。
當事件沒有重疊時，**必須給出明確的先後順序**。若event之間有重疊則是並行的，如下圖，這個過程中如果P1去讀取x, 不管讀出來是0還是1,都算符合linearizability,P2和P0之間也是這樣，但是P2和P1讀取x的結果只能是0-0、0-1，或是1-1，不能是1-0，因為P3起始晚於P0的結束，所以只能讀出x=1才才是符合Linearizability。
可以用下圖來簡單說明上面兩者的差異，因為A和C是並行的，A和C誰在前面都可以，但是C和B在Linearizabiltiy中必須C在前B在後，而Sequential Consistency中B和C的順序可以互換。
:::
## 1. INTRODUCTION
:::info
這篇論文主要是提出一個對並發系統(concurrent system)建構的一個模型，以及線性一致性的正式定義，接著討論線性一致性的局部性(local property)和非阻塞(nonblocking)屬性，提出一個驗證可線性化物件實作的方法，並實作了一個新穎的高並發隊列來闡述這個驗證方法，最後舉了幾個例子，分析了一下可線性化的並發寄存器和佇列。
:::
>**什麼是concurrent system(並行系統)?**
一個**系統能同時處理多個process或thread**，則稱之為concurrent system，過程可能會共享某些資源（如memory、I/O device等），在並行系統中，多個運算過程的執行可以在單核(多個process交錯使用cpu)或多核處理器上(真正的parallel，各自在不同的core上執行)，在一個concurrent system中一個concurrent object可能被多個process調用，每個操作間會有交叉執行的問題，我們需要定義清楚這些交叉執行的問題，如果一個concurrent計算與合法的序列計算在形式上定義的意義上是等價的，則該計算就是linearizability的。
>**關於linearizability的一些屬性**
>1. **nonblocking :** 在進行totally-defined的操作時，不用等待，增強concurrency，代表linearizability在real time系統中是合適的條件。
>2. **local :** 如果每個獨立對象是可線性化的，那整個系統就是可線性化的，加強了模組性和併行性，執行的排程可以完全去中心化，
直覺上來看，concurrent object的正確性應該包含下列兩個條件：
1. 每個操作都要是瞬間生效
2. 不存在concurrent 關係的操作，要保留執行的先後順序
這允許我們用"可接受的sequential行為"來描述"可接受的concurrent行為"，能簡化一些concurrent program的推理。
## 2. SYSTEM MODEL AND DEFINITION OF LINEARIZABILITY
一個concurrent system可以用history來表示。
>**那什麼是history?**
>由invocation(呼叫)和response(回應)構成的有限序列，一個有序的歷史H滿足下列條件：
>1. H的第一個事件是一個invocation
>2. 除了最後一個，每個呼叫後面都緊接著一個配對的回應，每個回應也都緊接著一個呼叫。
:::info
定義一個操作的 **invocation(呼叫)** 被定義為 $<x\ op(args^*)\ A>$
* $x$ : 物件名稱
* $op$ : 操作名稱
* $args^*$ : 參數值
* $A$ : process名稱
* 例子： $q$ $Enq(x)$ $A$，表示process A將x 加到queue q的尾部，$q$ $Ok()$ $A$表示操作結束。
定義一個操作的 **response(回應)** 被定義為 $<x\ terms(res^*)\ A>$
* $x$ : 物件名稱
* $terms$ : 結束條件
* $res^*$ : 回傳結果
* $A$ : process名稱
* 例子： $q\ Deq()\ A$，表示process A從queue q拿出一個值，$q\ Ok(x)\ A$則是代表process A成功將$x$從queue q中拿出，並結束操作。
:::
### Definition of Linearizability
歷史$H$引出了在操作上的一個非自反的偏序關係$<_H$，如果在H中$res(e_0)$發生在$inv(e_1)$之前，則會表示程$e_0<_He_1$，而不符合$<_H$的操作就被認為是concurrent。
如果$H$能夠透過加0到1個事件成为$H’$, 而且$H’$中事件的開始/结束是成對的($H’$是$H$的完整歷史), 那$H’$可以線性化为全序關係S，使得:
1. S中所有的事件開始/结束是”緊連著”的，事件具有原子性不可拆開
2. 一个事件$e_0$的结束早於$e_1$的開始, 那這個全序關係在S中仍然存在。
那麼在不違反queue的正確行為(例如FIFO)的前提下，$S$就是$H$的一個linearization。
舉例：下圖中最左邊是物理時間上發生的$H$，中間是補齊成對後的$H'$，右邊是$H'$的一個linearization。
除此之外，linearization不排除像是下面這樣的例子，有個操作(Enq)在回應前就生效了，$H_3$可以擴展到$H_3'=H_3$ $\cdot$ $<q\ Ok()\ A>$，就可以等同於進入queue在出來queue之前的順序歷史了。
```=
q Enq(x) A (History H3)
q Deq() B
q Ok(x) B
```
## 3. PROPERTIES OF LINEARIZABILITY
### 3.1 Locality
>**怎樣可以稱做是一個局部屬性(Locality)?**
如果一個concurrent系統中的每個物件都滿足屬性P，則該concurrent系統也滿足屬性P，那這個屬性P就是一個局部屬性。
* **THEOREM 1.** $H$ is linearizable if and only if, for each object $x$, $H|x$ is linearizable.
* **PROOF：** 如果對於每一個物件$x$來說，$H|x$是可線性化的，那麼$H$就是可線性化的。
這邊透過反證法來證明，如果存在一個違反線性化性質的操作序列（即一個循環），那麼可以通過分析該序列來找到一個更短的循環，直到這個過程顯示出矛盾，而證明了假設的線性化循環是不可能存在的，每個對象的操作可以被獨立地、局部地線性化，而無需考慮其他對象的操作。
>
<!-- **TODO：** 救命!!!證明到底在寫什麼 :frowning: -->
### 3.2 Blocking versus Nonblocking
>**什麼是Nonblocking?**
>A pending invocation of a totally- defined operation is never required to wait for another pending invocation to complete.
>**totally- defined operation :** 對於物件所有可能的取值都有明確的定義。
* **THEOREM 2.** 如果在一個線性化的歷史H中有一個待定的呼叫$<x\ inv\ P>$(也就是操作尚未完成)，那麼總是存在一個回應$<x\ res\ P>$，使得$H$ $\cdot$ $<x\ res\ P>$可線性化的。
<!-- *這邊令inv是一個完全操作* -->
* **PROOF :**
1. 如果S中已經包含了操作(x inv P)的回應，那麼我們已經完成了證明，因為S也是在H後面加上(x res P)的線性化。
2. 如果S中不包含了操作(x inv P)的回應，根據線性化的定義，S也不會包含任何未完成的調用，由於操作是完全的（total），這表明必然存在一個回應(x res P)。
### 3.3 Comparison to Other Correctness Conditions
* **sequential consistency(順序一致性):** 要求一個歷史等同於一個合法的順序歷史，要求較線性一致性低，因為它並沒有要求保留原始歷史中的優先順序($<_H$的部分)。
每個process的順序分開看有沒有符合合法順序，下面是一個例子，$H_7$是順序一致的，因為可以將前兩行A process和中間兩行B process的操作互換，讓他看起來符合合法順序(先enq y再enq x，所以會先deq出y)。
但不是可線性化的，因為可線性化不能隨意更改順序。
```=
q Enq(x) A (History H7)
q Ok() A
q Enq(y) B
q Ok() B
q Deq() B
q Ok(y) B
```
除此之外，**順序一致性並不具備局部性**，例子如下，$H_8|p$和$H_8|q$都是順序一致的，但$H_8$不是，因為**當合併來自兩個處理器的操作時，可能找不到一個單一序列來滿足所有處理器程序順序的要求**，為了達到順序一致性，合併後的操作序列必須反映出一系列可能的串行執行操作，這些操作既需要符合p的程式順序，也符合q的程式順序，從$H_8$中可以看出，p和q的交錯操作沒有反映出任何可能的串行執行。
```=
p Enq(X) A (History H8)
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
```
* **Serializability(可串行性) :** 是一個global屬性，被作為是併發計算的基本正確性條件，一個所有事務(transcation)都是順序執行的歷史（transcation執行沒有交叉），我們可以稱該歷史為serializable，也可以明確的給未重疊的事務之間指定執行的先後順序(這裡說的順序類似線性一致性中定義的$<_H$)
>註解 : transaction(事務)是用來控制thread的，由一些物件的操作構成的有限序列，這些物件也被其他事務共享。
下面建了一個表格供參考
或許可串行性和線性一致性最大的實際差異是兩個概念適合的領域不同，可串行性適合資料庫這類系統，對於那些包含了許多物件的複雜應用，開發者要能夠較容易的保證應用的一些不變性。像是two-phase locking,，使得開發者可以用串行的思路去推理事務的執行（但同時也造成有死結和效能的問題）。反觀線性一致性，適合併發性要求較高的系統。因為在這類系統中開發者更願意使用一些專用的同步協議，及思考並發的影響。
## 4. VERIFYING THAT IMPLEMENTATIONS ARE LINEARIZABLE
### 4.1 Definition of Correctness
>implementation是由兩個object的事件按一種受約束的方式交錯在一起的歷史記錄集合。
>* **REP(representation object):** 資料結構或系統的實作介面
>* **ABS(abstract object):** 代表了系統應該遵循的規範或者介面。
>**確保系統正確性的條件:**
>1. 對於每一個歷史記錄$H$，它包含了 REP 和 ABS 的子歷史記錄。這些子歷史記錄必須符合「良好形成條件」（well-formedness conditions），代表所有操作都要有一個明確的開始和結束，並且遵守某種合理的規則或序列。
>2. 對於每一個Process P，$H$中屬於 P 的所有 REP 操作都必須包含在$H$中 P 的一個 ABS 操作中，也就是說每個抽象操作可以被看作是它內部發生的一系列 REP 操作的集合，可以把一個抽象操作想像成一個外殼，這個外殼內的是實際發生的一系列 REP 操作。
如果一個實作對於 ABS 的規範是正確的，這意味著每一個 H 的 ABS 子歷史記錄都是可線性化的。
:::info
一個正確的實作將保證**無論系統內部如何處理這些 REP 操作（可能是並行的），對於外部世界來說，你的每一次操作（例如：存錢或取錢）都像是在一個個別、獨立的時間點完整發生的**，並且保持操作的順序。即使操作（可想像成存錢）實際上涉及了多個小步驟（如檢查帳戶狀態、更新餘額等），其他人觀察到的仍然是你的帳戶金額在一個操作結束後才更新，這樣就符合可線性化的概念。
:::
### 4.2 Representation Invariant and Abstraction Function
* **representation invariant :** 一個函數或條件，用來確定哪些表示狀態是合法的，只有滿足這個不變性質的表示狀態才被認為是有效的，可以被用來代表queue的當前狀態。
* **abstraction function :** 一個函數，用來解釋一個合法表示狀態實際上在抽象階層代表了什麼。也就是說這個函數可以把queue的內部狀態（也就是具體如何在記憶體中儲存）映射到queue應該有的抽象行為
為了更好理解，這邊用一個高度並行的線性化FIFO queue 實現，有一個 rep 結構，用來表示這個queue的內部，包含兩個部分：
**1. $back$ :** 一個整數，指向queue中下一個空閒位置的索引，初始化成$null$。
**2. $items$ :** 一個數組，用於儲存隊列中的元素，初始化為$1$。
>**Enq步驟**
當加入一個新元素$x$時，$back$的值增加1，為新元素$x$分配了一個位置，再將新元素$x$存到我們剛剛分配的位置$i$。
>**Deq步驟**
>讀取當前$back$的值（即queue中的下一個空位索引）並減1，得到queue中最後一個已經被使用的位置，遍歷全部range找可以dequeue的元素，將 $items[i]$ 的值與 $null$ 交換，如果該位置之前不是 $null$（代表有元素），那麼這個元素就會被賦值給$x$，如果$x$不是 $null$，代表找到了一個元素可以dequeue，返回它並結束過程。
**接著討論在並行對象實作中，representation invariant和abstraction function的難點**，特別是對於如queue這樣的資料結構，下面的例子說明了 Process A、B是如何在彼此之間幾乎同時執行enqueue操作的，queue需要在多個操作並行進行的情況下都能反映一個有效的狀態。
Process B完全完成了它的 enqueue 操作（將$y$存進位置2），而Process A的 enqueue 操作還沒有完成（$x$還沒有存進位置1），根據這個時刻隊列的狀態，抽象函數必須能夠處理一個元素已經 enqueue，另一個元素的 enqueue 操作已經開始但尚未完成的情況，因此**抽象函數必須能夠連續定義**，以便為並行操作中的暫時性表示值賦予意義。
```=
End(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
```
若在前面的結果後加上Process C進行dequeue操作，無論抽象函數$A(r)$在任何特定時刻的值是什麼，未來的計算都將與他矛盾。
**矛盾1.** 假設抽象函數$A(r$)在某時刻的值是$[x, y]$，然後Process C執行出dequeue操作並返回了$y$，這與假設$A(r)$是$[x, y]$相矛盾，因為$x$應該是第一個被返回的。
**矛盾2.** 如果假設$A(r)$是$[y]$或$[y, x]$，並讓A完成它的enqueue操作，這時隊列中必須包含$x$（因為它的enqueue操作已經完成了），且$x$應該跟隨在$y$之後，因為假設A的enqueue操作發生在B之後。但是，如果C再次執行dequeue操作並返回$x$，這又與假設$A(r)$是$[y, x]$相矛盾。
會發生上述矛盾的原因是因為**Race Condition**，如果Process A在Process C讀取位置1之前將一個元素$x$存到位置1，那麼A的enqueue操作看起來就像是發生在B的enqueue操作之前，如果C在A存之前讀取了位置1，則看起來B的操作會先於A的操作。不過這種順序的不確定性是可以接受的，因為無論哪種順序，結果的歷史記錄都是可以線性化的，也就是我們可以將它們重排成一個合理的序列。因此抽象函數必須能夠連續定義，以便為並行操作中的暫時性表示值賦予意義
:::info
線性化就是指把並發執行的操作按一定的順序排列，使它們看起來好像是按照某個順序一個接一個執行的，即使它們實際上是同時發生的。
:::
為了解決這個問題，重新定義抽象函數，將一個表示值映射到一組抽象值的集合。$$A:REP \rightarrow 2^{ABS}$$
這個集合代表了當前表示值允許的可能線性化集合，這是在並發環境中保持隊列一致性的一種策略，確保我們即使在多個操作可能同時發生的情況下也可以理解和預測數據的流動。
### 4.3 Verification Method
線性化的概念允許我們將對並發歷史的斷言轉換為對一組序列歷史的斷言，進而轉換為對值的集合的斷言，由於一個給定的歷史記錄可能有多於一個線性化，因此在一個歷史記錄結束時，一個對象可能有多個線性化值。
我們**用$Lin(H)$表示$H$的所有線性化值的集合**，一個歷史記錄的線性化值表示了從外部觀察者的角度看到的對象的可能值。下圖是一個queue歷史記錄和他在每個事件之後的線性化值集合。
下圖顯示了上圖中抽象操作(bstract operations)的一個序列，以及實現該序列的表徵操作(rep operations)序列，如果第二列中的每個集合都是第三列中對應集合的子集，則符合正確性標準。
* **critical sections**
到目前為止，我們證明實現正確性的方法都是假設存在一個連續定義的抽象函數，但如果對象的實現包含critical sections，可能無法總是定義這樣一個函數，因為**在critical sections中，程式計數器和局部變量中編碼了必要的狀態信息，而不是在對象的代表（representation）本身，所以表徵不變式可能會被暫時違反，導致抽象函數未定義**。這邊透過使用輔助隱藏數據（auxiliary hidden data）來保存正在從queue中移出的值，使得我們可以重新引入一個連續定義的抽象函數。
## 5. REASONING ABOUT LINEARIZABLE OBJECTS
### 5.1 Concurrent Registers
下面是關於concurrent register object $r$ 讀與寫的公理(axioms)，定義了讀與寫操作的預期行為
>{true}
Read()/Ok(v)
{r.val = r'.val = v}
>{true}
Write(v)/Ok()
{r'.val = v}
:::info
基於上述的公理推導出了下面的定理
**Theorem 3.** 如果存在一個讀操作$r$，它沒有直接跟在某個特定的寫操作$w$之後，那麼一定存在另一個寫操作$w'$，發生在$w$之後，並且在$r$之前，這樣$r$讀到的值就是$w'$寫入的。
**Theorem 4.** 如果歷史記錄中的一段時間內沒有發生任何寫操作，那麼在這段時間內的所有讀操作都會返回相同的值。
:::
上面兩個定理驗證了即使是在並發執行的情況下，系統的行為可以被視為是有序的，也就是線性一致性，每個操作（無論是讀是寫）都可以被視為在一個特定的、獨立的時刻發生的，形成了一個連貫且一致的操作序列。
### 5.2 Concurrent Queues
下面是關於Concurrent Queues的一系列性質和定理，說明了並發對列的一些重要屬性，像是enqueue一定在dequeue之前、元素不會自動消失等，用於證明queue操作的線性化正確性。
>**LEMMA 5.** 在任何序列queue歷史中，如果元素x在元素y之前被Enqueue，則x不會在y之後被Dequeue，保證了queue的FIFO（先進先出）性質
>**THEOREM 6.** 如果在某個操作歷史中，x的Enqueue操作發生在y的Enqueue操作之前，那麼y的Dequeue操作不會發生在x的Dequeue操作之前，也就是說如果兩個元素幾乎同時Dequeue，要麼它們的Dequeue操作是並發的，要麼保持著Enqueue時的相對順序。
>**THEOREM 7.** 如果x的Enqueue操作發生在y的Enqueue操作之前，且y已經被Dequeue，那麼要麼x已經被Dequeue，要麼x的Dequeue操作正在進行中，確保了隊列中元素的Dequeue操作符合FIFO原則。
>**THEOREM 8.** 如果x已經被Dequeue，那一定先前有被Enqueue，且Dequeue操作不會發生在Enqueue操作之前，這個定理強調了Dequeue操作必須對應於一個有效的先前Enqueue操作。
## 6. DISCUSSION
這邊探討了關於序列（sequential）與並行（concurrent）程序的規範和驗證的公理化方法的發展歷程，強調過去這些工作都集中在控制結構上，而本篇的工作著重於規範和驗證併發對象的數據，利用數據類型的語義來增加concurrent degree，因此更適用於併發程式。
除此之外，講解了線性化對於規範、實現和驗證多處理器系統中的並行對象非常有利，因為**線性化創造了一種幻覺，讓每個操作看似在調用和回應之間的某個瞬間立刻生效**，將並發領域的問題轉化為序列領域中的簡單問題，而不是直接針對並發計算複雜的計算。
Sign in with Wallet
Connect another wallet