サポートされていないマルチスレッド環境への同時実行欠陥チェッカーの拡張

このトピックでは、新しいスレッドの作成が自動的に検出されない場合など、サポートされていないマルチスレッド環境に同時実行欠陥チェッカーを導入する方法を説明します。

チェッカーの拡張が必要かどうかの特定

既定で、Bug Finder は、特定のファミリに属している同時実行プリミティブしか検出できません (Code Prover では、同じ自動検出をオプションで利用できます)。Polyspace でのスレッド作成とクリティカル セクションの自動検出を参照してください。サポートされているファミリのいずれにも属していないが、構文が似ているプリミティブを使用する場合は、スレッド作成やその他の同時実行関連関数をサポートされている関数にマッピングできます。

次に例をあげます。

  • 関数 createTask を使用して、新しいスレッドを作成する。

  • 関数 takeLock を使用して、クリティカル セクションを開始する。

  • 関数 releaseLock を使用して、クリティカル セクションを終了する。

typedef void* (*FUNT) (void*);

extern int takeLock(int* t);
extern int releaseLock(int* t);
// First argument is the function, second the id
extern int createTask(FUNT,int*,int*,void*);

int t_id1,t_id2;
int lock;

int var1; 
int var2; 

void* task1(void* a) {
    takeLock(&lock);
    var1++;
    var2++;
    releaseLock(&lock);
    return 0;
}

void* task2(void* a) {
    takeLock(&lock);
    var1++;
    releaseLock(&lock);
    var2++;
    return 0;
}

void main() {
    createTask(task1,&t_id1,0,0);
    createTask(task2,&t_id2,0,0);
}

Bug Finder は、制御フローがスレッドの開始関数 (createTask の第 1 引数) に移行するスレッドの新規作成である createTask の呼び出しを検出しません。task2 における関数 releaseLock の間違った配置と保護されていない共有変数 var2 上でのデータ レースの可能性は検出されないままです。

ただし、createTask、takeLock、および releaseLock の署名は、対応する POSIX® 関数の pthread_create、pthread_mutex_lock、および pthread_mutex_unlock と同様です。これらの関数の引数の順序は、POSIX と同等の関数とは異なる可能性があります。

チェッカーの拡張

POSIX スレッド作成は自動的に検出されるため、スレッド作成とその他の同時実行関連の関数を POSIX と同等の関数にマッピングします。たとえば、前述の例では、次のマッピングを実行します。

  • createTask → pthread_create

  • takeLock → pthread_mutex_lock

  • releaseLock → pthread_mutex_unlock

マッピングを実行するには、次のようにします。

  1. 特定の構文で XML ファイル内のマッピングを列挙します。

    テンプレート ファイル code-behavior-specifications-template.xml をフォルダー polyspaceroot\polyspace\verifier\cxx から書き込み可能な場所にコピーし、そのファイルを変更します。以下の構文を使用して、ファイル内の各マッピングを既存の同様のエントリの後ろに入力します。

    <function name="createTask" std="pthread_create" >
    <mapping std_arg="1" arg="2"></mapping>
    <mapping std_arg="3" arg="1"></mapping>
    <mapping std_arg="2" arg="3"></mapping>
    <mapping std_arg="4" arg="4"></mapping>
</function>
<function name="takeLock" std="pthread_mutex_lock" >
</function>
<function name="releaseLock" std="pthread_mutex_unlock" >
</function>
    createTask を pthread_create にマッピングしても、引数が正確に対応しないため、引数の再マッピングが必要になることに注意してください。たとえば、スレッド開始ルーチンは、pthread_create では 3 番目の引数ですが、createTask では最初の引数です。

    警告を回避するため、ファイル内の既存のエントリは削除してください。

  2. この XML ファイルをオプション -code-behavior-specifications の引数として指定します。

サポートされている同時実行プリミティブのファミリのいずれかに対するマッピングを実行できない場合は、マルチタスキング解析を手動でセットアップする必要があります。Polyspace マルチタスキング解析の手動設定を参照してください。

拡張可能なチェッカー

この方法で拡張可能な同時実行欠陥チェッカーを以下に示します。

制限

カスタム スレッド作成関数とロック/ロック解除関数を同様の標準ライブラリ関数にマッピングできます。その場合、以下の制約が適用されます。

  • カスタム関数には、標準ライブラリ関数と同じ数あるいはそれ以上の数の引数が必要です。標準ライブラリ関数のすべての引数がカスタム関数の引数にマッピングされるようにします。引数の再マッピングの例については、-code-behavior-specifications も参照してください。

  • マッピングされた関数の引数には、互換性のあるデータ型がなければなりません。同様に、カスタム関数の戻り値の型には、標準ライブラリ関数との互換性がなければなりません。次に例を示します。

    • 整数型 (char、int など) には、浮動小数点型 (float、double など) との互換性がありません。

    • 基本型には、構造体または列挙値との互換性がありません。

    • ポインター型には、非ポインター型との互換性がありません。

参考

トピック