Code Prover の同時実行の自動検出を有効にする (`-enable-concurrency-detection`)

マルチスレッド関数の特定ファミリの自動検出

説明

このオプションは Code Prover 解析のみに影響します。

解析で POSIX^®、VxWorks^®、Windows^®、μC/OS III、およびその他のマルチスレッド関数を自動検出するかどうかを指定します。

オプションの設定

以下のいずれかの方法を使用してオプションを設定します。

Polyspace^® ユーザーインターフェイス (デスクトップ製品のみ): プロジェクト構成で [マルチタスキング] ノードを選択してから、このオプションを選択します。このオプションのその他の要件については、依存関係 (Polyspace Code Prover)を参照してください。
Polyspace Platform ユーザーインターフェイス (デスクトップ製品のみ): プロジェクト構成の [静的解析] タブで [マルチタスキング] ノードを選択してから、このオプションを選択します。このオプションのその他の要件については、依存関係 (Polyspace Code Prover)を参照してください。
コマンドラインとオプションファイル: オプション -enable-concurrency-detection を使用します。コマンドライン情報を参照してください。

このオプションを使用する理由

このオプションを使用すると、Polyspace では、使用しているマルチスレッド関数からマルチタスキングモデルが判断されます。Bug Finder では、同時実行の自動検出は既定で有効になっています。Code Prover では、同時実行の自動検出を明示的に有効にしなければなりません。

場合によっては、同時実行の自動検出を使用すると、Code Prover 解析の速度が低下する可能性があります。その場合は、このオプションを有効にせず、マルチタスキングモデルを明示的に指定することを選択できます。Polyspace マルチタスキング解析の手動設定を参照してください。

設定

オン

サポートされているいずれかのマルチタスキング用関数を使用すると、解析によってコードからマルチタスキングモデルが自動的に検出されます。

スレッドの自動検出でサポートされるマルチタスキング関数と制限のリストについては、Polyspace でのスレッド作成とクリティカルセクションの自動検出を参照してください。

オフ (既定の設定)

解析では、コードからのマルチタスキングモデルの検出を試みません。

マルチタスクモデルを手動で構成する場合は、を参照してください。

依存関係

このオプションを有効にする場合、コードに main 関数が含まれていなければなりません。Code Prover オプションを使用して main を生成することはできません。

コマンドライン情報

パラメーター: -enable-concurrency-detection

既定値: オフ

例 (Code Prover): polyspace-code-prover -sources file_name -enable-concurrency-detection

例 (Code Prover Server): polyspace-code-prover-server -sources file_name -enable-concurrency-detection

バージョン履歴

すべて展開する

R2024b: 信号ハンドラーは非同期であると見なされる

Polyspace Code Prover™ でこのオプションを有効にして同時実行コードを検証する場合、signal() または std::signal() 関数を使用して指定された信号処理関数は非同期であると見なされます。つまり、Polyspace は信号ハンドラーを自動的に検出し、それらの信号ハンドラーをプリエンプタブル割り込みとしてモデル化するようになりました。Polyspace は次のように仮定します。

プログラムの実行中には随時、信号ハンドラー関数を実行できる。
信号ハンドラー関数の実行を他のタスクによって中断することはできない。信号ハンドラー関数は、その他の割り込みによって中断される場合がある。

Polyspace での信号ハンドラーの取り扱いが変更されため、Code Prover の結果が変わる可能性があります。次のコードについて考えます。

#include <stdbool.h>
#include <signal.h>

static bool cond = true;
typedef struct handler_s {
	int sig;
	void (* f)(int);
} handler;

static void signal_handler1(int sig) {

	if(sig == SIGSEGV) {
		cond = false;
	}
}

static void signal_handler2(int sig) {

	if(sig == SIGSEGV) {
		cond = false;
	}
}

void func(void) {
	assert(cond);   // Orange

	signal(SIGTERM, &signal_handler1);

	// even if signal_handler1 is called, it cannot set 'cond' to false for SIGTERM
	assert(cond);   //Orange

	// same handler: no creation, but modification of 
	// created interrupt to accepet SIGSEGV as parameter
	signal(SIGSEGV, &signal_handler1);

	assert(cond);  //Orange

	// remove handler for SIGSEGV
	signal(SIGSEGV, SIG_DFL);
	cond = true;

	assert(cond);    //Orange

	handler signals[2] = {{SIGSEGV, &signal_handler2}, {SIGTERM, &signal_handler2}};

	int i;
	for(i = 0; i < 2; i++) {
		signal(signals[i].sig, signals[i].f);
	}

	return;
}

int main(void) {

	func();
	return 0;
}

この場合、Polyspace は、関数 signal_handler1() および signal_holder2() は随時実行可能であると仮定し、変数 cond を false に設定します。この変数でのアサーションは、一部の実行パスでは失敗する可能性があるため、Polyspace はオレンジの [ユーザーアサーション] (Polyspace Code Prover) チェックを報告します。これまでは、これらのアサーションはグリーンチェックとして報告されていました。

R2024b: `std::thread` にポインター渡しされるクラスメンバー関数が検出される

Polyspace は、クラスメンバー std::thread にポインター渡しされると、それらのメンバー関数の実行を検出します。たとえば以下のコードでは、Polyspace は、関数 myClass::func がスレッド th によって実行されることを検出します。Polyspace は、assert ステートメントに対してグリーンチェックを報告します。

#include <thread>
#include <assert.h>

class myClass {
public:
	void func(char *command) {
		assert(1);  // Green check
	}
};

int main() {
	myClass *myPtr = new myClass();
	std::thread th(&myClass::func, myPtr, "values");

	return 0;
}

これまでは、Polyspace は myClass::func を、到達不能コードから呼び出される関数として扱っていました。

参考

グローバル変数の共有と使用のみを表示 (-shared-variables-mode) (Polyspace Code Prover)

Code Prover の同時実行の自動検出を有効にする (-enable-concurrency-detection)

説明