プログラム情報の管理

ロック lint は、C コンパイラによって作成される一連のデータベースによって、解析対象となるソースについての情報を獲得します。各ソースファイルのロック lint データベースは、独立したファイルに保存されます。一連のソースファイルを分析するには、load サブコマンドを使用してそれらに関連するデータベースファイルを読み込みます。files サブコマンドは、読み込まれたデータベースファイルによって表されるソースファイルのリストの表示に使用できます。いったんファイルが読み込まれると、ロック lint は、すべての関数、グローバルデータ、関連ソースファイルにおいて参照される外部関数についての情報を得るようになります。

関数管理

解析フェーズの一部として、ロック lint は、読み込まれたすべてのソースに対してコールグラフを作成します。定義された関数についての情報は、funcs サブコマンドを介して利用可能となります。ロック lint が解析対象であるコードに対する正確なコールグラフを持つということは、意味のある解析を行う上でとても重要です。

読み込まれたファイルから呼び出されることのない関数はすべてルート関数と呼ばれます。読み込まれたモジュール内で呼び出される関数であっても (たとえば、関数がライブラリのエントリポイントであり、ライブラリ内でも呼び出される場合など)、ルート関数として扱いたいこともあります。そのためには、declare root サブコマンドを使用してください。また、ignore サブコマンドを実行することによって、コールグラフから関数を削除することも可能です。

ロック lint は、関数ポインタに対するすべての参照およびそれらに対して行なわれる関数の割り当て状況について知っています。現在読み込まれているファイルの関数ポインタについての情報は、funcptrs サブコマンドを介して利用できます。関数ポインタを経由して行われる呼び出しについての情報は、pointer calls サブコマンドを介して利用できます。もしも、ロック lint が発見できないような関数ポインタの割り当てが存在する場合、それらは declare ... targets サブコマンドによって指定されている可能性があります。

デフォルトでは、ロック lint は可能性のあるすべての実行パスの検証を行おうとします。そして、コードが関数ポインタを使用している場合、コードの通常の動作においては、実行パスの多くが実際にはたどられない可能性があります。これにより、実際には起こらないデッドロックが報告されてしまうことがあります。こうした事態を防ぐには、disallow および reallow サブコマンドを使用して、決して使用されることのない実行パスをロック lint に知らせてください。また、reallows および disallows サブコマンドを使用することによって、現時点での制限事項を出力できます。

変数管理

ロック lint データベースにも、ソースコード内でアクセスされるすべてのグローバル変数についての情報が含まれます。これらの変数についての情報は、vars サブコマンドを介して利用できます。

ロック lint のジョブの 1 つは、変数のアクセスが整合性を保って保護されているかどうかを確認することです。特定の変数についてそのアクセスが問題にならない場合は、ignore サブコマンドによって、検証の対象から除外できます。

また、次に示すソースコードへの注釈の挿入のどれか1つを利用することも可能です。

SCHEME_PROTECTS_DATA

READ_ONLY_DATA

DATA_READABLE_WITHOUT_LOCK

NOW_INVISIBLE_TO_OTHER_THREADS

NOW_VISIBLE_TO_OTHER_THREADS

詳細は、 「ソースコードへの注釈の挿入」を参照してください。

ロック管理

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

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

MUTEX_PROTECTS_DATA

RWLOCK_PROTECTS_DATA

SCHEME_PROTECTS_DATA

DATA_READABLE_WITHOUT_LOCK

RWLOCK_COVERS_LOCK

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

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

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

MUTEX_ACQUIRED_AS_SIDE_EFFECT

READ_LOCK_ACQUIRED_AS_SIDE_EFFECT

WRITE_LOCK_ACQUIRED_AS_SIDE_EFFECT

LOCK_RELEASED_AS_SIDE_EFFECT

LOCK_UPGRADED_AS_SIDE_EFFECT

LOCK_DOWNGRADED_AS_SIDE_EFFECT

NO_COMPETING_THREADS_AS_SIDE_EFFECT

COMPETING_THREADS_AS_SIDE_EFFECT

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