Main Content

Define Critical Sections with Functions That Take Arguments

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

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

A group of operations in a critical section are atomic with respect to another group of operations that are in the same critical section (that is, having the same lock and unlock function). See also Define Atomic Operations in Multitasking Code.

Polyspace Assumption on Functions Defining Critical Sections

Polyspace ignores arguments to functions that begin and end critical sections.

For instance, Polyspace treats the two code sections below as the same critical section if you specify my_task_1 and my_task_2 as entry points, my_lock as the lock function and my_unlock as the unlock function.

int shared_var;

void my_lock(int);
void my_unlock(int);

void my_task_1() {
   my_lock(1);
   /* Critical section code */
   shared_var=0;
   my_unlock(1);
}

void my_task_2() {
   my_lock(2);
   /* Critical section code */
   shared_var++;
   my_unlock(2);
}

As a result, the analysis considers that these two sections are protected from interrupting each other even though they might not be protected. For instance, Bug Finder does not detect the data race on shared_var.

Often, the function arguments can be determined only at run time. Since Polyspace models the critical sections prior to the static analysis and run-time error checking phase, the analysis cannot determine if the function arguments are different and ignores the arguments.

Adapt Polyspace Analysis to Lock and Unlock Functions with Arguments

When the arguments to the functions defining critical sections are compile-time constants, you can adapt the analysis to work around the Polyspace assumption.

For instance, you can use Polyspace analysis options so that the code in the preceding example appears to Polyspace as shown here.

int shared_var;

void my_lock_1(void);
void my_lock_2(void);
void my_unlock_1(void);
void my_unlock_2(void);

void my_task_1() {
   my_lock_1();
   /* Critical section code */
   shared_var=0;
   my_unlock_1();
}

void my_task_2() {
   my_lock_2();
   /* Critical section code */
   shared_var++;
   my_unlock_2();
}

If you then specify my_lock_1 and my_lock_2 as the lock functions and my_unlock_1 and my_unlock_2 as the unlock functions, the analysis recognizes the two sections of code as part of different critical sections. For instance, Bug Finder detects a data race on shared_var.

To adapt the analysis for lock and unlock functions that take compile-time constants as arguments:

  1. In a header file common_polyspace_include.h, convert the function arguments into extensions of the function name with #define-s. In addition, provide a declaration for the new functions.

    For instance, for the preceding example, use these #define-s and declarations:

    #define my_lock(X) my_lock_##X()
#define my_unlock(X) my_unlock_##X()

void my_lock_1(void);
void my_lock_2(void);
void my_unlock_1(void);
void my_unlock_2(void);

  2. Specify the file name common_polyspace_include.h as argument for the option Include (-include).

    The analysis considers this header file as #include-d in all source files that are analyzed.

  3. Specify the new function names as functions beginning and ending critical sections. Use the options Critical section details (-critical-section-begin -critical-section-end).

See Also

Related Topics