1. 程式人生 > >併發資料結構-1.1.4 複雜度測量&1.1.5 正確性

併發資料結構-1.1.4 複雜度測量&1.1.5 正確性

原文連結譯文連結,譯者:張軍,校對:周可人

1.1.4 複雜度測量

一個被廣泛研究的方向是在理想化模型,如並行隨機存取機上分析併發資料結構和演算法的漸進複雜度[35, 122, 135]。然而,很少有將這些資料結構放在一個真實的多處理器上進行建模的。這裡有多種原因,大部分原因跟系統硬體架構與執行緒非同步執行的相互作用有關。想想組合樹(combining tree)的例子,雖然我們能通過計算(指令數)得到O(P/logP)的加速比,但這無法反映在實證研究中[52, 129]。真實世界的行為是被上述其他因素支配的,如競爭開銷,快取行為,同步操作(例如CAS)開銷,請求到達率,退避延時,資料結構在記憶體中的佈局等等。這些因素很難用一個精確的涵蓋目前所有架構的模型來量化。

採集這些方面的複雜度(的)測量方法已經由Dwork [28] ,Anderson,Yang [7]等人提出,雖然這些方法在演算法設計上提供了有用的見解,但它們還是不能準確捕捉所有上述因素的影響。因此,併發資料結構的設計者通過在真實機器和模擬架構[9, 52, 97, 103]上執行微基準測試實證地比較他們的設計。在本章的剩餘部分,我們普遍地根據這些資料結構基於經驗觀察到的行為來評價他們,並且用簡單的複雜度變數來輔助直覺進行判斷。

1.1.5 正確性

很容易發現,簡單的基於鎖的計數器,其行為跟那些順序的實現是“相同”的。然而,很明顯我們更難看到對合並樹(combining tree)而言,同樣如此。一般情況下,併發資料結構的實現往往是很精細的,不正確的實現並不少見。因此,宣告並嚴格證明一個特定的設計正確地實現了所要求的併發資料結構是非常重要的。我們不希望達到這些而不精確地指明什麼是“正確”。

順序資料結構的資料結構規格描述通常更容易。例如,我們可以通過選擇一組狀態,並提供一個以狀態,操作名,以及該操作的引數作為函式引數,將新的狀態和操作返回值作為函式返回值的轉換函式(trainsition function)來指明一個順序資料結構的語義。加上指定的初始狀態,轉換函式(transition function)指定了該資料結構上所有可接受操作序列。計數器的順序語義定義如下:計數器的狀態是一組整數,初始狀態是0。fetch-and-inc操作的轉換函式在舊狀態上加一來獲取新狀態,返回值是計數器的舊狀態。

順序資料結構上的操作是一次一個順序執行的,我們只簡單要求順序操作的結果遵循如上討論所指定的順序語義。然而,對併發資料結構來說,操作不一定完全按照順序。併發資料結構的正確性條件一般要求有些操作完全按照順序以滿足順序語義。不同正確性條件的區別在於對總順序的需求不同。

一個常見的正確性條件是Lamport的順序一致性(sequential consistency)[81],這要求總順序上保證每個執行緒執行操作的順序。從軟體工程的角度來看順序一致性有個缺點:使用順序一致性元件實現的資料結構本身可能不是順序一致的。

一個自然,廣泛使用且克服上述問題的正確性條件是Herlihy, Wing的可線性化(linearizability)[58],它是一個用於資料庫事務的序列化條件的一個變種。可線性化需要(滿足兩個特性:(1)該資料結構是順序一致的 ,(2)使其滿足順序一致性的總體順序遵循操作執行的實時順序。遵循實時順序意味著如果操作O1在操作O2開始之前完成(操作之間不是併發的),那麼O1必須排在O2之前。該正確性條件的另外一種理解方式是,它要求我們能夠確定每個操作執行時間間隔中的不同點,稱為可線性化點,這樣,如果我們根據可線性化點的順序來對操作排序,那麼排序結果會遵循順序一致性語義。

很容易看到,基於鎖的計數器是可線性化的,計數器的狀態始終儲存在變數X中。我們將儲存增加後的值到變數X定義為fetch-and-inc操作的可線性化點。基於CAS的無鎖(lock-free)實現的計數器的可線性化點同樣簡單,除了使用CAS指令的語義而不是論證鎖語義,我們能得出結論,計數器每被修改一次就加一。

對於合併樹(combining tree)來說,很明顯我們更難看到它是可線性化的,因為計數器的狀態在同一時間不止加一,並且因為一個fetch-and-inc操作實際上可能由之前合併的另一個操作來執行。我們定義基於合併樹(combining tree)的計數器上的fetch-and-inc操作的可線性化點如下:當一個獲勝執行緒到達樹的根節點並將其累積值加到計數器上時,我們將其之前合併的操作線性化。這些操作根據之後被分發到對應操作的返回值的順序線性化。雖然詳細的可線性化證明超出了我們討論的範圍,但我們應該清楚即使是簡單併發資料結構的嚴格的正確性證明,也是相當具有挑戰性的。

直觀的吸引力和模組化使可線性化(linearizability)成為一個廣受歡迎的正確性條件。在本章剩餘部分我們討論的大部分併發資料結構實現都是可線性化的。然而,在某些情況下,效能和可擴充套件性可通過滿足較弱正確性得到提高。例如,靜態一致性(quiescent consistency)條件[10]降低了對總操作順序滿足實時排序的要求,但要求所有靜態狀態(其中無任何操作執行)之後執行的操作必須排在該狀態之前執行的操作之後。一個滿足這種弱正確性條件的實現是否有用跟應用有關。相比之下,可線性化的實現始終是有用的,因為設計者可以將其視為具有原子性。