簡介
鎖定驗證是一種檢查鎖定行為一致性的技術 計畫中，找出潛在的死結危險。本文件討論 針對鎖定驗證和鎖定驗證的靜態和動態方法 說明瞭執行階段鎖定驗證程式庫的基礎 Zircon 和 Fuchsia。
背景
鎖定驗證可靜態或動態執行。下列 總結了靜態和動態方法之間的重要差異 鎖定驗證：
- 執行驗證時：編譯時間與執行時間。
- 驗證工具找出潛在問題的成效。
- 程式設計人員所需的參與程度。
- 驗證本身的經常性費用。
靜態驗證
靜態驗證通常是透過分析呼叫，以在編譯期間執行 編譯器或其他來源層級的處理器產生的圖形。使用這項 對程式碼進行檢測和鎖定原始物件時， 註解，用於通知驗證工具哪些類型代表鎖定，以及 規則，套用至使用鎖定類型的程式碼。
靜態驗證的優點包括在建構時及早發現問題 時間、確定性驗證結果，以及零執行階段負擔。這個 所以需要一律啟用靜態驗證 確保在程式碼傳入 而且不會影響建構構件的效能
Static 驗證也有一些缺點。其中一個問題是靜態的 必須對各種註解套用正確且一致的套用方式，才能進行驗證 進而提供實用的結果這可能會造成維護作業 不會產生問題。另一個問題是 靜態驗證的能見度有限，且可能會遭到條件式驗證 路徑、動態調度、移動語意，以及鎖定 編譯單位。
動態驗證
動態驗證會觀察關聯，以在執行階段線上執行 並在程式碼執行時切換鎖定。使用這個方法時 足以處理上鎖和取得/釋放 來提供驗證所需的資訊。
動態驗證的優點包括較簡單的檢測 更有機會深入瞭解實際執行階段 程式的行為。這樣一來，動態驗證就能用於大型程式碼中 但靜態驗證可能就無法透過 可能的鎖定互動組合
動態驗證的主要缺點為執行階段負擔和執行作業 承保範圍因為動態驗證功能必須追蹤鎖定互動 在執行階段中，每次取得和發布版本都會產生非零的更新執行成本 追蹤資料及追蹤資料本身的記憶體負荷。 執行階段追蹤也會導致程式碼路徑未執行 驗證工具無法加以分析這可能會增加 開發人員和品質確保，確保若尚未擴大執行作業涵蓋範圍 滿足專案需求
鎖定順序不變
鎖定驗證工具的工作是判斷鎖定是否不變 持續維護。主要的不變體是指兩個以上的 鎖定：在程式中取得兩個以上鎖定的所有路徑時，必須在 順序與包含兩個以上相同鎖定的每條路徑一致 避免潛在的死結處理硬體的環境 中斷點，如嵌入式系統和核心 以避免中斷的死結。這張圖呈現了 在接下來的幾個子節中
基本反轉
最簡單的反轉形式，當程式具有兩組鎖定 兩者順序不一致，且順序不同。
例如，程式具有 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-safe 鎖定，以防止間接鎖定反轉。符合 Irq 安全鎖 在 irq 與非 irq 結構定義之間保留順序；保持一致 在 irq 與 非 IR 的背景資訊對於非 SSL 安全鎖定的情況也是如此。原因如下 非安全鎖定允許 irq 處理常式能有效插入鎖定 由處理常式在中斷工作鎖定中的任何時間點取得 序列。
舉例來說，假設系統具有不安全的鎖定 A 和 irq-safe 鎖定 Birq；path P1、P2 和 irq path Pirq;具有以下行為的可能出現死結：
CPU1 上的路徑 P1 會依序取得並釋出鎖定：
- 開發(A)
- Pirq 會在 CPU1 中斷
- 版本(A)
CPU1 上的路徑 Pirq 會依序取得並釋出鎖定：
- 開發(Birq)
- 版本(Birq)
CPU2 上的路徑 P2 會依序取得並釋出鎖定：
- 開發(Birq)
- 開發(A)
- 版本(A)
- 版本(Birq)
採用正確的交錯路徑 P1、P2 和 當 Pirq 嘗試獲取死記時，就會發生死結 Birq，P2 會保留 Birq 和區塊 等待 A。這是間接鎖定反轉：Pirq 有效插入 Birq 的取得/發布序列 A 取得/發布序列在路徑 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，現在一律「依附」鎖定 B，其於 其他涉及兩個鎖定的路徑
在 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 Ordering 範例
本節說明用於偵測不合格順序的引導式圖方法 違反先前討論的變化版本範例
使用不安全的鎖定 A 和 irq-safe 鎖頭來回顧範例系統 Birq；path P1、P2 和 irq path Pirq;包含下列行為：
路徑 P1 會依序取得並釋放鎖定：
- 開發(A)
- 版本(A)
路徑 Pirq 會依序取得並釋放鎖定：
- 開發(Birq)
- 版本(Birq)
路徑 P2 可依序取得並釋放鎖定：
- 開發(Birq)
- 開發(A)
- 版本(A)
- 版本(Birq)
路徑分析 P1
讓 L1 依路徑持有的有效鎖定清單 P1。
讓 G = (V, E) 為有向圖，且有一組頂點 V 表示觀察到的鎖定和頂點之間的方向邊緣組合 E：
初始狀態：
| L1 | V | E 鍵 |
|---|---|---|
| () | {} | {} |
在 P1 步驟 1 之後：
| L1 | V | E 鍵 |
|---|---|---|
| (A)。 | {A} | {} |
在 P1 步驟 2 之後：
| L1 | V | E 鍵 |
|---|---|---|
| () | {A} | {} |
路徑分析
讓 Lirq 依路徑保留的「有效」鎖定清單 Pirq：
初始狀態：
| Lirq | V | E 鍵 |
|---|---|---|
| () | {A} | {} |
在 Pirq 步驟 1 後：
| Lirq | V | E 鍵 |
|---|---|---|
| (Birq)。 | {A、Birq} | {} |
在 Pirq 步驟 2 後：
| Lirq | V | E 鍵 |
|---|---|---|
| () | {A、Birq} | {} |
路徑分析
讓 L2 依路徑持有的有效鎖定清單 P2：
初始狀態：
| L2 | V | E 鍵 |
|---|---|---|
| () | {A} | {} |
P2 步驟 1 之後：
| L2 | V | E 鍵 |
|---|---|---|
| (Birq)。 | {A、Birq} | {} |
P2 步驟 2 之後：
| L2 | V | E 鍵 |
|---|---|---|
| (Birq、A) | {A、Birq} | {(A, Birq)} |
這個步驟會將鎖定 A 新增至有效清單。有效清單包含鎖定功能 Birq，因此從 A 加入邊緣來從 Birq 加入。 此為邊緣安全鎖的邊緣，而不受 irq-safe 鎖定的特性 違反順序不變，而且可能有死結。
從理論到實踐
本節會制定具體策略來實作有向圖 驗證工具是以上一節的分析技巧為基礎。
導入策略的目標如下：
- 請盡可能避免使用動態分配。
- 將驗證負擔降至最低。
- 支援管理硬體中斷的環境。
使用鎖定類別移除備援功能
在本文件前述的分析中，鎖定法只視為 所追蹤的物件屬於個別鎖定的執行個體。 追蹤個別例項會產生正確的結果，但具有多項 可能避免的結果：
- 追蹤結構必須隨鎖定執行個體動態調整 且可能就需要動態分配 每個執行個體的資料儲存空間
- 如有多個鎖定例項，圖表中即包含冗餘資訊 相同的程式碼路徑
- 相對來說，如果鎖定功能採行的鎖定方式，可能需要更長的時間才能找出違規行為 但尚未在所有 Pod 中個別傳播 所需的程式碼路徑
主要觀察是，提供相同函式的鎖定必須遵循 排列順序規則相同，無論執行個體數量為何。
請思考以下類型，這些類型包含鎖定成員，以及可變動的作業 這兩種語言
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 可同時存取這兩種鎖定，因此 如此一來，就能依地址排序鎖定，導致鎖定的 則無論引數的原始順序為何。
現在，假設序列中還有兩個鎖定類別：已取得 A 類別 操作 F 和 B 之後取得 F。 結果鎖定序列為：
A、L0、L1、B
請注意，這看起來類似 請參閱上一節的說明。事實上也是如此，只有鎖定的順序 提供地址，而非外部訂單。也就是說 這兩種情況下，使用中討論串清單中的簿記皆適用。
鎖定類別追蹤資料結構
本節將探討追蹤鎖定類別及 具體的處理技術，偵測潛在的死結。
每個鎖定類別的有向圖都有一個靜態分配的節點 代表該類別的所有鎖定。每個節點包含下列資料 結構：
免上鎖的雜湊組合
每個鎖定類別節點都有一組雜湊碼，可追蹤從鎖定類別到 先依順序排序鎖定類別
TODO：新增雜湊集的實作詳細資料。
免上鎖、不等待斷裂組合結構物
每個鎖定類別節點都有一個父項指標，用於追蹤連接的節點。 週期範圍。這樣可以確保 才會完全逆轉圖形。
TODO：新增不相交組合結構的實作詳細資料。
Thread-本機鎖定清單
每個執行緒都會保留一份目前保留的鎖定的執行緒本機清單。
TODO：新增執行緒本機鎖定清單的實作詳細資料。
環狀偵測執行緒
每當有新邊緣加入有向圖時，迴圈偵測執行緒就會 會觸發週遊圖表，找出涉及超過 有兩個鎖定。Tarjan 緊密連結集演算法是一個很有效率的選擇 最糟的情況是 O(|E| + |V|)。這個演算法的穩定性 且即使掃遍了由其他執行緒同時更新的圖表也是如此。
TODO：新增迴圈偵測執行緒的實作詳細資料。
參考資料
- Clang 靜態執行緒安全分析。
- LLVM 執行階段執行緒清理工具。
- Linux 核心的 lockdep 子系統。