註釋鎖定行為

為了避免多執行緒程式中發生並行 Bug,請務必遵循適當的鎖定規範並使用 SAL 註釋。

並行錯誤非常難以重現、診斷和偵錯,因為它們不具決定性。 關於執行緒交錯的推理充其量是困難的,而且當您設計的程式碼主體時,其程式碼主體超過一些執行緒時變得不切實際。 因此,較好的做法是遵循多執行緒程式中的鎖定規範。 例如,當擷取多個鎖定時遵循鎖定順序有助於避免發生死結,而在存取共用資源之前取得適當防護的鎖定有助於避免產生競爭條件。

可惜的是,看似簡單的鎖定規則在實務上可能非常不容易遵循。 現今程式設計語言和編譯器的基本限制是,它們不會直接支援並行需求的規格和分析。 程式設計人員必須依賴非正式的程式碼註解來表達其使用鎖定的目的。

並行 SAL 註釋的設計在於幫助您指定鎖定的副作用、鎖定責任、資料保護、鎖定順序階層,以及其他必要的鎖定行為。 SAL 並行註釋藉由讓隱含規則變為明確,提供了一致的方式讓您記錄程式碼使用鎖定規則的方式。 並行註釋還可以增強程式碼分析工具的能力,找出競爭條件、死結、不相符的同步處理作業及其他細小的並行錯誤。

一般準則

藉由使用注釋,您可以陳述實作(被呼叫者)與用戶端(呼叫者)之間函式定義所隱含的合約。 您也可以表示程式的其他屬性,以進一步改善分析。

SAL 支援多種不同的鎖定基本類型,例如關鍵區段、Mutex、微調鎖定和其他資源物件。 許多並行批註會採用鎖定運算式作為參數。 依照慣例,鎖定是由基礎鎖定物件的路徑運算式表示。

請記住一些執行緒擁有權規則:

  • 微調鎖定是擁有清楚執行緒擁有權的不可計數鎖定。

  • Mutex 和關鍵區段是擁有清楚執行緒擁有權的計數鎖定。

  • 旗號和事件會計算出沒有清楚執行緒擁有權的鎖定。

鎖定批註

下表列出鎖定批註。

註釋 描述
_Acquires_exclusive_lock_(expr) 為函式加上附註,並指出在後製狀態下,函式會讓 expr 命名之鎖定物件的獨佔鎖定計數遞增 1。
_Acquires_lock_(expr) 標註函式,並指出在後製狀態下,函式會讓 expr 命名之鎖定物件的鎖定計數遞增 1。
_Acquires_nonreentrant_lock_(expr) 取得由 expr 命名的鎖定。 如果鎖定已保留,則會報告錯誤。
_Acquires_shared_lock_(expr) 為函式加上附註,並指出在後製狀態下,函式會讓 expr 命名之鎖定物件的共用鎖定計數遞增 1。
_Create_lock_level_(name) 將符號 name 宣告為鎖定層級的陳述式,如此該符號就可以在註釋 _Has_Lock_level__Lock_level_order_ 中使用。
_Has_lock_kind_(kind) 批註任何物件,以精簡資源物件的類型資訊。 有時候,一般類型會用於不同類型的資源,而多載類型不足以區分各種資源的語意需求。 以下是預先定義的 kind 參數清單:

_Lock_kind_mutex_
鎖定 Mutex 的種類識別碼。

_Lock_kind_event_
鎖定事件的種類識別碼。

_Lock_kind_semaphore_
鎖定號志的種類識別碼。

_Lock_kind_spin_lock_
微調鎖定的鎖定種類識別碼。

_Lock_kind_critical_section_
鎖定重要區段的種類識別碼。
_Has_lock_level_(name) 標註鎖定物件,並為其指定 name 的鎖定層級。
_Lock_level_order_(name1, name2) 語句,提供 和 name2 之間的 name1 鎖定順序。 在具有 name2 層級的鎖定之前,必須先取得具有層級 name1 的鎖定。
_Post_same_lock_(expr1, expr2) 標注函式,並指出在後置狀態中,兩個鎖定 expr1expr2 和 會被視為相同的鎖定物件。
_Releases_exclusive_lock_(expr) 標註函式,並指出在後製狀態下,函式會讓 expr 命名之鎖定物件的獨佔鎖定計數遞減 1。
_Releases_lock_(expr) 為函式加上附註,並指出在後製狀態下,函式會讓 expr 命名之鎖定物件的鎖定計數遞減 1。
_Releases_nonreentrant_lock_(expr) 會釋放由 expr 命名的鎖定。 如果目前未保留鎖定,就會報告錯誤。
_Releases_shared_lock_(expr) 為函式加上附註,並指出在後製狀態下,函式會讓 expr 命名之鎖定物件的共用鎖定計數遞減 1。
_Requires_lock_held_(expr) 為函式加上附註,並指出在前置狀態下,由 expr 命名之物件的鎖定計數至少為一。
_Requires_lock_not_held_(expr) 標註函式標註,並指出在前置狀態下,由 expr 命名之物件的鎖定計數為零。
_Requires_no_locks_held_ 為函式加上附註,並指出檢查程式已知之所有鎖定的鎖定計數為零。
_Requires_shared_lock_held_(expr) 為函式加上附註,並指出在前置狀態下,由 expr 命名之物件的共用鎖定計數至少為一。
_Requires_exclusive_lock_held_(expr) 標註函式,並指出在前置狀態下,由 expr 命名之物件的獨佔鎖定計數至少為一。

未公開之鎖定物件的 SAL 內在變數

相關鎖定函式的實作不會公開特定鎖定物件。 下表列出 SAL 內部變數,這些變數會啟用在未公開的鎖定物件上運作之函式的註釋。

註釋 描述
_Global_cancel_spin_lock_ 描述取消微調鎖定。
_Global_critical_region_ 描述關鍵區域。
_Global_interlock_ 描述連鎖作業。
_Global_priority_region_ 描述優先權區域。

共用資料存取注釋

下表列出共用資料存取的註釋。

註釋 描述
_Guarded_by_(expr) 標註變數,並指出只要存取變數,由 expr 命名之鎖定物件的鎖定計數就會至少為一。
_Interlocked_ 為變數標注 ,且 相當於 _Guarded_by_(_Global_interlock_)
_Interlocked_operand_ 批註函式參數是其中一個不同 Interlocked 函式的目標運算元。 這些運算元必須具有特定的其他屬性。
_Write_guarded_by_(expr) 為變數加上附註,並指出只要修改變數,由 expr 命名之鎖定物件的鎖定計數就會至少為一。

智慧鎖定和 RAII 注釋

智慧型鎖定通常會包裝原生鎖定並管理其存留期。 下表列出可搭配智慧鎖定和 RAII 編碼模式搭配語意支援的 move 批註。

註釋 描述
_Analysis_assume_smart_lock_acquired_(lock) 告知分析器假設已取得智慧鎖定。 此批註預期參考鎖定類型為其參數。
_Analysis_assume_smart_lock_released_(lock) 告知分析器假設已釋放智慧鎖定。 此批註預期參考鎖定類型為其參數。
_Moves_lock_(target, source) 描述作業 move constructor ,此作業會將鎖定狀態從 source 物件傳輸至 targettarget會被視為新建構的物件,因此它之前的任何狀態都會遺失,並由狀態取代 sourcesource也會重設為沒有鎖定計數或別名目標的清除狀態,但指向它的別名會維持不變。
_Replaces_lock_(target, source) 描述 move assignment operator 從來源傳輸狀態之前釋放目標鎖定的語意。 您可以將它視為 _Moves_lock_(target, source) 前面加上 _Releases_lock_(target) 的組合。
_Swaps_locks_(left, right) 描述標準 swap 行為,其假設物件 leftright 交換其狀態。 交換的狀態包括鎖定計數和別名目標,如果有的話。 指向 leftright 物件的別名會保持不變。
_Detaches_lock_(detached, lock) 描述鎖定包裝函式類型允許與其自主資源解除關聯的案例。 它類似于其內部指標的運作方式 std::unique_ptr :它可讓程式設計人員擷取指標,並將其智慧型指標容器保持乾淨狀態。 支援類似的邏輯 std::unique_lock ,而且可以在自訂鎖定包裝函式中實作。 卸離鎖定會保留其狀態(如果有的話,鎖定計數和別名目標),而包裝函式會重設為包含零鎖定計數,且沒有別名目標,同時保留自己的別名。 鎖定計數沒有作業(釋放和取得)。 此批註的行為完全一樣 _Moves_lock_ ,不同之處在于卸離的引數應該是 return ,而不是 this

另請參閱