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