歷史
線性一致性是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)為序列: ,其中 為此I/O自動機的狀態集,定義執行序列(Execution sequence)為 是初始狀態的執行片段。那么歷史就是執行序列中的事件子序列。在我們即將研究的並發系統中,歷史中的輸出事件(Output event)和輸入事件(Input event)分別對應執行緒P和對象X的調用(Invoke)和回響(Response)。下面將回響事件記做 ,將調用事件記做 ,其中P為執行緒名稱,op為操作名稱,X為對象名稱,res為返回值。
基本概念
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的順序性說明。
線性一致性的形式化定義
對於給定的一個歷史H,其中必然蘊含著一個非自反的偏序關係 (可稱之為“之前” - precede),其定義如下: , 若 在 之前。
如果滿足以下條件,則定義歷史H 是線性一致的(或可線性化的-linearizable):
1.首先我們將H擴展為H';
2.Complete(H')等價於一個合法的順序歷史S;
線性一致性的性質
線性一致性最重要的性質就是其“局部性”(Local property,或可組合性 - Compositional),即數個線性一致單對象歷史的組合也是線性一致的。
線性一致性的非阻塞性(Non-blocking property):執行緒P對完全操作(total function)的調用永遠不會阻塞。
線性一致性操作
實現線性一致性的最簡單方法是在關鍵部分運行原始操作組。嚴格來說,可以小心地允許獨立的操作重疊它們的關鍵部分,只要這不違反線性一致性。這種方法必須平衡大量鎖的成本與增加的並行性的好處。
研究人員喜歡的另一種方法是(但還沒有廣泛套用於軟體行業),就是使用硬體提供的原生原子來設計可線性化的對象。這有可能最大限度地提高可用的並行性和最小化同步成本,但需要數學證明,表明對象的行為是正確的。
這兩個有希望的混合是提供事務性記憶體抽象。與關鍵部分一樣,用戶標記必須與其他執行緒隔離運行的順序代碼。然後實現確保代碼以原子方式執行。這種抽象風格在與資料庫互動時很常見,例如,在使用Spring框架時,使用@Transactional注釋一個方法將確保所有的封閉的資料庫互動發生在單個資料庫事務中。事務記憶體確保所有的記憶體互動發生原子。與資料庫事務一樣,事務的組成,特別是資料庫和記憶體中的事務也會出現問題。
設計可線性化對象時的一個常見主題是提供一個全有或全無的接口:一個操作完全成功,或者失敗,什麼都不做。(ACID資料庫把這個原理稱為原子性。)如果操作失敗(通常是由於並發操作),用戶必須重試,通常執行不同的操作。例如:
1.僅當後者的內容與提供的舊值匹配時,比較和交換才會將新值寫入位置。這通常用於讀取 - 修改 - CAS序列:用戶讀取位置,計算新的值以寫入,並用CAS(比較和交換)寫入;如果該值同時改變,則CAS將失敗並且用戶再次嘗試。
2.Load-link / store-conditional更直接地編碼這個模式:用戶用load-link讀取位置,計算一個新的值來寫入,並用store-conditional寫入;如果該值同時發生變化,則SC(存儲條件)將失敗,用戶再次嘗試。
3.在資料庫事務中,如果事務由於並發操作(例如死鎖)而無法完成,事務將被中止,用戶必須再次嘗試。