このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。

Polyspace 解析によるメモリ使用量の削減と解析時間の短縮

問題

検証が特定のポイントから長時間進まなくなります。場合によっては、非アクティブな時間に対する内部しきい値を超えて検証が停止することや、次のエラー メッセージが表示されることもあります。

The analysis has been stopped by timeout.

数百のソース ファイルや数百万行のコードを使用する大規模なプロジェクトの場合、同じ問題が別の形で発生することがあります。検証が停止して、次のエラー メッセージが表示されます。

Fatal error: Not enough memory

4 プロセッサを超えるマルチコア システムの場合は、オプション-max-processesを使用してプロセッサの数を増やしてみます。既定の検証では、最大 4 プロセッサが使用されます。4 プロセッサ未満の場合、検証では利用可能な最大数が使用されます。解析用に、プロセッサごとに少なくとも 4 GB の RAM がなければなりません。たとえば、マシンに 16 GB の RAM がある場合、このオプションで 4 つを超えるプロセッサを指定しないようにします。検証のログ ファイル内に、Polyspace® によって、検証のさまざまなステージごとの最大メモリ使用量の推定値が生成されます。たとえば、このログ ファイルには次のようなメッセージが表示されます。

Maximum Memory Usage: 573 MB
これらの推定値を参考に、メモリを増やすことで検証を高速化できるかどうかを評価できます。

それでも検証に時間がかかる場合は、速度を向上して検証を迅速に行うために、以下の解決法のいずれかを試します。

考えられる原因: ネットワーク ドライブ上の一時フォルダー

Polyspace は、解析中にいくつか一時ファイルを生成します。これらのファイルの保存に使用するフォルダーがネットワーク ドライブ上にある場合、解析の速度が低下する可能性があります。

解決法: 一時フォルダーを変更する

一時フォルダーをローカル ドライブ上のパスに変更します。

Polyspace が一時フォルダーの場所を特定する方法については、Polyspace 解析中の一時ファイルの保存を参照してください。

考えられる原因: ウイルス対策ソフトウェア

場合によっては、ウイルス対策ソフトウェアのチェックによって、Polyspace 解析の速度が顕著に低下することがあります。この低下は、Polyspace 解析で生成される一時ファイルがチェックされるために発生します。

Polyspace プロセスの例外の設定

実行中のプロセスをチェックして、ウイルス対策のために大量のメモリが消費されていないかを確認します。

ディスク最適化およびウイルス対策ソフトウェアによる Polyspace 実行のエラーまたは実行速度の低下の修正を参照してください。

考えられる原因: アプリケーションが大きく複雑である

検証時間はコードのサイズと複雑度によって変わります。

コードの行数が 100,000 行を超えるようなアプリケーションでは、検証時間が長くなる場合があります。小さなアプリでも、構造が複雑な場合は検証に時間がかかることがあります。たとえば、多くのレベルの入れ子を含む場合や、ポインターによる複数のレベルのエイリアシングを含む場合などが該当します。結果フォルダーにある解析ログの最初の方で、コメントを除く行数を確認できます。次の文字列を検索します。 

Number of lines without comments

ただし、既定のオプションを使用した検証で不当に時間がかかったり完全に停止したりする場合は、検証時間を短縮する手法がいくつかあります。いずれの手法でも、検証の複雑度を何らかの方法で下げることが必要になります。

解決法: 最初に PolyspaceBug Finder を使用する

最初に Polyspace Bug Finder™ を使用して、コードの欠陥を見つけます。Polyspace Bug Finder で検出される一部の欠陥は、Polyspace Code Prover™ におけるレッド エラーと解釈できる場合があります。それらの欠陥を修正したら、Polyspace Code Prover を使用して、より厳密な検証を行います。

解決法: アプリケーションをモジュール化する

アプリケーションを複数のモジュールに分割できます。各モジュールを他のモジュールとは別個に検証します。他のモジュールの検証を継続しながら、1 つのモジュールの完全な結果をレビューできます。

完全なアプリケーションをモジュールに分割すると、モジュール単位では一部の情報が欠落することになります。たとえば、あるモジュールに別のモジュールで定義されている関数の呼び出しが含まれることがあります。ソフトウェアでは未定義の関数について特定の仮定を行います。仮定が関数の実際の表現よりも幅広い場合、過大近似によりオレンジ チェックが増加します。たとえば、エラー管理関数が int の値 0 または 1 を返すとします。しかし、Polyspace で関数定義が見つからないと、この関数が変数 int に対して許容されるすべての値を返す可能性があると仮定されます。このような仮定は、外部制約を指定して絞り込むことができます。

アプリケーションを手動でモジュール化するときは、独自のモジュール化方法を使用できます。たとえば、1 つのモジュールに確認が必要な重要なファイルだけをコピーして検証できます。残りのファイルについては外部制約で表すことができます。ただし、それらの制約で欠落しているコードを忠実に表すことが必要になります。たとえば、未定義の関数に対する制約で関数の戻り値を表し、他の関連する二次的影響も再現していれば、その制約は関数を忠実に表していることになります。外部制約を指定するには、オプション [制約の設定] (-data-range-specifications) を使用します。

解決法: 低い精度レベルまたは検証レベルを選択する

検証に時間がかかりすぎる場合は、より低い精度レベルや、より低い検証レベルを使用します。そうしたレベルでレッド エラーを修正し、検証を再実行します。

  • 精度レベルでは、検証に使用するアルゴリズムが決定されます。精度を高めると証明済み結果の数は増えますが、必要な検証時間も増加します。詳細は、精度レベル (-O0 | -O1 | -O2 | -O3)を参照してください。

  • 検証レベルでは、Polyspace のソース コードでの実行回数が決定されます。詳細は、検証レベル (-to)を参照してください。

精度を下げると、検証結果に含まれるオレンジ チェックが増える可能性があります。オレンジ チェックは、解析で処理に疑わしい点があると見なされたものの、ランタイム エラーが存在するか否かを証明できないことを表します。処理を継続できるかどうかを確認するために、オレンジ チェックについては十分なレビューが必要です。オレンジ チェックの数が増えれば、検証結果のレビューにかかる時間は事実上長くなります。したがって、以下の手法を使用するのは、検証時間が極端に長い場合だけにしてください。

解決法: コードの複雑度を低減する

コードを読みやすくし、検証時間も短縮するために、コードの複雑度を低減できます。Polyspace では、アプリケーションからコード複雑度メトリクスが計算され、それらのメトリクスが事前定義値よりも低くなるように制限できます。

詳細は、次を参照してください。

解決法: グローバル変数の共有と使用のみを計算

アプリケーションに対して、グローバル変数の共有と使用のみを計算するような、簡易 Code Prover 解析を実行します。その後、実行時エラーを検出するための、コンポーネント単位での完全な解析を実行できます。グローバル変数の共有と使用のみを表示 (-shared-variables-mode) を参照してください。

解決法: 近似を有効にする

状況に応じて、特定の近似を有効にするようにスケーリング オプションを選択できます。多くの場合、それらのオプションを使用して検証を軽減しなければならないことを示す警告メッセージが表示されます。

状態オプション
コードにさまざまなレベルの深さの構造体が含まれている。構造体内の検証の深さ (-k-limiting)
検証ログに特定の関数をインライン化する提案が含まれている。インライン (-inline)

解決法: コードの部分を削除する

サードパーティ ライブラリのコードの削除を試みることができます。ソフトウェアでは、Polyspace 解析用に指定されていて、ファイル内で定義されていない関数にスタブを使用します。

解析時間は短くなりますが、スタブ関数に関する Polyspace による仮定が原因で、オレンジ チェックが多く表示される可能性があります。スタブ関数に関する Code Prover の仮定を参照してください。

考えられる原因: マルチタスク アプリケーションのエントリ ポイントが多すぎる

コードがマルチタスキングを対象としており、多くのタスクを指定している場合、検証に時間がかかることがあります。次の警告が表示される可能性があります。

Warning: Polyspace detected that the application has x tasks and y critical sections.
         The precision of the analysis will be reduced to avoid scaling issues.
         Check if you can reduce the number of tasks and critical sections in the configuration.
この警告が表示された場合は、検証を妥当な時間で完了できるように、Polyspace で精度の低い解析モードに切り替えられることを意味します。この精度の低いモードでは、検証時に一部の共有変数が全範囲と見なされ、過大近似によりオレンジ チェックの原因となる場合があります。

解決法

指定するエントリ ポイントの数を減らすことができるかどうかを確認します。一部のエントリ ポイント関数が同時に実行されないことがわかっている場合、それらを個別のエントリ ポイントとして指定する必要はありません。それらの関数をラッパー関数で順番に呼び出し、そのラッパー関数をエントリ ポイントとして指定できます。

たとえば、エントリ ポイント関数 task1、task2、task3 が同時に実行されないことがわかっているとします。

  1. task1、task2、task3 を可能性があるすべての順序で呼び出すラッパー関数 task を定義します。

    void task() {
   volatile int random = 0;
   if (random) {
       task1();
       task2();
       task3();
  } else if (random) {
       task1();
       task3();
       task2();
  } else if (random) {
       task2();
       task1();
       task3();
  } else if (random) {
       task2();
       task3();
       task1();
  } else if (random) {
       task3();
       task1();
       task2();
  } else {
       task3();
       task2();
       task1();
  } 
}

  2. task1、task2、task3 の代わりに、task をオプションタスク (-entry-points)に指定します。

ラッパー関数をエントリ ポイントとして使用する例については、Polyspace マルチタスキング解析の手動設定を参照してください。

参考

トピック

外部の Web サイト