Extend Concurrency Defect Checkers to Unsupported Multithreading Environments

This topic shows how to adapt concurrency defect checkers to unsupported multithreading environments, for instance, when a new thread creation is not detected automatically.

Identify Need for Extending Checker

By default, Bug Finder can detect concurrency primitives in certain families only (in Code Prover, the same automatic detection is available on an option). See Auto-Detection of Thread Creation and Critical Section in Polyspace. If you use primitives that do not belong to one of the supported families but have similar syntaxes, you can map your thread creation and other concurrency-related functions to the supported functions.

For instance, the following example uses:

The function createTask to create a new thread.
The function takeLock to begin a critical section.
The function releaseLock to end the critical section.

typedef void* (*FUNT) (void*);

extern int takeLock(int* t);
extern int releaseLock(int* t);
// First argument is the function, second the id
extern int createTask(FUNT,int*,int*,void*);

int t_id1,t_id2;
int lock;

int var1; 
int var2; 

void* task1(void* a) {
    takeLock(&lock);
    var1++;
    var2++;
    releaseLock(&lock);
    return 0;
}

void* task2(void* a) {
    takeLock(&lock);
    var1++;
    releaseLock(&lock);
    var2++;
    return 0;
}

void main() {
    createTask(task1,&t_id1,0,0);
    createTask(task2,&t_id2,0,0);
}

Bug Finder does not detect the invocation of createTask as the creation of a new thread where control flow goes to the start function of the thread (first argument of createTask). The incorrect placement of the function releaseLock in task2 and the possibility of a data race on the unprotected shared variable var2 remains undetected.

However, the signature of createTask, takeLock and releaseLock are similar to the corresponding POSIX^® functions, pthread_create, pthread_mutex_lock and pthread_mutex_unlock. The order of arguments of these functions might be different from their POSIX equivalents.

Extend Checker

Since a POSIX thread creation can be detected automatically, map your thread creation and other concurrency-related functions to their POSIX equivalents. For instance, in the preceding example, perform the following mapping:

createTask → pthread_create
takeLock → pthread_mutex_lock
releaseLock → pthread_mutex_unlock

To perform the mapping:

List each mapping in an XML file in a specific syntax.
Copy the template file code-behavior-specifications-template.xml from the folder polyspaceroot\polyspace\verifier\cxx to a writable location and modify the file. Enter each mapping in the file using the following syntax after existing similar entries:
```
<function name="createTask" std="pthread_create" >
    <mapping std_arg="1" arg="2"></mapping>
    <mapping std_arg="3" arg="1"></mapping>
    <mapping std_arg="2" arg="3"></mapping>
    <mapping std_arg="4" arg="4"></mapping>
</function>
<function name="takeLock" std="pthread_mutex_lock" >
</function>
<function name="releaseLock" std="pthread_mutex_unlock" >
</function>
```
Note that when mapping createTask to pthread_create, argument remapping is required, because the arguments do not correspond exactly. For instance, the thread start routine is the third argument of pthread_create but the first argument of createTask.
Remove previously existing entries in the file to avoid warnings.
Specify this XML file as argument for the option -code-behavior-specifications.

If you cannot perform a mapping to one of the supported families of concurrency primitives, you have to set up the multitasking analysis manually. See Configuring Polyspace Multitasking Analysis Manually.

Checkers That Can Be Extended

The concurrency defect checkers that can be extended in this way are:

Documentation