ロック動作に注釈を付ける
は、マルチスレッド プログラムの同時実行のバグを回避するには、適切なロックの作業分野に常に従い、SAL コメントを使用します。
同時実行のバグは非確定的であるため、再生や診断やデバッグ悪名も困難です。スレッド インターリーブについての推論はいくつかのスレッドを超えているコードの本体をデザインする場合せいぜい困難で、現実的でなくなります。したがって、モデルによって、マルチスレッド プログラムのロックの作業分野に従うことをお勧めします。たとえば、ヘルプがデッドロックを避ける、適切なロックを守る共有リソースのヘルプにアクセスする前に、競合状態が取得されないように、ロックを取得している間、ロックに従って指示します。
ただし、表面上は単純なロックの規則は、実際に従って意外にも困難です。今日のプログラミング言語およびコンパイラの基本的な制限は、直接同時実行の条件の指定と分析がサポートされないことです。プログラマは、非公式コード コメントで表現するロックを使用する方法についてや目的をなっています。
同時実行の SAL コメントに責任、データの保護、ロックの順序の階層、と予想されるそのほかのロックする副作用のロックを指定できるように設計され動作をロックします。暗黙の規則を明示することにより、コードの規則をロックすることを使用する方法を説明する、SAL 同時実行のコメントは、一貫した方法を提供します。同時実行のコメントは、コード分析ツールの機能が競合状態、デッドロックが一致して、同期操作、およびそのほかの軽度の同時実行エラーを検索できます。
一般的なガイドライン
コメントを使用して、実装 (呼び出し先) とクライアント側 (呼び出し元) 間の関数定義によってコントラクトを示す意味することができ、さらに分析を向上プログラムの不変条件などのプロパティを表します。
SAL はさまざまな種類のロック例は、クリティカル セクション、ミューテックス、スピン ロックなどのリソース オブジェクトのプリミティブのロックをサポートします。多くの同時実行のコメントは、パラメーターとしてロックの式を設定します。規則により、ロックは、基になるオブジェクトのロックのパスの式によって表示されます。
ただし、に留意して、所有権の規則を遅らせます:
スピン ロックは、明示的なスレッドの所有権のある無数のロックです。
ミューテックスとクリティカル セクションは、明示的なスレッドの所有権を持つカウントが設定されたロックです。
セマフォおよびイベントは、明示的なスレッドの所有権がないカウントが設定されたロックです。
コメントのロック
次の表は、ロックのコメントを示します。
注釈 |
説明 |
|---|---|
_Acquires_exclusive_lock_(expr) |
関数を指定し、1 種類によってポストの状態で関数のインクリメント exprで、ロック オブジェクトの排他ロック カウント示します。 |
_Acquires_lock_(expr) |
関数を指定し、1 種類によってポストの状態で関数のインクリメント exprで、ロック オブジェクトのロック カウント示します。 |
_Acquires_nonreentrant_lock_(expr) |
expr によって示されるロックが取得されます。エラーは既に保持しているロックが報告されます。 |
_Acquires_shared_lock_(expr) |
関数を指定し、1 種類によってポストの状態で関数のインクリメント exprで、ロック オブジェクトの共有ロック カウント示します。 |
_Create_lock_level_(name) |
コメント _Has_Lock_level_ と _Lock_level_order_で使用するようにロックのレベルでシンボル name を宣言するステートメント。 |
_Has_lock_kind_(kind) |
オブジェクトをリソース オブジェクトの型情報を得るために指定します。、共通の型は異なる種類のリソースに使用され、オーバーロードされた型は、さまざまなリソースとの意味条件を区別するだけでは不十分です。kind の定義済みのパラメーターの一覧を次に示します。:
|
_Has_lock_level_(name) |
ロック オブジェクトを注釈し、nameのレベルをロックできます。 |
_Lock_level_order_(name1, name2) |
name1 と name2の間に命令するロックを提供するステートメント。 |
_Post_same_lock_(expr1, expr2) |
関数を注釈し、Post 状態で 2 種類のロック、expr1 示し、それらが同じロック オブジェクトとして expr2は、扱われます。 |
_Releases_exclusive_lock_(expr) |
関数を指定し、1 種類によってポストの状態で関数のデクリメント exprで、ロック オブジェクトの排他ロック カウント示します。 |
_Releases_lock_(expr) |
関数を指定し、1 種類によってポストの状態で関数のデクリメント exprで、ロック オブジェクトのロック カウント示します。 |
_Releases_nonreentrant_lock_(expr) |
expr で、ロックが解放されます。エラーは、ロックが現行である報告されます。 |
_Releases_shared_lock_(expr) |
関数を指定し、1 種類によってポストの状態で関数のデクリメント exprで、ロック オブジェクトの共有ロック カウント示します。 |
_Requires_lock_held_(expr) |
少なくとも 1 によってがある expr で示されたオブジェクトのロック カウント関数を注釈し、前に示すことを示します。 |
_Requires_lock_not_held_(expr) |
がゼロである expr で示されたオブジェクトのロック カウント関数を注釈し、前に示すことを示します。 |
_Requires_no_locks_held_ |
関数注釈を付けてチェッカーで認識されるすべてのロックのロック カウントがゼロであることを示します。 |
_Requires_shared_lock_held_(expr) |
少なくとも 1 によってがある expr で示されたオブジェクトの共有ロック カウント関数を注釈し、前に示すことを示します。 |
_Requires_exclusive_lock_held_(expr) |
少なくとも 1 によってがある expr で示されたオブジェクトの排他ロック カウント関数を注釈し、前に示すことを示します。 |
Unexposed ロック オブジェクトの SAL の組み込み
特定のロック オブジェクトは、関連付けられたロックの関数の実装によって公開されません。次の表は、非公開のロック オブジェクトを操作する関数のコメントを有効にする SAL 基本的な変数を示します。
注釈 |
説明 |
|---|---|
_Global_cancel_spin_lock_ |
キャンセルのスピン ロックについて説明します。 |
_Global_critical_region_ |
クリティカル領域について説明します。 |
_Global_interlock_ |
推奨操作をかみ合わせました。 |
_Global_priority_region_ |
優先順位の領域について説明します。 |
共有データはコメントにアクセス
次の表は、共有データ アクセスについてのコメントを示します。
注釈 |
説明 |
|---|---|
_Guarded_by_(expr) |
変数にアクセスするたびに変数を指定し、expr で、ロック オブジェクトのロック カウントは 1 以上であることを示します。 |
_Interlocked_ |
変数を指定し、_Guarded_by_(_Global_interlock_)と同じです。 |
_Interlocked_operand_ |
注釈先関数のパラメーターは、インタロックされた関数の 1 種類のターゲットのオペランドです。これらのオペランドは固有の追加のプロパティが必要です。 |
_Write_guarded_by_(expr) |
変数が変更されるたびに、変数、注釈を付けて、expr で、ロック オブジェクトのロック カウントは 1 以上であることを示します。 |