說明
鎖定驗證可用於檢查程式中鎖定行為的一致性，以找出潛在的死結危險。本文件探討鎖定驗證的靜態和動態方法相關層面，並介紹 Zircon 和 Fuchsia 中可用的執行階段鎖定驗證程式庫的基礎。
背景
鎖定驗證可以透過靜態或動態方式執行。以下摘要說明鎖定驗證的靜態和動態方法間的重要差異：
- 進行驗證時：編譯時間和執行時間。
- 驗證工具對於找出潛在問題的成效。
- 程式設計師需要哪個等級的參與。
- 驗證本身的營運成本。
靜態驗證
靜態驗證通常會在編譯時間執行，方法是分析編譯器或其他來源層級處理器產生的呼叫圖。此方法需要檢測程式碼，並利用註解鎖定基元，向驗證工具告知哪些類型代表鎖定，以及要 (或不套用) 對使用鎖定類型的程式碼套用哪些規則。
靜態驗證的優點包括在建構時間及早偵測問題、確定性驗證結果，以及零的執行階段負擔。這種屬性組合有利於一律啟用靜態驗證，確保系統在將問題導入建構版本之前通常會擷取到鎖定問題，同時不影響建構構件的效能。
靜態驗證也會有一些缺點。其中一個問題是，靜態驗證需要正確且一致的套用多種註解，以便用於鎖定和程式碼，才能提供有用的結果。除非實作檢驗程式碼審查標準，否則這可能會導致維護問題。另一個問題是靜態驗證的瀏覽權限有限，可能會受到條件式路徑、動態分派、移動語意，以及跨多個編譯單元鎖定的依附元件欺騙。
動態驗證
系統會在執行階段在線上執行動態驗證，方法是在執行程式碼時觀察鎖定之間的關係。採用這種做法時，通常只要檢測鎖定基元和取得/發布作業，就能提供驗證所需的資訊。
動態驗證的優點包括簡化的檢測作業 (從使用者的角度來看)，或許能進一步掌握程式的實際執行階段行為。這可以讓動態驗證在大型程式碼集中更為實用，因為靜態驗證可能無法查看完整的可能鎖定互動組合。
動態驗證的主要缺點是執行階段負擔和執行涵蓋範圍需求。由於動態驗證必須追蹤執行階段的鎖定互動，因此每次取得和發布時，除了追蹤資料本身的記憶體負擔之外，每次取得和發布作業都會產生非零的執行費用。執行階段追蹤也會導致驗證工具無法分析未執行的程式碼路徑。這可能會增加開發人員和品質確保的負擔，確保即使尚未達到專案需求，也能確保足夠的執行涵蓋範圍。
鎖定順序不變
鎖定驗證工具的作用是判斷鎖定程式保留狀態是否不變。主要不變性是指兩個以上鎖定之間的順序：程式中獲得兩個或多個鎖定的路徑必須按照順序與包含兩個或更多相同鎖定的其他路徑保持一致，以避免發生死結。處理硬體中斷情形的環境 (例如嵌入式系統和核心) 會有額外的排序方式，以免因中斷造成的死結問題。這些不變量會在下列子區段中說明。
基本反轉
如果某個程式有兩個鎖定，但各自在不同路徑中的順序不一致，就發生了最簡單的反轉問題。
舉例來說，如果程式含有 A 和 B 鎖定，以及程式碼路徑 P1 和 P2，且下列行為可能有死結：
路徑 P1 取得並釋放序列：
- 開發(A)
- 開發(B)
- 版本(B)
- 版本(A)
路徑 P2 取得並釋放反轉序列中的鎖定：
- 開發(B)
- 開發(A)
- 版本(A)
- 版本(B)
如果採用正確的交錯方式，可能是因為兩個路徑同時在不同執行緒上執行，當路徑 P1 保留鎖定 A 和等待鎖定 B 的區塊，而 P2 會保留鎖定 B 和等待鎖定 A 的區塊，就會發生死結。
循環依附元件
兩個鎖定和路徑之間也可能會發生反轉。這類反向檢查很難透過手動檢查的方式辨識，因為每對牽涉的鎖定可能在僅涉及組合的每個路徑中都正確排序，但在對於鎖定的整體排序的情況下，可能還是會存在潛在的死結。
例如，具有鎖定 A、B 和 C 的程式；路徑 P1、P2 和 P3；下列行為具有死結的可能性：
路徑 P1 取得並釋放序列：
- 開發(A)
- 開發(B)
- 版本(B)
- 版本(A)
路徑 P2 取得並釋放序列：
- 開發(B)
- 開發(C)
- 版本(C)
- 版本(B)
路徑 P3 取得並釋放序列：
- 開發(C)
- 開發(A)
- 版本(A)
- 版本(C)
路徑 P1、P2 和 P3 右側交錯時，每條路徑在第一個步驟都取得鎖定，並在第二個步驟等待鎖定，就會發生死結。在這個情況下，可能會因為許多不同路徑產生相同的配對鎖定序列而變得複雜。
IRQ-安全訂購
如果系統處理硬體，會中斷 irq 安全和非 irq 安全鎖定之間的順序，就非常重要：不得在持有 irq 安全鎖定的情況下，取得非 irq 安全鎖定，避免間接鎖定反轉。Irq 安全鎖定會保留 irq 和非 irq 環境之間的排序；如果兩個或多個 irq 安全鎖定的順序一致，可確保在 irq 和非 irq 環境中執行的路徑安全無虞。非 irq 安全鎖定也是如此。之所以會這樣，是因為非 irq 安全鎖定允許 irq 處理常式有效插入處理常式取得的鎖定，這些鎖定在中斷任務的鎖定序列中。
例如，具有非 irq 安全鎖定 A 和 irq 安全鎖頭 Birq、路徑 P1、P2 和 irq 路徑 Pirq 的系統，這些行為都有可能導致死結：
CPU1 上的路徑 P1 會依序取得並釋放鎖定：
- 開發(A)
- Pirq 幹擾在 CPU1 上
- 版本(A)
CPU1 上的 Pirq 路徑會依序取得並釋放鎖定：
- 開發(Birq)
- 版本(irq)
CPU2 上的路徑 P2 會依序取得並釋放鎖定：
- 開發(Birq)
- 開發(A)
- 版本(A)
- 版本(irq)
在路徑 P1、P2 和 Pirq 中，Pirq 嘗試取得 Birq，而 P2 包含 Birq 和等待 A 的區塊時，就會發生死結。這是間接鎖定反轉：Pirq 在路徑 P1 中，有效將 Birq 的收購/釋放序列插入路徑 P1 的取得/釋放序列中間，而這與路徑 P2 中相同鎖定的鎖定序列不一致。
執行驗證
上一節討論的不變量可以使用有限導向圖進行驗證。當分析會在分析程式碼路徑時，有向圖可以追蹤鎖定的身分和鎖定順序。建立這類圖表的方式有兩種：週遊編譯器或來源層級處理器 (靜態分析) 產生的呼叫圖表，或是觀察程式執行期間的鎖定順序 (動態分析)。本節以抽象術語介紹流程，並應用到任一方法，為日後制定具體動態分析策略的準備工作。
通常來說，從程式碼路徑建構有向圖的原因是，在周遊路徑時，必須維護主動保留鎖定清單：每當取得鎖定時，代表鎖定的節點就會新增至清單中，並在鎖定發布時從清單中移除。除了保留使用中清單以外，圖表也會從代表新取得的頂點新增至圖表的頂點新增至圖表，代表清單中已有鎖定的鎖定。
基本反轉範例
本節說明偵測基本雙鎖定反轉的有向圖方法。
回想一下，在先前的範例中，有鎖定 A 和 B 的程式、程式碼路徑 P1 和 P2，以及下列行為：
路徑 P1 取得並釋放序列：
- 開發(A)
- 開發(B)
- 版本(B)
- 版本(A)
路徑 P2 取得並釋放反轉序列中的鎖定：
- 開發(B)
- 開發(A)
- 版本(A)
- 版本(B)
路徑分析 P1
從路徑 P1 開始，我們定義並更新有向圖。
讓 L1 成為路徑 P1 保留的已排序鎖定清單。
讓 G = (V、E) 成為有向圖，使用一組代表觀察到的鎖定點的頂點 V，以及頂點之間的有向邊緣組合 E。
初始狀態：
| L1 | V | E |
|---|---|---|
| () | {}敬上 | {}敬上 |
在 P1 步驟 1 之後：
| L1 | V | E |
|---|---|---|
| (A)。 | {A}敬上 | {}敬上 |
這個步驟會將鎖定 A 新增至使用中清單，並將相同鎖定的頂點導入有向圖。由於使用中清單中沒有其他鎖定，因此不會加入任何邊緣。
在 P1 步驟 2 之後：
| L1 | V | E |
|---|---|---|
| (A、B)。 | {A、B} | {(B, A)} |
這個步驟會將鎖頭的 B 新增至使用中的清單，並在圖表中加入對應的端點。目前的使用清單包含鎖定，因此系統會將新鎖定與現有鎖定的邊緣新增至圖形。此邊緣表示鎖定 B 現在「決定」在它之前的鎖定 A 於任何其他包含兩個鎖定的路徑之前。
在 P1 步驟 3 之後：
| L1 | V | E |
|---|---|---|
| (A)。 | {A、B} | {(B, A)} |
鎖定「B」已從使用清單中移除。沒有更新圖表。
在 P1 步驟 4 之後：
| L1 | V | E |
|---|---|---|
| () | {A、B} | {(B, A)} |
鎖定「A」已從有效清單中移除。沒有更新圖表。
路徑分析 P2
讓 L2 成為 P2 保留的鎖定清單。
初始狀態：
| L2 | V | E |
|---|---|---|
| () | {A、B} | {(B, A)} |
在這種情況下，初始狀態是路徑 P1 的最終狀態。
在 P2 步驟 1 之後：
| L2 | V | E |
|---|---|---|
| (B)。 | {A、B} | {(B, A)} |
這個步驟會將鎖定「B」新增至使用中清單。由於使用中的清單中並沒有其他鎖定，因此系統不會在圖形中加入任何邊緣。由於圖表中已有 B 的頂點，因此「V」也維持不變。
在 P2 步驟 2 之後：
| L2 | V | E |
|---|---|---|
| (B、A)。 | {A、B} | {(B, A), (A, B)} |
這個步驟會將鎖頭圖示 A 新增至使用中清單。由於這個鎖定已有端點，V 並不會變更。不過，由於使用中清單中有一個鎖頭從新鎖定到現有鎖定的邊緣，因此會加到圖表中。利用這個新邊緣，圖表現在會在頂點 A 和 B 之間形成一個循環，表示目前考慮的兩個路徑之間的順序不一致，但可能有死結。
循環依附元件範例
本節說明使用先前在「不變性」一節中討論的範例，偵測循環依附元件反轉的有向圖方法。這張插圖因為與上一張插圖相似，因此有些縮寫。
假設有鎖定 A、B 和 C 以及路徑 P1、P2 和 P3 的程式，以及下列行為：
路徑 P1 取得並釋放序列：
- 開發(A)
- 開發(B)
- 版本(B)
- 版本(A)
路徑 P2 取得並釋放序列：
- 開發(B)
- 開發(C)
- 版本(C)
- 版本(B)
路徑 P3 取得並釋放序列：
- 開發(C)
- 開發(A)
- 版本(A)
- 版本(C)
路徑分析 P1
讓 L1 成為路徑 P1 保留的已排序鎖定清單。
讓 G = (V、E) 成為有向圖，使用一組代表觀察到的鎖定點的頂點 V，以及頂點之間的有向邊緣組合 E。
初始狀態：
| L1 | V | E |
|---|---|---|
| () | {}敬上 | {}敬上 |
在 P1 步驟 1 之後：
| L1 | V | E |
|---|---|---|
| (A)。 | {A}敬上 | {}敬上 |
在 P1 步驟 2 之後：
| L1 | V | E |
|---|---|---|
| (A、B)。 | {A、B} | {(B, A)} |
在 P1 步驟 3 之後：
| L1 | V | E |
|---|---|---|
| (A)。 | {A、B} | {(B, A)} |
在 P1 步驟 4 之後：
| L1 | V | E |
|---|---|---|
| () | {A、B} | {(B, A)} |
路徑分析 P2
讓 L2 是路徑 P2 保留的有效鎖定清單。
初始狀態：
| L2 | V | E |
|---|---|---|
| () | {A、B} | {(B, A)} |
在 P2 步驟 1 之後：
| L2 | V | E |
|---|---|---|
| (B)。 | {A、B} | {(B, A)} |
在 P2 步驟 2 之後：
| L2 | V | E |
|---|---|---|
| (B、C)。 | {A、B、C} | {(B, A), (C, B)} |
此步驟會將鎖定 C 新增至使用中的清單，並在圖表中加入對應的端點。使用中的清單包含鎖定「B」，因此邊緣已從 C 新增至 B。
在 P2 步驟 3 之後：
| L2 | V | E |
|---|---|---|
| (B)。 | {A、B、C} | {(B, A), (C, B)} |
在 P2 步驟 4 之後：
| L2 | V | E |
|---|---|---|
| () | {A、B、C} | {(B, A), (C, B)} |
路徑分析 P3
讓 L3 是路徑 P3 保留的已排序鎖定清單。
初始狀態：
| L3 | V | E |
|---|---|---|
| () | {A、B、C} | {(B, A), (C, B)} |
在 P3 步驟 1 之後：
| L3 | V | E |
|---|---|---|
| (C)。 | {A、B、C} | {(B, A), (C, B)} |
在 P3 步驟 2 後：
| L3 | V | E |
|---|---|---|
| (C、A)。 | {A、B、C} | {(B, A), (C, B), (A, C)} |
這個步驟會將鎖頭圖示 A 新增至使用中清單。使用中的清單包含鎖頭「C」，因此邊緣是從 A 新增至 C。利用這個新邊緣，圖表現在會在頂點 (A、B、C) 形成一個循環，意味著如果路徑 P1、P2 和 P3 以正確方式交錯，就會出現循環相依性和死結的可能性。
IRQ-Safe 排序範例
本節說明以「invariants」(獨立變數) 一節中提及的範例來偵測 Iq-safe 順序違規行為的有向圖方法。
使用非 irq 安全鎖定 A 和 irq 安全鎖頭 Birq、路徑 P1、P2 和 irq 路徑 Pirq 等方法請回想範例系統。請注意，這些行為如下：
路徑 P1 會依序取得及釋放鎖定：
- 開發(A)
- 版本(A)
路徑 Pirq 會依序取得及釋放鎖定：
- 開發(Birq)
- 版本(irq)
路徑 P2 會依序取得及釋放鎖定：
- 開發(Birq)
- 開發(A)
- 版本(A)
- 版本(irq)
路徑分析 P1
讓 L1 成為路徑 P1 保留的已排序鎖定清單。
讓 G = (V、E) 成為有向圖，使用一組代表觀察到的鎖定點的頂點 V，以及頂點之間的有向邊緣組合 E。
初始狀態：
| L1 | V | E |
|---|---|---|
| () | {}敬上 | {}敬上 |
在 P1 步驟 1 之後：
| L1 | V | E |
|---|---|---|
| (A)。 | {A}敬上 | {}敬上 |
在 P1 步驟 2 之後：
| L1 | V | E |
|---|---|---|
| () | {A}敬上 | {}敬上 |
路徑分析 Pirq
讓 Lirq 是路徑 Pirq 所保留的有效鎖定清單。
初始狀態：
| Lirq | V | E |
|---|---|---|
| () | {A}敬上 | {}敬上 |
在 Pirq 步驟 1 之後：
| Lirq | V | E |
|---|---|---|
| (irq)。 | {A、Birq} | {}敬上 |
在 Pirq 步驟 2 之後：
| Lirq | V | E |
|---|---|---|
| () | {A、Birq} | {}敬上 |
路徑分析 Pirq
讓 L2 是路徑 P2 保留的有效鎖定清單。
初始狀態：
| L2 | V | E |
|---|---|---|
| () | {A}敬上 | {}敬上 |
在 P2 步驟 1 之後：
| L2 | V | E |
|---|---|---|
| (irq)。 | {A、Birq} | {}敬上 |
在 P2 步驟 2 之後：
| L2 | V | E |
|---|---|---|
| (Birq、A) | {A、Birq} | {(A, Birq)} |
這個步驟會將鎖頭圖示 A 新增至使用中清單。使用中的清單包含鎖頭 Birq，因此邊緣會從 A 新增至 Birq。因為這是從非 irq 安全鎖定改為 irq 安全鎖定 的邊緣，不會違反 irq-safe 順序的變體，並存在潛在的死結。
從理論到實作
本節會根據上一節的分析技巧，開發實作有向圖驗證的具體策略。
這項導入策略有以下目標：
- 請盡量避免使用動態分配。
- 將驗證作業的負擔降至最低。
- 支援管理硬體中斷情形的環境。
使用鎖定類別移除備援功能
在本文件之前的分析中，將追蹤物件視為個別鎖定的執行個體，因此將鎖定視為抽象化。雖然追蹤個別例項可以產生正確的結果，但可能會避免以下幾點：
- 當鎖定執行個體進入或不存在時，追蹤結構必須動態調整，這可能需要動態分配或其他個別執行個體的資料儲存空間。
- 如果有多個鎖定例項由相同的程式碼路徑使用，則圖表會包含備援資訊。
- 相對地，如果鎖定提供相同函式，但尚未逐一傳播所有必要的程式碼路徑，可能需要更長的時間才能識別違規行為。
重要的觀察是，無論執行個體數量為何，提供相同函式的鎖定都應遵循相同的排序規則。
請考量下列類型有鎖定成員，以及會變動這兩種類型的作業：
struct Foo {
Mutex lock;
int data; GUARDED_BY(lock);
};
struct Bar {
Mutex lock;
int data; GUARDED_BY(lock);
};
void Swap(Foo* foo, Bar* bar) {
foo->lock.Acquire();
bar->lock.Acquire();
int temp = foo->data;
foo->data = bar->data;
bar->data = temp;
bar->Release();
foo->Release();
}
由於 Swap 作業可在 Foo 的任何執行個體和 Bar 的任何例項上運作，因此 Swap 會在 Foo 和 Bar 的所有例項的鎖定之間建立順序；如果未將順序套用至程式的其他部分，則當相同的 Foo 和 Bar 執行個體同時鎖定不同順序時，可能會導致死結。
請注意，可能會刻意或無意間隔離不同的 Foo 和 Bar 集合，使鎖定不同順序的執行個體不會重疊。但是，這仍是危險的，因為程式的輸入內容、結構或時間如果幾乎沒有改變，可能會打破劃分並造成潛在死結。如要完全避免這個問題，您可以同等處理 Foo 和 Bar 的所有例項，並在程式中套用相同的排序規則。
透過追蹤鎖定類別 (而非鎖定例項) 的做法，確保程式中所有的通用排序都能達成：每種類型的鎖定成員都代表一個專屬的鎖定類別。如要追蹤及分析每個鎖定類別之間的關係，您可以使用與個別鎖定相同的有向圖技巧。
追蹤鎖定類別具有以下優點：
- 靜態分配的記憶體：由於所有鎖定類別在編譯期間已知，因此追蹤結構可以預先分配為靜態全域資料。
- 消除多餘圖節點：同一類別中的鎖定使用相同的追蹤結構。
- 更快速地偵測變化版本違規事件：即使鎖定的個別執行個體從未一起使用，只要鎖定類別順序不一致，就會偵測違規事件。
其他排序規則
鎖定同一類別的多個鎖定時，追蹤鎖定類別會產生額外的排序注意事項。由於系統不會追蹤個別執行個體，因此在必須同時取得相同類別的多個鎖定時，必須採取額外步驟以確保一致性。
外接式鎖
當階層或其他已排序的資料結構在每個節點中鎖定，且每個節點必須同時保留多個，需要同類別的巢狀鎖定。在這種情況下，資料結構或存取模式必須提供穩定的順序，用來保證鎖定順序。
驗證可巢狀鎖定類別時，您只需要記錄每個可巢狀鎖定在有效鎖定清單中的外部順序，並且在相同類別的新鎖定加入清單時進行比較。這項設計的結果是，其他鎖定類別不得交錯在相同類別的巢狀鎖定之間，只有巢狀鎖定在集合之前或之後。
例如，非巢狀鎖定類別 A 和 B 以及可巢狀鎖定類別 N 可能是這樣交錯的：
A、N0、N1、... Nn、B
但不喜歡：
A、N0、B、N1... Nn 或 A、N0、N1、B、... Nn 等...
在大部分情況下，這是合理的限制，因為在執行階段更新結構時，將其他鎖定在巢狀結構結構內交錯會改用其他鎖定，因此可能會導致反轉。另一方面，如果巢狀結構綁定幾個層級，則為每個層級定義獨立的鎖定類別 (而非使用巢狀類別) 可能更有效率，在此情況下，您可以在符合一般鎖定排序規則的特定層級允許其他鎖定。
地址訂購
如果在不同時間取得鎖定，就很難將相同類別的鎖定順序一般化，除非使用外部提供的順序。不過，在同時獲取多個鎖定時，在不進行時間分隔的情況下，可提供訂購保證。在這種情形下，鎖定順序可能會按照地址排序，藉此確保取得相同組合鎖定的任何路徑都能產生一致的鎖定順序。
例如，假設作業 F(Sa、Sb) 在結構 S 的兩個例項上運作，每個執行個體都有 L 類別的鎖定，且在作業 F 作業過程中，必須同時鎖定兩個鎖定。
如果執行個體 S
如果我們以不同順序執行作業，就會發生鎖定順序問題：
F(S0, S1) 和 F(S1, S0)
在沒有介入的情況下，這些指令會產生反轉的鎖定序列：
L0、L1 和 L1、L0
由於 F 可以同時存取這兩個鎖定，因此可依地址排序鎖定，因此無論引數的原始順序為何，都會產生一致的鎖定序列。
現在，我們如果在序列中另外新增兩個鎖定類別：在作業 F 之前取得的類別 A，以及作業 F 後取得的類別 B。產生的鎖定序列為：
A、L0、L1、B
請注意，這與上一節的巢狀鎖定類別序列圖表類似。實際上，鎖定順序也是由地址提供，而非外部順序。這表示在這兩種情況下，使用中的執行緒清單中可以使用相同的簿記。
鎖定類別追蹤資料結構
本節說明追蹤鎖定類別的實作詳細資料，以及具體處理技術來偵測潛在的死結。
每個鎖定類別在導向圖中都有一個靜態分配的節點，代表屬於該類別的所有鎖定。每個節點都具有下列資料結構：
無鎖版、免費等待雜湊集
每個鎖定類別節點都有雜湊組合，用於追蹤從鎖定類別到先後順序鎖定類別的邊緣。
TODO：新增雜湊集的實作詳細資料。
防鎖無鎖版功能隔閡組結構
每個鎖定類別節點都有一個父項指標，用來追蹤在引導圖中處於連接週期的節點。這可允許原本由迴圈偵測演算法產生的報表週期，不必完全反向掃遍圖表。
TODO：新增不連續集結構的實作詳細資料。
執行緒本機鎖定清單
每個執行緒都有一個執行緒目前保留的執行緒本機清單，
TODO：新增執行緒本機鎖定清單的實作詳細資料。
環狀偵測執行緒
每當將新的邊緣新增至導向圖時，系統都會觸發迴圈偵測執行緒以掃遍圖表，以找出涉及超過兩個鎖定的循環依附元件。Tarjan 的密切連結組合演算法是有效率的選擇，其中 O(|E| + |V|) 最為複雜。即使周遊由其他執行緒同時更新的圖形，這個演算法仍保持穩定。
TODO：新增迴圈偵測執行緒的實作詳細資料。
參考資料
- Clang 靜態執行緒安全性分析。
- LLVM 執行階段執行緒清理工具。
- Linux 核心 lockdep 子系統。