Enable automatic concurrency detection for Code Prover (-enable-concurrency-detection)

Automatically detect certain families of multithreading functions

Description

This option affects a Code Prover analysis only.

Specify whether the analysis must automatically detect POSIX^®, VxWorks^®, Windows^®, μC/OS III and other multithreading functions.

Set Option

Set the option using one of these methods:

• Polyspace^® user interface (desktop products only): In your project configuration, select the Multitasking node and then select this option. See Dependencies for other requirements on this option.

• Polyspace Platform user interface (desktop products only): In your project configuration, on the Static Analysis tab, select the Multitasking node and then select this option. See Dependencies for other requirements on this option.

• Command line and options file: Use the option -enable-concurrency-detection. See Command-Line Information.

Why Use This Option

If you use this option, Polyspace determines your multitasking model from your use of multithreading functions. In Bug Finder, automatic concurrency detection is enabled by default. In Code Prover, you have to explicitly enable automatic concurrency detection.

In some cases, using automatic concurrency detection can slow down the Code Prover analysis. In those cases, you can choose to not enable this option and explicitly specify your multitasking model. See Configuring Polyspace Multitasking Analysis Manually.

Settings

On

If you use one of the supported functions for multitasking, the analysis automatically detects your multitasking model from your code.

For a list of supported multitasking functions and limitations in auto-detection of threads, see Auto-Detection of Thread Creation and Critical Section in Polyspace.

Off (default)

The analysis does not attempt to detect the multitasking model from your code.

If you want to manually configure your multitasking model, see Configuring Polyspace Multitasking Analysis Manually.

Dependencies

If you enable this option, your code must contain a main function. You cannot use the Code Prover options to generate a main.

Command-Line Information

Parameter: -enable-concurrency-detection

Default: Off

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

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

Version History

R2024b: Signal handlers are assumed to be asynchronous

When verifying concurrent code in Polyspace Code Prover™ by enabling this option, the signal handler functions specified using the signal() or std::signal() function are assumed to be asynchronous. That is, Polyspace now detects the signal handlers automatically and models them as preemptable interrupts. Polyspace now assumes:

• Signal handling functions can be executed any time during the program execution.

• Execution of the signal handling functions cannot be interrupted by other tasks. Signal handling functions can be interrupted by other interrupts.

Because of the change in how Polyspace treats signal handling, Code Prover results can change. Consider this code:

#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;
}

Here, Polyspace assumes that the functions signal_handler1() and signal_holder2() can execute at any time, setting the variable cond to false. Because the assertions on this variable can fail in some execution paths, Polyspace reports orange User assertion checks. Previously, these assertions were reported as green checks.

R2024b: Class member functions passed by pointer to std::thread are detected

Polyspace detects the execution of class member functions when they are passed by pointer to std::thread. For example, in this code, Polyspace detects that the function myClass::func is executes by the thread th. Polyspace reports a green check on the assert statement.

#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;
}

Previously, Polyspace treated myClass::func as a function called from unreachable code.