引数を取る関数によるクリティカル セクションの定義

マルチタスキング コードを検証するとき、Polyspace® はクリティカル セクションがロック関数とロック解除関数の呼び出しの間に存在すると見なします。

lock();
/* Critical section code */
unlock();

クリティカル セクション内の操作のグループは、同じクリティカル セクション内の (つまり、同じ関数でロックおよびロック解除する) 別の操作のグループに対してアトミックです。マルチタスキング コードでのアトミック操作の定義も参照してください。

クリティカル セクションを定義する関数についての Polyspace の仮定

Polyspace はクリティカル セクションを開始および終了させる関数の引数を無視します。

たとえば、以下のコードで、my_task_1 と my_task_2 をエントリ ポイント、my_lock をロック関数、my_unlock をロック解除関数として指定する場合、Polyspace は 2 つのコード セクションを同じクリティカル セクションとして扱います。

int shared_var;

void my_lock(int);
void my_unlock(int);

void my_task_1() {
   my_lock(1);
   /* Critical section code */
   shared_var=0;
   my_unlock(1);
}

void my_task_2() {
   my_lock(2);
   /* Critical section code */
   shared_var++;
   my_unlock(2);
}

その結果、これら 2 つのセクションが保護されていない場合でも、解析では、これらのセクションが互いの割り込みから保護されていると見なされます。たとえば、Bug Finder では shared_var のデータ レースが検出されません。

多くの場合、関数の引数は実行時にのみ判断できます。Polyspace は、静的解析およびランタイム エラー チェック段階の前にクリティカル セクションをモデル化するため、解析では、関数の引数が異なるかどうかを判断できず、引数が無視されます。

引数のあるロック関数およびロック解除関数への Polyspace 解析の適応

クリティカル セクションを定義する関数の引数がコンパイル時の定数である場合、Polyspace の仮定を回避するために解析を適応させることができます。

たとえば、Polyspace 解析オプションを使用すると、前の例のコードを次に示すコードとして Polyspace に認識させることができます。

int shared_var;

void my_lock_1(void);
void my_lock_2(void);
void my_unlock_1(void);
void my_unlock_2(void);

void my_task_1() {
   my_lock_1();
   /* Critical section code */
   shared_var=0;
   my_unlock_1();
}

void my_task_2() {
   my_lock_2();
   /* Critical section code */
   shared_var++;
   my_unlock_2();
}

その後、my_lock_1 と my_lock_2 をロック関数として指定し、my_unlock_1 と my_unlock_2 をロック解除関数として指定すると、解析では、コードの 2 つのセクションが異なるクリティカル セクションの一部として認識されます。たとえば、Bug Finder では shared_var のデータ レースが検出されます。

コンパイル時の定数を引数として取るロック関数およびロック解除関数に解析を適応させるには、次のようにします。

  1. ヘッダー ファイル common_polyspace_include.h で、#define を使用して関数の引数を関数名の拡張に変換します。また、新しい関数の宣言を指定します。

    たとえば、前の例の場合、次の #define と宣言を使用します。

    #define my_lock(X) my_lock_##X()
#define my_unlock(X) my_unlock_##X()

void my_lock_1(void);
void my_lock_2(void);
void my_unlock_1(void);
void my_unlock_2(void);

  2. ファイル名 common_polyspace_include.h をオプション [インクルード] (-include) の引数として指定します。

    解析では、解析されるすべてのソース ファイルに、このヘッダー ファイルが #include されていると見なします。

  3. 新しい関数名をクリティカル セクションを開始および終了する関数として指定します。オプション [クリティカル セクション詳細] (-critical-section-begin -critical-section-end) を使用します。

参考

トピック