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

Polyspace マルチタスキング解析の手動設定

Polyspace® を使用して、複数のスレッドを同時実行するプログラムを解析できます。場合によっては、Polyspace で、コード内のスレッド作成とクリティカル セクションを自動的に検出できます。Polyspace でのスレッド作成とクリティカル セクションの自動検出を参照してください。

同時実行すべき関数がコードにあっても、それらを自動で検出できない場合は、解析前にその関数を指定しなければなりません。これらの関数が共通の変数に対して演算を実行する場合、演算に保護メカニズムを指定しなくてはなりません。

マルチタスキング コード解析のワークフローについては、Polyspace でのマルチタスキング プログラムの解析を参照してください。

マルチタスキング解析用のオプションの指定

次のオプションを使用して、周期タスク、割り込み、および共有変数の保護を指定します。Polyspace デスクトップ製品のユーザー インターフェイスでは、これらのオプションは [構成] ペインの [マルチタスキング] ノードにあります。次のオプションは、Bug Finder と Code Prover の両方の解析で使用できます。

Polyspace 解析では、4 つのレベルのタスクの優先順位がサポートされます。つまり、解析で、優先順位の低いタスクが特定のタスクに割り込むことができないことを考慮に入れることができます。タスクの優先順位を指定するために以下のオプションを使用できます。

優先順位の使用例については、マルチタスキング コードでの共有変数の保護を参照してください。

Code Prover マルチタスキング解析へのコードの適応

Code Prover のマルチタスキング解析は、保護されていない可能性のある共有変数をより網羅的に特定するため、厳格なモデルに従います。

タスクと割り込みは void(void) 関数でなければなりません。

タスクおよび割り込みとして指定する関数は、以下のプロトタイプを持たなければなりません。

void func(void);

引数 int を取り int 型を返す関数 func を指定するとします。

int func(int);
volatile 値を使用する func を呼び出すラッパー void-void 関数を定義します。このラッパー関数を、タスクまたは割り込みとして指定します。
void func_wrapper() {
  volatile int arg;
  (void)func(arg);
}
ラッパー関数定義を元の関数の宣言とともに別のファイルに保存し、このファイルを解析に追加することができます。

main 関数は終了しなければなりません。

Code Prover では、main 関数はすべてのタスクと割り込みが開始する前に終了していると見なされます。main 関数が無限ループやランタイム エラーを含む場合、タスクと割り込みは解析されません。タスクや割り込みのチェックがない場合、赤い破線の下線が付いたトークンを探し、main 関数の問題を特定します。コードがチェックされない理由を参照してください。

main 関数を周期タスクとして指定するとします。

void performTask1Cycle(void);
void performTask2Cycle(void);

void main() {
 while(1) {
    performTask1Cycle();
  } 
}

void task2() {
 while(1) {
    performTask2Cycle();
  }
}

main の定義を以下で置き換えます。

#ifdef POLYSPACE
void main() {
}
void task1() {
 while(1) {
    performTask1Cycle();
  } 
}

#else
void main() {
 while(1) {
    performTask1Cycle();
  } 
}
#endif
この置き換えでは、マクロ POLYSPACE が定義されている場合、空の main が定義され、main の内容が別の関数 task1 に配置されます。オプション [プリプロセッサ定義] (-D) を使用してマクロ POLYSPACE を定義し、オプション [タスク] (-entry-points) に task1 を指定します。

この仮定は、自動的に検出されたスレッドには適用されません。たとえば、main 関数は pthread_create を使用してスレッドを作成できます。

Polyspace マルチタスキング解析は、タスクまたは割り込みがそれ自身に割り込む可能性がないことを前提としています。

すべてのタスクと割り込みは任意の順序で任意の回数実行できます。

Code Prover 解析では、すべてのタスクと割り込みは任意の順序で任意の回数実行できると見なされます。

次の例で、reset と inc を周期タスクとして指定するとします。解析では、操作 var+=2 に対してオーバーフローが示されます。

void reset(void) {
 var=0;
}

void inc(void) {
  var+=2;
}

inc が 5 回実行された後に reset が実行されるように、タスクのスケジューリングをモデル化するとします。この順序を実装するラッパー関数を作成します。reset と inc の代わりに、この新しい関数を周期タスクとして指定します。

void task() {
 volatile int randomValue = 0;
 while(randomValue) {
   inc();
   inc();
   inc();
   inc();
   inc();
   reset();
   }
 }

inc が 0 ～ 5 回実行された後に reset が実行されるように、タスクのスケジューリングをモデル化するとします。この順序を実装するラッパー関数を作成します。reset と inc の代わりに、この新しい関数を周期タスクとして指定します。

void task() {
 volatile int randomValue = 0;
 while(randomValue) {
   if(randomValue)
     inc();
   if(randomValue)
     inc();
   if(randomValue)
     inc();
   if(randomValue)
     inc();
   if(randomValue)
     inc();
   reset();
   }
 }

参考

トピック