ロック管理

ソースコードへの注釈の挿入を利用することで、コード中のロックに関するアサーションを効率的に調整できます。アサーションには、保護、順序、副作用の 3 種類があります。

保護アサーションは、特定のロックによって何が保護されているかを説明します。以下に示すソースコードへの挿入を使用してください。

assert サブコマンドのバリエーションは、特定のロックがデータまたは関数の一部分を保護していることをアサートするために使用されます。さらに別のバリエーションである assert ... covers は、特定のロックがほかのロックを保護していることをアサートします (これは階層的ロッキングスキームに使用されます)。

順序アサーションは、特定のロックが取得されるべき順序を指定します。ソースコードへの注釈の挿入 LOCK_ORDER または assert order サブコマンドによって、ロックの順序を指定できます。

副作用アサーションは、ある関数が特定のロックの解放または取得の副作用を持つことをアサートします。 以下に示すソースコードへの注釈の挿入を使用してください。

assert side effect サブコマンドによって副作用を指定することも可能です。ときには、外部関数についての副作用アサーションを作成したいこともあり、その場合、ロックは読み込まれたモジュールから可視ではありません (たとえば、外部関数のモジュールに対して静的である場合など)。このようなケースでは、declare サブコマンドの形式を使用することで、ロックを“作成”できます。