-non-preemptable-tasks

非プリエンプタブルタスクを表す関数の指定

構文

-non-preemptable-tasks function1[,function2[,...]]

-non-preemptable-tasks function1[,function2[,...]] では、非プリエンプタブルタスクを表す関数を指定します。

この関数には、他の非周期のタスクや周期タスクから割り込まれる可能性はありませんが、割り込み (プリエンプタブルまたは非プリエンプタブル) から割り込まれる可能性があります。非周期のタスクはオプション [タスク] (-entry-points) を使用して指定され、周期タスクはオプション [周期タスク] (-cyclic-tasks)、割り込みはオプション [割り込み] (-interrupts) を使用して指定されます。例については、Polyspace でのデータレース検出のタスク優先順位の定義を参照してください。

関数を非プリエンプタブル周期タスクとして指定するには、最初に関数を周期タスクまたは非周期のタスクとして指定しなければなりません。指定する関数は、以下のプロトタイプをもたなければなりません。

void function_name(void);

ユーザーインターフェイス (Polyspace^® デスクトップ製品のみ) では、[構成] ペインの [その他] フィールドにこのオプションを入力します。Otherを参照してください。

次のプログラムを考えます。関数 task1 および task2 は、同時に実行できるタスクを表すものとします。

int x;
void task1() {
    x++;
}
void task2() {
    x = 0;
}
void main() {
}

task1 と task2 が周期タスクであることを指定するために、以下を入力します。

polyspace-bug-finder -sources filename -cyclic-tasks task1,task2

これらのタスクは共有変数 x に同時にアクセスしようとするため、[データレース] 欠陥が表示されます。

task1 を非プリエンプタブルとして指定します。

polyspace-bug-finder -sources multi.c -cyclic-tasks task1,task2 -non-preemptable-tasks task1

task1 の演算 x++ は割り込まれる可能性がなくなるため、[データレース] が表示されなくなります。

このオプションは、Polyspace as You Code 解析では役立ちません。
Code Prover では、このオプションを解釈する際にいくつかの制限があります。その理由は、Code Prover では、すべての操作が非アトミックかつ割り込み可能である可能性があるものと見なされるためです。この過大近似のため、このオプションが無視されているように見える状況になることがあります。例は、Code Prover でのタスクの優先順位の効果 (Polyspace Code Prover)を参照してください。

R2016b で導入