線性一致性

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

Herlihy的論文中採用了Nancy A. Lynch和Mark R. Tuttle所發明的I/O自動機（I/O automata） 模型來定義線性一致性的概念。在 I/O automata 中程序的執行用歷史(History/schedule)來描述。所謂歷史就是指一個有限的方法調用和響應事件構成的集合。嚴格地：我們先定義執行片段(Execution fragment)為序列：

，其中

為此I/O自動機的狀態集，定義執行序列(Execution sequence)為

是初始狀態的執行片段。那麼歷史就是執行序列中的事件子序列。在我們即將研究的併發系統中，歷史中的輸出事件(Output event)和輸入事件(Input event)分別對應線程P和對象X的調用(Invoke)和響應(Response)。下面將響應事件記做

，將調用事件記做

，其中P為線程名稱，op為操作名稱，X為對象名稱，res為返回值。 ^[1] 

1、定義響應事件

與調用事件

相匹配，如果P=P'，X=X'。

2、順序歷史(Sequential history)：歷史H是順序的，滿足以下兩個條件：H中的第一個成員為調用事件；除了H中的最後一個調用事件之外，H 由相鄰的、兩兩相匹配的調用事件和響應事件組成。

3、併發歷史(Concurrent history)：不是順序歷史的歷史稱為併發歷史。

4、在線程P上的子歷史(Process subhistory)

定義為H在線程P上的射影，即H中所有線程名為P的事件構成的子集。

5、如果對於H中任意的P，H|P 是順序歷史，則稱H是良形式的(well-formed)。

6、等價的兩個歷史H與H'：

定義為

。

7、操作(Operation)e定義為相匹配的一對調用事件和響應事件。

8、完備化函數Complete(H)：Complete(H)的結果是包含在H中的、最大的、僅含有互相匹配的調用事件和響應時間的時間序列。

9、歷史集S是前綴閉(prefix-closed)的，如果

，其中

代表H中以操作e結尾的一個前綴。

10、對象X順序性説明(Sequential specification)定義為對象X的前綴閉的順序歷史集。順序性説明描述了一個對象所有可能的順序行為。

11、合法的(Legal)順序歷史指的是

（指H中對象為x的那些事件）屬於x的順序性説明。 ^[1] 

對於給定的一個歷史H，其中必然藴含着一個非自反的偏序關係

（可稱之為“之前” - precede），其定義如下：

， 若

在

之前。 ^[1] 

如果滿足以下條件，則定義歷史H是線性一致的(或可線性化的-linearizable)：

線性一致性最重要的性質就是其“局部性”（Local property，或可組合性 - Compositional），即數個線性一致單對象歷史的組合也是線性一致的。

線性一致性的非阻塞性(Non-blocking property)：線程P對完全操作(total function)的調用永遠不會阻塞。 ^[2] 

實現線性一致性的最簡單方法是在關鍵部分運行原始操作組。嚴格來説，可以小心地允許獨立的操作重疊它們的關鍵部分，只要這不違反線性一致性。這種方法必須平衡大量鎖的成本與增加的並行性的好處。

研究人員喜歡的另一種方法是（但還沒有廣泛應用於軟件行業），就是使用硬件提供的原生原子來設計可線性化的對象。這有可能最大限度地提高可用的並行性和最小化同步成本，但需要數學證明，表明對象的行為是正確的。

這兩個有希望的混合是提供事務性內存抽象。與關鍵部分一樣，用户標記必須與其他線程隔離運行的順序代碼。然後實現確保代碼以原子方式執行。這種抽象風格在與數據庫交互時很常見，例如，在使用Spring框架時，使用@Transactional註釋一個方法將確保所有的封閉的數據庫交互發生在單個數據庫事務中。事務內存確保所有的內存交互發生原子。與數據庫事務一樣，事務的組成，特別是數據庫和內存中的事務也會出現問題。

設計可線性化對象時的一個常見主題是提供一個全有或全無的接口：一個操作完全成功，或者失敗，什麼都不做。（ACID數據庫把這個原理稱為原子性。）如果操作失敗（通常是由於併發操作），用户必須重試，通常執行不同的操作。例如：