Polyspace でのマルチタスキング プログラムの解析

Polyspace^® を使用して、複数のスレッド (タスク) を同時実行するプログラムを解析できます。

解析では、通常の実行時チェックに加えて、次のような同時実行に固有の問題を調査します。

• データ レース、デッドロック、連続または不足しているロックとロック解除 (Bug Finder)

• 保護されていない共有変数 (Code Prover)

解析の設定

スレッド作成用の pthread_create など、コードで特定のファミリのマルチタスキング プリミティブを使用する場合は、次のようになります。

• Bug Finder では、解析でそれらを検出せず、コードからマルチタスキング モデルを抽出します。

• Code Prover では、自動検出を明示的に有効にしなければなりません。Code Prover の同時実行の自動検出を有効にする (-enable-concurrency-detection) (Polyspace Code Prover) を参照してください。

Polyspace でのスレッド作成とクリティカル セクションの自動検出を参照してください。

あるいは、解析オプションでマルチタスキング モデルを定義します。Polyspace デスクトップ製品のユーザー インターフェイスでは、これらのオプションは [構成] ペインの [マルチタスキング] ノードにあります。ほとんどのオプションは Bug Finder と Code Prover とで共通しています。Code Prover のマルチタスキング解析は、保護されていない可能性のある共有変数をより網羅的に特定するため、より厳密なモデルに従います。Code Prover のマルチタスキング解析を正常に完了させるには、コードが特定の形式で記述されていなければなりません。たとえば、エントリ ポイントとして指定する関数は void(void) 関数でなければなりません。ただし、この形式でコードが記述されていない場合は、これらの制限を回避できます。詳細は、Polyspace マルチタスキング解析の手動設定を参照してください。

解析結果のレビュー

Bug Finder

Bug Finder 解析では、次を含むさまざまな同時実行の欠陥を検出できます。

• 異なるタスクの変数での操作が互いに干渉する場合のデータ レース。

• ロック関数とロック解除関数の誤った配置によるデッドロックまたはダブル ロック。

完全なリストについては、同時実行の欠陥を参照してください。ただし、解析では誤検出を回避するために特定の仮定を行うため、解析ですべてのデータ レースが検出されるとは限りません。最初に Bug Finder でデータ レースをチェックしてから、Code Prover でより網羅的なチェックを行うという方法をとることができます。

Code Prover

Code Prover 解析では、共有されるグローバル変数が同時アクセスから保護されているかどうかが網羅的にチェックされます。解析では、確実に保護されている変数が緑色で報告され、保護されていない可能性がある変数がオレンジ色で報告されます。グローバル変数 (Polyspace Code Prover)を参照してください。

[結果の詳細] ペインのメッセージを使用して、結果をレビューします。 (グラフ) アイコンを使用して、競合する操作の視覚的な表現を確認します。

Bug Finder と Code Prover の違い

次の表は、Polyspace Bug Finder™ と Polyspace Code Prover™ の間でのマルチタスキング解析の相違点をまとめたものです。

構成

	Bug Finder	Code Prover
同時実行ルーチンの自動検出	既定でサポートされます	オプション [Code Prover の同時実行の自動検出を有効にする] (-enable-concurrency-detection) (Polyspace Code Prover) でサポートされます
main 関数に対する制約	なし	main 関数は終了しなければなりません。無限ループやランタイム エラーが含まれていてはなりません。 main に意図的な無限ループが含まれている場合の回避方法については、Code Prover マルチタスキング解析へのコードの適応 (Polyspace Code Prover)を参照してください。
Atomic operations	ターゲットのサイズによっては、特定の操作はアトミック (割り込み不可) と見なされます。 すべての操作を非アトミックと見なすには、オプション -detect-atomic-data-race を使用します。マルチタスキング コードでのアトミック操作の定義も参照してください。	すべての操作は非アトミックと見なされます。

結果

	Bug Finder	Code Prover
共有変数に対する保護されていない同時アクセス (データ レース)	以下のいずれかの結果を使用して示されます。 データ レース 隣接するビット フィールドでのデータ レース 標準ライブラリ関数呼び出しでデータ レースが発生しました	結果 [保護されていない可能性のある変数] (Polyspace Code Prover) を使用して示されます。 Code Prover は、制御フローとデータ フローを追跡するときに、より網羅的に行われます。そのため、Code Prover は Bug Finder で検出されなかった可能性のあるデータ レースを検出することがあります。
データ レース以外の以下のような同時ルーチンの問題: デッドロック、ダブル ロック、ロック解除されていないなど。 不適切なスレッドの作成、結合、または破棄。 スレッドからのメモリ エスケープ	検出される	検出されない

参考

トピック

• Polyspace でのスレッド作成とクリティカル セクションの自動検出
• Polyspace マルチタスキング解析の手動設定
• マルチタスキング コードでの共有変数の保護