線性一致性

線性一致性（Linearizability），或稱原子一致性或嚴格一致性指的是程序在執行的歷史中在存在可線性化點P的執行模型，這意味着一個操作將在程序的調用和返回之間的某個點P起作用。這裏「起作用」的意思是被系統中並發運行的所有其他線程所感知。

歷史

線性一致性是Maurice P. Herlihy 與 Jeannette M. Wing共同提出的關於並行對象行為正確性的一個條件模型。在此之前，Lamport已經提出了順序一致性的概念。

嚴格的定義

I/O自動機

Herlihy 的論文中採用了 Nancy A. Lynch 和 Mark R. Tuttle 所發明的 I/O自動機（I/O automata）模型來定義線性一致性的概念。在 I/O automata 中程序的執行用歷史(History/schedule)來描述。所謂歷史就是指一個有限的方法調用和響應事件構成的集合。嚴格地：我們先定義執行片段(Execution fragment)為序列： ${s_{0},e_{1},s_{1},....e_{n},s_{n}}$ ，其中 $s_{i}$ 為此I/O自動機的狀態集，定義執行序列(Execution sequence)為 $s_{0}$ 是初始狀態的執行片段。那麼歷史就是執行序列中的事件子序列。在我們即將研究的並發系統中，歷史中的輸出事件(Output event)和輸入事件(Input event)分別對應線程P對對象X的調用(Invoke)和響應(Response)。下面將響應事件記做 $R(P,res,X)$ ，將調用事件記做 $I(P,op,X)$ 其中P為線程名稱，op為操作名稱，X為對象名稱，res為返回值。

基本概念

定義響應事件 $R(P,res,X)$ 與調用事件 $I(P',op,X')$ 相匹配(match)，如果P=P',X=X'。
順序歷史(Sequential history)：歷史H是順序的，如果滿足以下兩個條件：
- H中的第一個成員為調用事件；
- 除了H中的最後一個調用事件之外，H 由相鄰的、兩兩相匹配的調用事件和響應事件組成。
並發歷史(Concurrent history)：不是順序歷史的歷史稱為並發歷史。
在線程P上的子歷史(Process subhistory) $H|P$ 定義為H在線程P上的射影，即H中所有線程名為P的事件構成的子集。
如果對於H中任意的P，H|P 是順序歷史，則稱H是良形式的(well-formed)。
等價的兩個歷史H與H'： $H\iff H'$ 定義為 $\forall P,H|P=H'|P$ 。
操作(Operation) e 定義為相匹配的一對調用事件和響應事件。
完備化函數Complete(H)：Complete(H)的結果是包含在H中的、最大的、僅含有互相匹配的調用事件和響應事件的時間序列。
歷史集S是前綴閉(prefix-closed)的，如果 $\forall H\in S,\forall e,H^{e}\in S$ ，其中 $H^{e}$ 代表H中以操作e結尾的一個前綴。
對象X順序性說明(Sequential specification)定義為對象X的前綴閉的順序歷史集。順序性說明描述了一個對象所有可能的順序行為。
合法的(Legal)順序歷史指的是 $\forall x,H|x$ （指H中對象為x的那些事件）屬於x的順序性說明。