ロック動作に注釈を付ける

  • [アーティクル]

マルチスレッド プログラムでのコンカレンシー バグを回避するには、常に適切なロックの規範に従い、SAL 注釈を使用します。

コンカレンシーのバグは非決定的であるため、再現、診断、デバッグが難しいことで知られています。 スレッドインターリーブに関する推論は、せいぜい難しく、数スレッドを超えるコード本体を設計する場合は実用的ではありません。 したがって、マルチスレッド プログラムのロックの規範に従うことをお勧めします。 たとえば、複数のロックを取得する場合に順序に従うと、デッドロックを回避でき、共有リソースにアクセスする前に適切な保護ロックを取得すると、競合状態を防ぐことができます。

残念ながら、一見単純なロック規則は実際には従うのがかなり難しい場合があります。 現在のプログラミング言語とコンパイラの基本的な制限は、コンカレンシー要件の仕様と分析を直接サポートしていないことです。 プログラマーは、ロックの使用方法に関する意図を表現するために、非公式のコード コメントに依存する必要があります。

コンカレンシー SAL 注釈は、ロックの副作用、ロックの責任、データの保護、ロック順序の階層、およびその他の想定されるロック動作の指定に役立つするように設計されています。 暗黙の規則を明示的にすると、SAL のコンカレンシー注釈によって、コードでロック規則を使用する方法を一貫した方法で記述できます。 コンカレンシー注釈を使用すると、競合状態、デッドロック、同期操作の不一致、およびその他の微妙なコンカレンシー エラーを検出するためのコード分析ツールの機能も強化されます。

一般的なガイドライン

注釈を使用すると、実装 (呼び出し元) とクライアント (呼び出し元) の間の関数定義によって暗黙的に指定されるコントラクトを指定できます。 また、プログラムのインバリアントやその他のプロパティを表現して、分析をさらに向上させることもできます。

SAL は、重要なセクション、ミューテックス、スピン ロック、およびその他のリソース オブジェクトなど、さまざまな種類のロック プリミティブをサポートしています。 多くのコンカレンシー注釈は、パラメーターとしてロック式を受け取ります。 表記規則では、ロックは、基になるロック オブジェクトのパス式によって示されます。

次のスレッド所有権の一部の規則にご注意ください。

  • スピン ロックは、明確なスレッド所有権を持つロックをカウントしません。

  • Mutex およびクリティカル セクションは、スレッドの所有権が明確になるようにカウントされたロックです。

  • セマフォとイベントは、明確なスレッド所有権を持たないカウントされたロックです。

ロックの注釈

次の表に、ロック注釈の一覧を示します。

注釈 説明
_Acquires_exclusive_lock_(expr) 関数に注釈を付け、post 状態のときに、関数が expr によって指定されたロック オブジェクトの排他ロック カウントを 1 インクリメントすることを示します。
_Acquires_lock_(expr) 関数に注釈を付け、post 状態のときに、関数が expr によって指定されたロック オブジェクトのロック カウントを 1 インクリメントすることを示します。
_Acquires_nonreentrant_lock_(expr) expr によって指定されたロックを取得します。 ロックが既に保持されている場合は、エラーが報告されます。
_Acquires_shared_lock_(expr) 関数に注釈を付け、post 状態のときに、関数が expr によって指定されたロック オブジェクトの共有ロック カウントを 1 インクリメントすることを示します。
_Create_lock_level_(name) 注釈 _Has_Lock_level_ と _Lock_level_order_ で使用できるようにシンボル name をロック レベルとして宣言するステートメント。
_Has_lock_kind_(kind) リソース オブジェクトの型情報を絞り込むために、任意のオブジェクトに注釈を付けます。 異なる種類のリソースに共通の型が使用され、オーバーロードされた型がさまざまなリソース間でセマンティック要件を区別するのに十分でない場合があります。 事前定義済みの kind パラメーターの一覧を次に示します。

_Lock_kind_mutex_
Mutex のロックの種類 ID。

_Lock_kind_event_
イベントのロックの種類 ID。

_Lock_kind_semaphore_
セマフォのロックの種類 ID。

_Lock_kind_spin_lock_
スピン ロックのロックの種類の ID。

_Lock_kind_critical_section_
重要なセクションのロックの種類 ID。
_Has_lock_level_(name) ロック オブジェクトに注釈を付け、name のロック レベルを指定します。
_Lock_level_order_(name1, name2) name1 と name2 の間のロック順序を指定するステートメント。 レベル name1 のロックは、レベル name2 のロックの前に取得する必要があります。
_Post_same_lock_(expr1, expr2) 関数に注釈を付け、事後状態で 2 つのロックとexpr2、expr1同じロック オブジェクトであるかのように扱われることを示します。
_Releases_exclusive_lock_(expr) 関数に注釈を付け、post 状態のときに、関数が expr によって指定されたロック オブジェクトの排他ロック カウントを 1 デクリメントすることを示します。
_Releases_lock_(expr) 関数に注釈を付け、post 状態のときに、関数が expr によって指定されたロック オブジェクトのロック カウントを 1 デクリメントすることを示します。
_Releases_nonreentrant_lock_(expr) expr によって指定されたロックを解除します。 ロックが現在保持されていない場合、エラーが報告されます。
_Releases_shared_lock_(expr) 関数に注釈を付け、post 状態のときに、関数が expr によって指定されたロック オブジェクトの共有ロック カウントを 1 デクリメントすることを示します。
_Requires_lock_held_(expr) 関数に注釈を付け、pre 状態のときに、expr によって指定されたオブジェクトのロック カウントが 1 以上であることを示します。
_Requires_lock_not_held_(expr) 関数に注釈を付け、pre 状態のときに、expr によって指定されたオブジェクトのロック カウントが 0 であることを示します。
_Requires_no_locks_held_ 関数に注釈を付け、チェッカーが認識しているすべてのロックのロック数が 0 であることを示します。
_Requires_shared_lock_held_(expr) 関数に注釈を付け、pre 状態のときに、expr によって指定されたオブジェクトの共有ロック カウントが 1 以上であることを示します。
_Requires_exclusive_lock_held_(expr) 関数に注釈を付け、pre 状態のときに、expr によって指定されたオブジェクトの排他ロック カウントが 1 以上であることを示します。

非公開のロック オブジェクトに対する 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_ 注釈付き関数のパラメーターは、インタロックされたさまざまな関数のいずれかのターゲット オペランドです。 これらのオペランドには、特定の追加プロパティが必要です。
_Write_guarded_by_(expr) 変数に注釈を付け、変数が変更されるたびに、expr によって指定されたロック オブジェクトのロック カウントが 1 以上であることを示します。

スマート ロックと RAII 注釈

通常、スマート ロックはネイティブ ロックをラップし、その有効期間を管理します。 次の表に、move セマンティクスをサポートするスマート ロックと RAII コーディングパターンで使用できる注釈を挙げます。

注釈 説明
_Analysis_assume_smart_lock_acquired_(lock) スマート ロックが取得されたと見なすようにアナライザーに指示します。 この注釈では、パラメーターとして参照ロックの種類が想定されます。
_Analysis_assume_smart_lock_released_(lock) スマート ロックが解除されたと見なすようにアナライザーに指示します。 この注釈では、パラメーターとして参照ロックの種類が想定されます。
_Moves_lock_(target, source) オブジェクトからsourceロック状態をmove constructor転送する操作について説明しますtarget。 target は新しく構築されたオブジェクトと見なされるため、以前の状態はいかなるものであっても失われ、source 状態に置き換えられます。 また、source は、ロック カウントまたは別名ターゲットを使用せずにクリーン状態にリセットされますが、それを指すエイリアスは変更されません。
_Replaces_lock_(target, source) ソースから状態を転送する前にターゲット ロックが解放される move assignment operator セマンティクスについて記述します。 これは、先行_Releases_lock_(target)する _Moves_lock_(target, source) .
_Swaps_locks_(left, right) オブジェクトleftrightとその状態の交換を前提とする標準的swapな動作について説明します。 交換される状態には、ロック カウントとエイリアス ターゲット (存在する場合) が含まれます。 left および right オブジェクトを指すエイリアスは変更されません。
_Detaches_lock_(detached, lock) ロック ラッパーの種類により、含まれているリソースとの関連付けを解除できるシナリオを記述します。 内部ポインターの操作方法std::unique_ptrと似ています。これにより、プログラマはポインターを抽出し、スマート ポインター コンテナーをクリーン状態のままにすることができます。 同様のロジックは std::unique_lock でサポートされており、カスタム ロック ラッパーで実装できます。 デタッチされたロックは、その状態 (ロック カウントとエイリアス ターゲットが存在する場合) を保持しますが、ラッパーは、独自のエイリアスを保持しながら、ゼロ ロック カウントを含み、エイリアス ターゲットを含まないようにリセットされます。 ロック カウントに対する操作 (解除と取得) はありません。 この注釈は、_Moves_lock_ とまったく同じように動作しますが、デタッチされた引数が this ではなく return である必要がある点が異なります。

関連項目