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.

This option is not available for code generated from MATLAB^® code or Simulink^® models.

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

Set Option

User interface (desktop products only): In your project configuration, the option is available on the Multitasking node. See Dependencies for other options that you must enable or disable.

User interface (Polyspace Platform, desktop products only): In your project configuration, the option is on the Static Analysis tab on the Multitasking node. See Dependencies for other options you must also enable.

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

expand all

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.

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

Description

Set Option

Why Use This Option

Settings

Dependencies

Command-Line Information

Version History

R2024b: Signal handlers are assumed to be asynchronous

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

See Also

Topics

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

Description

Set Option

Why Use This Option

Settings

Dependencies

Command-Line Information

Version History

R2024b: Signal handlers are assumed to be asynchronous

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

See Also

Topics

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

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