Polyspace でのデータ レース検出のタスク優先順位の定義

Bug Finder では同時実行タスク間のデータ レースが検出されます。データ レースを修正する方法の 1 つは、特定のタスクの優先順位を上げるように指定することです。優先順位の高いタスクは、優先順位の低いタスクに対してアトミックであり、優先順位の低いタスクが割り込む可能性はありません。

タスクの優先順位のエミュレート

以下のオプションを使用して最大 4 つの異なる優先順位を指定できます (優先順位が高い順にリスト)。

たとえば、割り込みの優先順位が最も高く、他のタスクがプリエンプトする可能性がないとします。プリエンプト可能な割り込みのクラスを定義するには、割り込みをプリエンプタブルにしてその優先順位を低くします。

タスクの優先順位の例

3 つのタスクの例を考えてみます。変数 var は 2 つのタスク task1 と task2 間で共有され、クリティカル セクションのような保護はありません。Bug Finder では、task1 と task2 の優先順位に基づいてデータ レースが示されます。3 番目のタスクはこの例とは関係がありません (クリティカル セクションを含める目的でのみ追加されたものです。このようにしないとデータ レース検出が無効になります)。 

int var;

void begin_critical_section(void);
void end_critical_section(void);

void task1(void)  { 
    var++;
}

void task2(void)  { 
    var = 0;
}

void task3(void){
    begin_critical_section();
    /* Some atomic operation */
    end_critical_section();
}

task1 と task2 の優先順位を調整して、データ レースが検出されるかどうかを確認します。次に例を示します。

  1. 以下のマルチタスキング オプションを設定します。

  2. Bug Finder を実行します。

    データ レースは表示されません。task1 と task2 は非プリエンプタブルな割り込みであるため、共有変数には同時にアクセスできません。

  3. オプション -preemptable-interrupts を使用して、task1 をプリエンタブルな割り込みに変更します。

  4. Bug Finder をもう一度実行します。今回は共有変数 var でのデータ レースが示されます。

その他の調査

この例を以下の方法で変更して、変更の効果を確認します。

  • task1 と task2 を変更します。

    たとえば task1 は非プリエンプタブルな割り込みのままにする一方で、オプション -preemptable-interrupts を使用して task2 はプリエンプタブルな割り込みに変更するとします。

    データ レースが表示されなくなります。理由は以下のとおりです。

    • task1 の優先順位が高いため、task2 が割り込む可能性はありません。

    • task2 の操作がアトミックであるため、task1 が割り込む可能性はありません。

  • オプション -detect-atomic-data-race を指定します。

    データ レースが再び表示されます。チェッカーはすべての操作を非アトミックの可能性があるものと見なすため、task2 の操作に task1 の優先順位が高い操作が割り込むことができるようになります。

解析オプションに対して他の変更を試し、チェッカーの結果を確認してください。

Code Prover でのタスクの優先順位の効果

タスクの優先順位を指定するオプションは、Code Prover でも使用できます。ただし Code Prover では、すべての操作が非アトミックであり、割り込む可能性があるものと見なされます。この過大近似のため、タスクの優先順位の指定が無視されているように見える状況になることがあります。

たとえば、前述の例で Code Prover を実行すると、過大近似のために誤検知が発生する可能性があります。

  • task1 と task2 の両方を非プリエンプタブルな割り込みとして指定すると、共有変数 var はグリーンの [保護された共有グローバル変数] として表示されます。両方のタスクへの割り込みが不可能であるため、これは妥当な結果です。

  • task1 の優先順位を task2 よりも低く指定すると、共有変数 var はオレンジの [保護されていない可能性のある変数] として表示されます。task1 の操作 var++ は非アトミックであり、複数のマシン命令が関与しているため、これは妥当で正確な結果です。この操作に task2 の操作 var = 0 が割り込む可能性があります。

  • task1 の優先順位を task2 よりも高く指定しても、共有変数 var はオレンジの [保護されていない可能性のある変数] として表示されます。これは妥当ですが正確ではない結果です。

    • task1 の優先順位が高いため、task1 の操作 var++ が割り込まれる可能性はありません。

    • task2 の操作 var = 0 はアトミックであるため、割り込まれる可能性はありません。

    ただし Code Prover では、すべての操作が非アトミックである可能性があるものと見なされるため、task2 の var = 0 は割り込み可能と見なされ、引き続き var が保護されていない可能性があるものとして示されます。

参考

Polyspace 解析オプション

Polyspace 結果

トピック