Critical section details (-critical-section-begin -critical-section-end)

Specify functions that begin and end critical sections

Description

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

When verifying multitasking code, Polyspace^® considers that a critical section lies between calls to a lock function and an unlock function.

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

Specify the lock and unlock function names for your critical sections (for instance, lock() and unlock() in above example).

Set Option

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

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 -critical-section-begin and -critical-section-end. See Command-Line Information.

Why Use This Option

When a task my_task calls a lock function my_lock, other tasks calling my_lock must wait till my_task calls the corresponding unlock function. Therefore, critical section operations in the other tasks cannot interrupt critical section operations in my_task.

For instance, the operation var++ in my_task1 and my_task2 cannot interrupt each other.

int var;

void my_task1() {
   my_lock();
   var++;
   my_unlock();
}

void my_task2() {
   my_lock();
   var++; 
   my_unlock();
}

Using your specifications, a Code Prover verification checks if your placement of lock and unlock functions protects all shared variables from concurrent access. When determining values of those variables, the verification accounts for the fact that critical sections in different tasks do not interrupt each other.

A Bug Finder analysis uses the critical section information to look for concurrency defects such as data race and deadlock.

Settings

No Default

Click to add a field.

• In Starting routine, enter name of lock function.

• In Ending routine, enter name of unlock function.

Enter function names or choose from a list.

• Click to add a field and enter the function name.

• Click to list functions in your code. Choose functions from the list.

Dependencies

To enable this option in the user interface of the desktop products, first select the option Configure multitasking manually.

Tips

• You can also use primitives such as the POSIX^® functions pthread_mutex_lock and pthread_mutex_unlock to begin and end critical sections. For a list of primitives that Polyspace can detect automatically, see Auto-Detection of Thread Creation and Critical Section in Polyspace.

• For function calls that begin and end critical sections, Polyspace ignores the function arguments.

  For instance, Polyspace treats the two code sections below as the same critical section.

  Starting routine: my_lock
  Ending routine: my_unlock
  void my_task1() { my_lock(1); /* Critical section code */ my_unlock(1); }	void my_task2() { my_lock(2); /* Critical section code */ my_unlock(2); }

  To work around the limitation, see Define Critical Sections with Functions That Take Arguments.

• The functions that begin and end critical sections must be functions. For instance, if you define a function-like macro:

  #define init() num_locks++

  You cannot use the macro init() to begin or end a critical section.

• When you use multiple critical sections, you can run into issues such as:

  • Deadlock: A sequence of calls to lock functions causes two tasks to block each other.

  • Double lock: A lock function is called twice in a task without an intermediate call to an unlock function.

  Use Polyspace Bug Finder™ to detect such issues. See Concurrency Defects.

  Then, use Polyspace Code Prover™ to detect if your placement of lock and unlock functions actually protects all shared variables from concurrent access. See Global Variables (Polyspace Code Prover).

• When considering possible values of shared variables, a Code Prover verification takes into account your specifications for critical sections.

  However, if the shared variable is a pointer or array, the software uses the specifications only to determine if the variable is a shared protected global variable. For run-time error checking, the software does not take your specifications into account and considers that the variable can be concurrently accessed.

Command-Line Information

Parameter: -critical-section-begin | -critical-section-end

No Default

Value: function1:cs1[,function2:cs2[,...]]

Example (Bug Finder): polyspace-bug_finder -sources file_name -critical-section-begin func_begin:cs1 -critical-section-end func_end:cs1

Example (Code Prover): polyspace-code-prover -sources file_name -critical-section-begin func_begin:cs1 -critical-section-end func_end:cs1

Example (Bug Finder Server): polyspace-bug_finder-server -sources file_name -critical-section-begin func_begin:cs1 -critical-section-end func_end:cs1

Example (Code Prover Server): polyspace-code-prover-server -sources file_name -critical-section-begin func_begin:cs1 -critical-section-end func_end:cs1