英語

• 義大利語

執行時鎖正確性驗證器

由 Ingo Molnar <mingo@redhat.com> 啟動

由 Arjan van de Ven <arjan@linux.intel.com> 新增

鎖類 (Lock-class)

驗證器操作的基本物件是鎖的“類”。

鎖類是鎖的一個組，它們在邏輯上是相同的，符合鎖定規則，即使鎖可能有多個（可能數萬個）例項。 例如，inode 結構中的鎖是一個類，而每個 inode 都有該鎖類的自己的例項化。

驗證器跟蹤鎖類的“使用狀態”，並跟蹤不同鎖類之間的依賴關係。 鎖使用情況表明鎖是如何用於其 IRQ 上下文的，而鎖依賴性可以理解為鎖順序，其中 L1 -> L2 表示任務嘗試在持有 L1 時獲取 L2。 從 lockdep 的角度來看，這兩個鎖（L1 和 L2）不一定相關； 這種依賴關係只是意味著該順序曾經發生過。 驗證器不斷努力證明鎖的使用和依賴關係是正確的，否則驗證器會發出錯誤資訊。

鎖類的行為由其所有例項共同構建：當啟動後使用鎖類的第一個例項時，該類會被註冊，然後所有（後續）例項將被對映到該類，因此它們的用法和依賴關係將有助於該類的用法和依賴關係。 鎖類不會在鎖例項消失時消失，但如果鎖類（靜態或動態）的記憶體空間被回收，則可以將其刪除，例如，當模組被解除安裝或工作佇列被銷燬時。

狀態 (State)

驗證器跟蹤鎖類使用歷史記錄，並將使用情況分為 (4 種用法 * n 個狀態 + 1) 個類別

其中 4 種用法可以是

• “在狀態上下文中曾經被持有”

• “在狀態上下文中曾經作為讀鎖被持有”

• “在啟用狀態的情況下曾經被持有”

• “在啟用狀態的情況下曾經作為讀鎖被持有”

其中 n 個狀態在 kernel/locking/lockdep_states.h 中編碼，截至目前包括

• 硬中斷 (hardirq)

• 軟中斷 (softirq)

其中最後一個類別是

• “曾經被使用” [ == !unused ]

當鎖定規則被違反時，這些使用位會顯示在鎖定錯誤訊息中，位於花括號內，總共有 2 * n 個狀態位。 一個虛構的例子

modprobe/2287 is trying to acquire lock:
 (&sio_locks[i].lock){-.-.}, at: [<c02867fd>] mutex_lock+0x21/0x24

but task is already holding lock:
 (&sio_locks[i].lock){-.-.}, at: [<c02867fd>] mutex_lock+0x21/0x24

對於給定的鎖，從左到右的位位置分別指示每個上面列出的 n 個狀態的鎖和讀鎖（如果存在）的使用情況，並且每個位位置上顯示的字元指示

“.”	在停用中斷且不在中斷上下文的情況下獲取
“-”	在中斷上下文中獲取
“+”	在啟用中斷的情況下獲取
“？”	在啟用中斷的情況下在中斷上下文中獲取。

這些位用一個例子來說明

(&sio_locks[i].lock){-.-.}, at: [<c02867fd>] mutex_lock+0x21/0x24
                     ||||
                     ||| \-> softirq disabled and not in softirq context
                     || \--> acquired in softirq context
                     | \---> hardirq disabled and not in hardirq context
                      \----> acquired in hardirq context

對於給定的狀態，無論鎖是否曾經在該狀態上下文中獲取，以及該狀態是否啟用，都會產生如下表所示的四種可能情況。 位字元能夠指示報告時鎖的確切情況。

	啟用中斷	停用中斷
曾經在中斷中	“？”	“-”
從未在中斷中	“+”	“.”

字元“-”表示停用了中斷，因為否則會顯示字元“？”。 類似的推論也適用於“+”。

未使用的鎖（例如，互斥鎖）不能成為錯誤的原因。

單鎖狀態規則：

一個鎖是中斷安全的，意味著它曾經在中斷上下文中被使用過，而一個鎖是中斷不安全的，意味著它曾經在啟用中斷的情況下被獲取過。

軟中斷不安全的鎖類也自動是硬中斷不安全的。 以下狀態必須是互斥的：基於其用法，任何鎖類只允許設定其中一個

<hardirq-safe> or <hardirq-unsafe>
<softirq-safe> or <softirq-unsafe>

這是因為如果一個鎖可以在中斷上下文中使用（中斷安全），那麼它不能在啟用中斷的情況下獲取（中斷不安全）。 否則，可能會發生死鎖。 例如，在這種鎖被獲取但尚未釋放的情況下，如果上下文被中斷，則會嘗試兩次獲取此鎖，從而導致死鎖，稱為鎖遞迴死鎖。

驗證器檢測並報告違反這些單鎖狀態規則的鎖使用情況。

多鎖依賴規則：

同一個鎖類不得被獲取兩次，因為這可能導致鎖遞迴死鎖。

此外，不能以相反的順序獲取兩個鎖

<L1> -> <L2>
<L2> -> <L1>

因為這可能導致死鎖 - 稱為鎖反轉死鎖 - 因為嘗試獲取兩個鎖形成一個迴圈，這可能導致兩個上下文永久地相互等待。 驗證器將找到這種任意複雜度的依賴關係圈，即，在 acquire-lock 操作之間可以有任何其他的鎖定序列； 驗證器仍然會找到這些鎖是否可以以迴圈的方式獲取。

此外，以下基於用法的鎖依賴關係在任何兩個鎖類之間都是不允許的

<hardirq-safe>   ->  <hardirq-unsafe>
<softirq-safe>   ->  <softirq-unsafe>

第一條規則來自以下事實：硬中斷安全的鎖可能被硬中斷上下文獲取，從而中斷硬中斷不安全的鎖 - 因此可能導致鎖反轉死鎖。 同樣，軟中斷安全的鎖可能被軟中斷上下文獲取，從而中斷軟中斷不安全的鎖。

以上規則適用於核心中發生的任何鎖定序列：當獲取新鎖時，驗證器會檢查新鎖和任何持有的鎖之間是否存在任何規則衝突。

當鎖類改變其狀態時，將執行以上依賴規則的以下方面

• 如果發現新的硬中斷安全鎖，我們會檢查它是否在過去獲取過任何硬中斷不安全的鎖。

• 如果發現新的軟中斷安全鎖，我們會檢查它是否在過去獲取過任何軟中斷不安全的鎖。

• 如果發現新的硬中斷不安全鎖，我們會檢查是否任何硬中斷安全的鎖在過去獲取過它。

• 如果發現新的軟中斷不安全鎖，我們會檢查是否任何軟中斷安全的鎖在過去獲取過它。

（同樣，我們進行這些檢查的原因是，中斷上下文可能會中斷_任何_中斷不安全或硬中斷不安全的鎖，這可能會導致鎖反轉死鎖 - 即使該鎖場景尚未在實踐中觸發。）

例外情況：導致巢狀鎖定的巢狀資料依賴關係

在某些情況下，Linux 核心會獲取同一鎖類的多個例項。 這種情況通常發生在同一型別的物件中存在某種層次結構時。 在這些情況下，兩個物件之間存在固有的“自然”順序（由層次結構的屬性定義），並且核心以這種固定的順序獲取每個物件的鎖。

這種導致“巢狀鎖定”的物件層次結構的一個例子是“整個磁碟”塊裝置物件和“分割槽”塊裝置物件； 分割槽是“整個裝置的一部分”，只要始終將整個磁碟鎖作為比分割槽鎖更高的鎖，鎖順序就完全正確。 驗證器不會自動檢測到這種自然順序，因為該順序背後的鎖定規則不是靜態的。

為了讓驗證器瞭解這種正確的使用模型，添加了各種鎖定原語的新版本，允許您指定“巢狀級別”。 塊裝置互斥鎖的一個示例呼叫如下

enum bdev_bd_mutex_lock_class
{
     BD_MUTEX_NORMAL,
     BD_MUTEX_WHOLE,
     BD_MUTEX_PARTITION
};

mutex_lock_nested(&bdev->bd_contains->bd_mutex, BD_MUTEX_PARTITION);

在這種情況下，鎖定是在已知是分割槽的 bdev 物件上完成的。

驗證器將以這種巢狀方式獲取的鎖視為用於驗證的單獨（子）類。

注意：在更改程式碼以使用 _nested() 原語時，請務必小心並徹底檢查層次結構是否正確對映； 否則，您可能會得到誤報或漏報。

註解

可以使用兩個構造來註釋和檢查何時以及是否必須持有某些鎖：lockdep_assert_held*(&lock) 和 lockdep_*pin_lock(&lock)。

顧名思義，lockdep_assert_held* 系列宏斷言在特定時間持有特定鎖（否則會生成 WARN()）。 此註解在核心中被廣泛使用，例如 kernel/sched/ core.c

void update_rq_clock(struct rq *rq)
{
      s64 delta;

      lockdep_assert_held(&rq->lock);
      [...]
}

其中需要持有 rq->lock 才能安全地更新 rq 的時鐘。

另一系列宏是 lockdep_*pin_lock()，不得不承認，它僅用於 rq->lock ATM。 儘管它們的採用有限，但如果感興趣的鎖被“意外”解鎖，這些註解會生成 WARN()。 事實證明，這對於除錯帶有回撥的程式碼特別有幫助，在回撥程式碼中，上層假定鎖仍然被持有，但下層認為它可以可能地放棄並重新獲取鎖（“無意中”引入競爭）。 lockdep_pin_lock() 返回一個“struct pin_cookie”，然後 lockdep_unpin_lock() 使用它來檢查是否有人篡改了鎖，例如 kernel/sched/sched.h

static inline void rq_pin_lock(struct rq *rq, struct rq_flags *rf)
{
      rf->cookie = lockdep_pin_lock(&rq->lock);
      [...]
}

static inline void rq_unpin_lock(struct rq *rq, struct rq_flags *rf)
{
      [...]
      lockdep_unpin_lock(&rq->lock, rf->cookie);
}

雖然關於鎖定要求的註釋可能提供有用的資訊，但註解執行的執行時檢查在除錯鎖定問題時非常寶貴，並且在檢查程式碼時具有相同的詳細程度。 如有疑問，請始終首選註解！

100% 正確性的證明：

驗證器實現了完美的、數學上的“閉包”（鎖定正確性的證明），因為對於核心生命週期內至少發生過一次的每個簡單的、獨立的單任務鎖定序列，驗證器以 100% 的確定性證明了這些鎖定序列的任何組合和時間安排都不會導致任何類別的鎖相關死鎖。 [1]

也就是說，複雜的 multi-CPU 和 multi-task 鎖定場景不必在實踐中發生才能證明死鎖：只有簡單的“元件”鎖定鏈必須至少發生一次（任何時間，在任何任務/上下文中），驗證器才能證明正確性。 （例如，通常需要 3 個以上的 CPU 和任務、中斷上下文和時間安排的非常不可能的星座才能發生的複雜死鎖也可以在普通的、負載較輕的單 CPU 系統上檢測到！）

這從根本上降低了核心鎖定相關 QA 的複雜性：QA 期間必須做的是在核心中儘可能多地觸發“簡單”的單任務鎖定依賴關係，至少一次，以證明鎖定正確性 - 而不是必須觸發 CPU 之間鎖定互動的每種可能組合，以及每種可能的硬中斷和軟中斷巢狀場景（這在實踐中是不可能做到的）。

[1]

假設驗證器本身是 100% 正確的，並且系統的其他部分不會以任何方式破壞驗證器的狀態。 我們還假設所有 NMI/SMM 路徑[即使是停用硬中斷的程式碼路徑也可能被中斷]都是正確的，並且不會干擾驗證器。 我們還假設 64 位“鏈雜湊”值對於系統中的每個鎖鏈都是唯一的。 此外，鎖遞迴不得高於 20。

效能：

以上規則需要大量的執行時檢查。 如果我們對每次獲取鎖和每次啟用中斷事件都這樣做，這將使系統實際上慢得無法使用。 檢查的複雜性是 O(N^2)，因此即使只有幾百個鎖類，我們也不得不對每個事件進行數萬次檢查。

透過僅檢查任何給定的“鎖定場景”（彼此獲取的鎖的唯一序列）一次來解決此問題。 維護一個簡單的持有鎖堆疊，並計算一個輕量級的 64 位雜湊值，該雜湊值對於每個鎖鏈都是唯一的。 首次驗證鏈時，雜湊值隨後被放入雜湊表中，可以在無鎖方式下檢查該雜湊表。 如果鎖定鏈稍後再次發生，雜湊表會告訴我們不必再次驗證該鏈。

問題排查：

驗證器最多跟蹤 MAX_LOCKDEP_KEYS 個鎖類。 超過此數量將觸發以下 lockdep 警告

(DEBUG_LOCKS_WARN_ON(id >= MAX_LOCKDEP_KEYS))

預設情況下，MAX_LOCKDEP_KEYS 當前設定為 8191，並且典型的桌面系統具有少於 1,000 個鎖類，因此此警告通常由鎖類洩漏或無法正確初始化鎖導致。 以下說明了這兩個問題

1. 執行驗證器時重複載入和解除安裝模組將導致鎖類洩漏。 這裡的問題是，每次載入模組都會為該模組的鎖建立一組新的鎖類，但解除安裝模組不會刪除舊類（請參閱下面關於重用鎖類的討論，瞭解原因）。 因此，如果重複載入和解除安裝該模組，鎖類的數量最終將達到最大值。

2. 使用諸如陣列之類的結構，這些結構具有大量未顯式初始化的鎖。 例如，具有 8192 個儲存桶的雜湊表，其中每個儲存桶都有自己的 spinlock_t，將消耗 8192 個鎖類 - 除非 - 每個自旋鎖在執行時顯式初始化，例如，使用執行時 spin_lock_init() 而不是編譯時初始化器，例如 __SPIN_LOCK_UNLOCKED()。 無法正確初始化每個儲存桶的自旋鎖將保證鎖類溢位。 相比之下，在每個鎖上呼叫 spin_lock_init() 的迴圈會將所有 8192 個鎖放入單個鎖類。

   這個故事的寓意是您應該始終顯式初始化您的鎖。

有人可能會爭辯說，應該修改驗證器以允許重用鎖類。 但是，如果您想提出此論點，請首先檢視程式碼並仔細考慮所需的更改，同時牢記要刪除的鎖類可能已連結到鎖依賴關係圖中。 事實證明，這比說說要難做到。

當然，如果您確實用完了鎖類，那麼接下來要做的就是找到有問題的鎖類。 首先，以下命令為您提供當前正在使用的鎖類數量以及最大值

grep "lock-classes" /proc/lockdep_stats

此命令在適度的系統上產生以下輸出

lock-classes:                          748 [max: 8191]

如果分配的數量（以上為 748）隨著時間的推移不斷增加，則可能存在洩漏。 以下命令可用於識別洩漏的鎖類

grep "BD" /proc/lockdep

執行該命令並儲存輸出，然後與稍後執行此命令的輸出進行比較，以識別洩漏者。 同樣的輸出也可以幫助您找到省略執行時鎖初始化的情況。

遞迴讀取鎖：

本文件的其餘部分試圖證明某種型別的迴圈等同於死鎖的可能性。

有三種類型的鎖：寫者（即獨佔鎖，如 spin_lock() 或 write_lock()）、非遞迴讀者（即共享鎖，如 down_read()）和遞迴讀者（遞迴共享鎖，如 rcu_read_lock()）。 並且我們在文件的其餘部分中使用這些鎖的以下表示法

W 或 E：代表寫者（獨佔鎖）。 r：代表非遞迴讀者。 R：代表遞迴讀者。 S：代表所有讀者（非遞迴 + 遞迴），因為兩者都是共享鎖。 N：代表寫者和非遞迴讀者，因為兩者都不是遞迴的。

顯然，N 是“r 或 W”，S 是“r 或 R”。

遞迴讀者，顧名思義，是即使在同一鎖例項的另一個讀者的臨界區內也允許獲取的鎖，換句話說，允許一個鎖例項的巢狀讀端臨界區。

而如果嘗試在同一鎖例項的另一個讀者的臨界區內獲取，非遞迴讀者將導致自身死鎖。

遞迴讀者和非遞迴讀者之間的區別是因為：遞迴讀者僅被寫鎖持有者阻塞，而非遞迴讀者可能被寫鎖等待者阻塞。 考慮以下示例

TASK A:                 TASK B:

read_lock(X);
                        write_lock(X);
read_lock_2(X);

任務 A 首先透過 read_lock() 獲取 X 上的讀者（無論遞迴還是非遞迴）。 並且當任務 B 嘗試獲取 X 上的寫者時，它將阻塞併成為 X 上寫者的等待者。 現在，如果 read_lock_2() 是遞迴讀者，任務 A 將取得進展，因為寫者等待者不會阻塞遞迴讀者，並且沒有死鎖。 但是，如果 read_lock_2() 是非遞迴讀者，它將被寫者等待者 B 阻塞，並導致自身死鎖。

同一鎖例項的讀者/寫者的阻塞條件：

只有四個阻塞條件

1. 寫者阻塞其他寫者。

2. 讀者阻塞寫者。

3. 寫者阻塞遞迴讀者和非遞迴讀者。

4. 並且讀者（無論是否遞迴）不阻塞其他遞迴讀者，但可能會阻塞非遞迴讀者（由於可能共存的寫者等待者）

阻塞條件矩陣，Y 表示行阻塞列，N 表示否則。

	W	r	R
W	Y	Y	Y
r	Y	Y	N
R	Y	Y	N

(W：寫者，r：非遞迴讀者，R：遞迴讀者)

遞迴獲取。 與非遞迴讀取鎖不同，遞迴讀取鎖僅被當前的寫鎖持有者（而不是寫鎖等待者）阻塞，例如

TASK A:                 TASK B:

read_lock(X);

                        write_lock(X);

read_lock(X);

對於遞迴讀取鎖不是死鎖，因為當任務 B 正在等待鎖 X 時，第二次 read_lock() 不需要等待，因為它是一個遞迴讀取鎖。 但是，如果 read_lock() 是非遞迴讀取鎖，則上述情況是死鎖，因為即使 TASK B 中的 write_lock() 無法獲得鎖，但它可以阻塞 TASK A 中的第二次 read_lock()。

請注意，鎖可以是寫鎖（獨佔鎖）、非遞迴讀取鎖（非遞迴共享鎖）或遞迴讀取鎖（遞迴共享鎖），具體取決於用於獲取它的鎖操作（更具體地說，是 lock_acquire() 的“read”引數的值）。 換句話說，單個鎖例項根據獲取函式有三種類型的獲取：獨佔、非遞迴讀取和遞迴讀取。

為了簡潔起見，我們將寫鎖和非遞迴讀取鎖稱為“非遞迴”鎖，並將遞迴讀取鎖稱為“遞迴”鎖。

遞迴鎖不互相阻塞，而非遞迴鎖會互相阻塞（這甚至對於兩個非遞迴讀取鎖也是如此）。 非遞迴鎖可以阻塞相應的遞迴鎖，反之亦然。

涉及遞迴鎖的死鎖情況如下

TASK A:                 TASK B:

read_lock(X);
                        read_lock(Y);
write_lock(Y);
                        write_lock(X);

任務 A 正在等待任務 B 的 read_unlock() Y，而任務 B 正在等待任務 A 的 read_unlock() X。

依賴型別和強依賴路徑：

鎖依賴關係記錄了一對鎖的獲取順序，並且因為鎖有 3 種類型，理論上鎖依賴關係有 9 種類型，但我們可以證明 4 種類型的鎖依賴關係足以進行死鎖檢測。

對於每個鎖依賴關係

L1 -> L2

，這意味著 lockdep 在執行時看到在同一個上下文中 L1 被持有，之後 L2 被持有。 在死鎖檢測中，我們關心是否會在持有 L1 的情況下阻塞 L2，IOW，是否存在一個鎖 L3，L1 阻塞 L3 並且 L2 被 L3 阻塞。 因此，我們只關心 1) L1 阻塞什麼，2) 什麼阻塞 L2。 因此，我們可以合併 L1 的遞迴讀者和非遞迴讀者（因為它們阻塞相同的型別），並且我們可以合併 L2 的寫者和非遞迴讀者（因為它們被相同的型別阻塞）。

透過以上組合進行簡化，lockdep 圖中有 4 種類型的依賴關係邊

1. -(ER)->

   獨佔寫者到遞迴讀者的依賴關係，“X -(ER)-> Y”表示 X -> Y，並且 X 是寫者，Y 是遞迴讀者。

2. -(EN)->

   獨佔寫者到非遞迴鎖的依賴關係，“X -(EN)-> Y”表示 X -> Y，並且 X 是寫者，Y 要麼是寫者，要麼是非遞迴讀者。

3. -(SR)->

   共享讀者到遞迴讀者的依賴關係，“X -(SR)-> Y”表示 X -> Y，並且 X 是讀者（無論遞迴與否），Y 是遞迴讀者。

4. -(SN)->

   共享讀者到非遞迴鎖的依賴關係，“X -(SN)-> Y”表示 X -> Y，並且 X 是讀者（無論遞迴與否），Y 要麼是寫者，要麼是非遞迴讀者。

請注意，給定兩個鎖，它們之間可能存在多個依賴關係，例如

TASK A:

read_lock(X);
write_lock(Y);
...

TASK B:

write_lock(X);
write_lock(Y);

，我們在依賴關係圖中同時具有 X -(SN)-> Y 和 X -(EN)-> Y。

我們使用 -(xN)-> 來表示 -(EN)-> 或 -(SN)-> 的邊，與 -(Ex)->、-(xR)-> 和 -(Sx)-> 類似

“路徑”是圖中一系列的合取依賴關係邊。 並且我們定義一個“強”路徑，它指示路徑中每個依賴關係的強依賴關係，作為沒有兩個合取邊（依賴關係）作為 -(xR)-> 和 -(Sx)-> 的路徑。 換句話說，“強”路徑是從一個鎖透過鎖依賴關係走到另一個鎖的路徑，如果 X -> Y -> Z 在路徑中（其中 X、Y、Z 是鎖），並且從 X 到 Y 的路徑是透過 -(SR)-> 或 -(ER)-> 依賴關係，從 Y 到 Z 的路徑不能透過 -(SN)-> 或 -(SR)-> 依賴關係。

我們將在下一節中看到為什麼該路徑被稱為“強”。

遞迴讀死鎖檢測：

我們現在證明兩件事

引理 1

如果存在閉合的強路徑（即強迴圈），則存在導致死鎖的鎖定序列組合。 也就是說，強迴圈足以進行死鎖檢測。

引理 2

如果不存在閉合的強路徑（即強迴圈），則不存在可能導致死鎖的鎖定序列組合。 也就是說，強迴圈對於死鎖檢測是必要的。

有了這兩個引理，我們可以很容易地說閉合的強路徑對於死鎖既是充分的又是必要的，因此閉合的強路徑等同於死鎖的可能性。 由於閉合的強路徑代表可能導致死鎖的依賴鏈，因此我們稱其為“強”，考慮到存在不會導致死鎖的依賴迴圈。

充分性的證明（引理 1）

假設我們有一個強迴圈

L1 -> L2 ... -> Ln -> L1

，這意味著我們有依賴關係

L1 -> L2
L2 -> L3
...
Ln-1 -> Ln
Ln -> L1

我們現在可以構建導致死鎖的鎖定序列組合

首先，讓一個 CPU/任務在 L1 -> L2 中獲取 L1，然後讓另一個 CPU/任務在 L2 -> L3 中獲取 L2，依此類推。 在此之後，Lx -> Lx+1 中的所有 Lx 都由不同的 CPU/任務持有。

然後，因為我們有 L1 -> L2，所以 L1 的持有者將在 L1 -> L2 中獲取 L2，但是由於 L2 已經被另一個 CPU/任務持有，加上 L1 -> L2 和 L2 -> L3 不是 -(xR)-> 和 -(Sx)->（強的定義），這意味著 L1 -> L2 中的 L2 要麼是非遞迴鎖（被任何人阻塞），要麼 L2 -> L3 中的 L2 是寫者（阻塞任何人），因此 L1 的持有者無法獲得 L2，它必須等待 L2 的持有者釋放。

此外，我們可以對 L2 的持有者得出類似的結論：它必須等待 L3 的持有者釋放，依此類推。 我們現在可以證明 Lx 的持有者必須等待 Lx+1 的持有者釋放，並請注意 Ln+1 是 L1，所以我們有一個迴圈等待場景，沒有人能夠取得進展，因此發生死鎖。

必要性的證明（引理 2）

引理 2 等同於：如果存在死鎖場景，則依賴關係圖中必須存在強迴圈。

根據 Wikipedia[1]，如果存在死鎖，則必須存在迴圈等待場景，這意味著存在 N 個 CPU/任務，其中 CPU/任務 P1 正在等待 P2 持有的鎖，P2 正在等待 P3 持有的鎖，... 並且 Pn 正在等待 P1 持有的鎖。 讓我們將 Px 正在等待的鎖命名為 Lx，因此由於 P1 正在等待 L1 並且持有 Ln，因此我們將在依賴關係圖中具有 Ln -> L1。 類似地，我們在依賴關係圖中具有 L1 -> L2、L2 -> L3、...、Ln-1 -> Ln，這意味著我們有一個迴圈

Ln -> L1 -> L2 -> ... -> Ln

，現在讓我們證明該迴圈是強的

對於鎖 Lx，Px 會產生依賴關係 Lx-1 -> Lx，而 Px+1 會產生依賴關係 Lx -> Lx+1。由於 Px 正在等待 Px+1 釋放 Lx，所以 Lx 在 Px+1 上不可能是讀鎖，而 Lx 在 Px 上是遞迴讀鎖，這是不可能的。因為讀鎖（無論是否遞迴）不會阻塞遞迴讀鎖，因此 Lx-1 -> Lx 和 Lx -> Lx+1 不可能是一個 -(xR)-> -(Sx)-> 對。這對於環中的任何鎖都成立，因此，這個環是強環。

參考文獻：

[1]: https://en.wikipedia.org/wiki/Deadlock [2]: Shibu, K. (2009). Intro To Embedded Systems (1st ed.). Tata McGraw-Hill