註釋鎖定行為
若要避免在多執行緒程式的並行 Bug，請遵循適當的鎖定規則並使用 SAL 附註。
因為它們不是決定性的，因此並行 Bug 臭名遠通話地難以重現，診斷和偵錯。 對齊有關執行緒交錯很難最佳的情況是，而變得不實際，當您設計的一些執行緒有更多的程式碼主體。 因此，最好遵循在多執行緒應用程式的鎖定規則。 例如，必須遵守鎖定排序，當取得協助避免死結的多個鎖定時，，並擷取適當 Guarded 鎖定存取共用資源說明前請避免競爭情形。
可惜的是，介面上簡單鎖定規則很驚訝地困難實際上後面。 在今天的程式設計語言和編譯器的基本限制並不直接支援並行要求規格和分析。 程式設計人員必須依賴非正式的程式碼註解表示其相對於其如何檢視使用鎖定。
並行 SAL 附註可以幫助您指定鎖定副作用、鎖定責任、資料、保護，鎖定命令階層架構和其他必要的鎖定的行為。 可以隱含規則明確， SAL 並行附註提供一致的方式來記錄您的程式碼如何使用鎖定規則。 並行附註可以提高程式碼分析工具的能力會出現競爭情形和死結、不相符的同步處理作業和其他小並行存取錯誤。
一般方針
使用標記法，您可以陳述式由實作的合約 (被呼叫端) 和用戶端 (呼叫端) 之間的函式定義提示，並表示不可變和可以進一步改善分析程式的其他屬性。
SAL 支援各種不同的鎖定基本型別 (例如、關鍵區段、Mutex、微調鎖定和其他資源。 許多並行附註採用鎖定運算式做為參數。 依照慣例，鎖定已由基礎鎖定物件的路徑運算式表示。
某些執行緒擁有權規則記住:
微調鎖定是會清除執行緒擁有權的未磁碟上的鎖定。
Mutex 和關鍵區段是會清除執行緒擁有權的計數的鎖定。
號誌和事件是未清除執行緒擁有權的計數的鎖定。
鎖定附註
下表列出鎖定的附註。
註釋 |
描述 |
|---|---|
_Acquires_exclusive_lock_(expr) |
附註的函式並指出在張貼狀態函式會將由 expr命名的鎖定物件的獨佔鎖定計數。 |
_Acquires_lock_(expr) |
附註的函式並指出在張貼狀態函式會將由 expr命名的鎖定物件的鎖定計數。 |
_Acquires_nonreentrant_lock_(expr) |
由 expr 命名的取得鎖定。 錯誤報告鎖定已保留。 |
_Acquires_shared_lock_(expr) |
附註的函式並指出在張貼狀態函式會將由 expr命名的鎖定物件的共用鎖定計數。 |
_Create_lock_level_(name) |
宣告符號 name 是鎖定層級的陳述式，以便能用來附註 _Has_Lock_level_ 和 _Lock_level_order_。 |
_Has_lock_kind_(kind) |
附註任何物件去修改資源物件的型別資訊。 有時，一個常用的型別針對不同類型的資源和並不足以分辨各種資源中的語意要求的多載的型別而使用。 這個預先定義的 kind 參數清單:
|
_Has_lock_level_(name) |
附註的鎖定物件並將其鎖定的 name。 |
_Lock_level_order_(name1, name2) |
一個陳述式給定 name1 name2和之間的鎖定的順序。 |
_Post_same_lock_(expr1, expr2) |
附註的函式並指出在張貼的兩種方式鎖定， expr1 和 expr2，，視為已相同鎖定物件。 |
_Releases_exclusive_lock_(expr) |
附註的函式並指出在張貼狀態函式減一。是由 expr命名的鎖定物件的獨佔鎖定計數。 |
_Releases_lock_(expr) |
附註的函式並指出在張貼狀態函式減一。是由 expr命名的鎖定物件的鎖定計數。 |
_Releases_nonreentrant_lock_(expr) |
由 expr 命名的釋放的鎖定。 錯誤報告鎖定不目前持有。 |
_Releases_shared_lock_(expr) |
附註的函式並指出在張貼狀態函式減一。是由 expr命名的鎖定物件的共用鎖定計數。 |
_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_ |
附註函式參數為目標的其中一個運算元各種連鎖的函式。 這些運算元必須有特定額外屬性。 |
_Write_guarded_by_(expr) |
標註變數表示，只要修改變數，是由 expr 命名的鎖定物件的鎖定計數是至少一個。 |