跳至內容

線性一致性

維基百科,自由的百科全書

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

歷史

[編輯]

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

嚴格的定義

[編輯]

Herlihy 的論文中採用了 Nancy A. LynchMark 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為返回值。

基本概念

[編輯]
  • 定義響應事件與調用事件相匹配(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是良形式的(well-formed)。
  • 等價的兩個歷史H與H': 定義為
  • 操作(Operation) e 定義為相匹配的一對調用事件和響應事件。
  • 完備化函數Complete(H):Complete(H)的結果是包含在H中的、最大的、僅含有互相匹配的調用事件和響應事件的時間序列。
  • 歷史集S是前綴閉(prefix-closed)的,如果,其中代表H中以操作e結尾的一個前綴。
  • 對象X順序性說明(Sequential specification)定義為對象X的前綴閉的順序歷史集。順序性說明描述了一個對象所有可能的順序行為。
  • 合法的(Legal)順序歷史指的是(指H中對象為x的那些事件)屬於x的順序性說明。

線性一致性的形式化定義

[編輯]
  • 對於給定的一個歷史H,其中必然蘊含着一個非自反的偏序關係(可稱之為「之前」 - precede),其定義如下:, 若 之前。
  • 如果滿足以下條件,則定義歷史 H是線性一致的(或可線性化的-linearizable):
  1. 首先我們將H 擴展
  2. 等價於一個合法的順序歷史S;

例子

[編輯]

線性一致性的性質

[編輯]
  • 線性一致性最重要的性質就是其「局部性」(Local property, 或可組合性 - Compositional),即數個線性一致單對象歷史的組合也是線性一致的。
  • 線性一致性的非阻塞性(Non-blocking property):線程P對完全操作(total function)的調用永遠不會阻塞。

嚴格一致性

[編輯]

相關的話題

[編輯]

參考資料

[編輯]
  1. Linearizability: A Correctness Condition for Concurrent Objects, MAURICE P. HERLIHY and JEANNETTE M. WING Carnegie Mellon University