Auto-Detection of Thread Creation and Critical Section in Polyspace

With Polyspace^®, you can analyze programs where multiple threads run concurrently. Polyspace can analyze your multitasking code for data races, deadlocks and other concurrency defects, if the analysis is aware of the concurrency model in your code. In some situations, Polyspace can detect thread creation and critical sections in your code automatically. Bug Finder detects them by default. In Code Prover, you enable automatic detection using the option Enable automatic concurrency detection for Code Prover (-enable-concurrency-detection).

For the multitasking code analysis workflow, see Analyze Multitasking Programs in Polyspace.

If your thread creation function is not detected automatically:

• You can also map the function to a thread-creation function that Polyspace can detect automatically. Use the option -code-behavior-specifications.

• Otherwise, you must manually model your multitasking threads by using configuration options. See Configuring Polyspace Multitasking Analysis Manually.

Multitasking Routines that Polyspace Can Detect

Polyspace can detect thread creation and critical sections if you use primitives from these groups. Polyspace recognizes calls to these routines as the creation of a new thread or as the beginning or end of a critical section.

POSIX

Thread creation: pthread_create

Critical section begins: pthread_mutex_lock

Critical section ends: pthread_mutex_unlock

VxWorks

Thread creation: taskSpawn

Critical section begins: semTake

Critical section ends: semGive

To activate automatic detection of concurrency primitives for VxWorks^®, in the user interface of the Polyspace desktop products, use the VxWorks template. For more information on templates, see Create Project Using Configuration Template (Polyspace Code Prover). At the command-line, use these options:

-D1=CPU=I80386
-D2=__GNUC__=2
-D3=__OS_VXWORKS

Concurrency detection is possible only if the multitasking functions are created from an entry point named main. If the entry point has a different name, such as vxworks_entry_point, do one of the following:

• Provide a main function.

• Preprocessor definitions (-D): In preprocessor definitions, set vxworks_entry_point=main.

Windows

Thread creation: CreateThread

Critical section begins: EnterCriticalSection

Critical section ends: LeaveCriticalSection

μC/OS II

Thread creation: OSTaskCreate

Critical section begins: OSMutexPend

Critical section ends: OSMutexPost

C++11

Thread creation: std::thread::thread

Critical section begins: std::mutex::lock

Critical section ends: std::mutex::unlock

For autodetection of C++11 threads, explicitly specify paths to your compiler header files or use polyspace-configure.

For instance, if you use std::thread for thread creation, explicitly specify the path to the folder containing thread.h.

See also Limitations of Automatic Thread Detection.

C11

Thread creation: thrd_create

Critical section begins: mtx_lock

Critical section ends: mtx_unlock

Example of Automatic Thread Detection

The following multitasking code models five philosophers sharing five forks. The example uses POSIX^® thread creation routines and illustrates a classic example of a deadlock. Run Bug Finder on this code to see the deadlock.

#include "pthread.h" #include <stdio.h> #include <unistd.h> pthread_mutex_t forks[5]; void* philo1(void* args) { while (1) { printf("Philosopher 1 is thinking\n"); sleep(1); pthread_mutex_lock(&forks[0]); printf("Philosopher 1 takes left fork\n"); pthread_mutex_lock(&forks[1]); printf("Philosopher 1 takes right fork\n"); printf("Philosopher 1 is eating\n"); sleep(1); pthread_mutex_unlock(&forks[1]); printf("Philosopher 1 puts down right fork\n"); pthread_mutex_unlock(&forks[0]); printf("Philosopher 1 puts down left fork\n"); } return NULL; } void* philo2(void* args) { while (1) { printf("Philosopher 2 is thinking\n"); sleep(1); pthread_mutex_lock(&forks[1]); printf("Philosopher 2 takes left fork\n"); pthread_mutex_lock(&forks[2]); printf("Philosopher 2 takes right fork\n"); printf("Philosopher 2 is eating\n"); sleep(1); pthread_mutex_unlock(&forks[2]); printf("Philosopher 2 puts down right fork\n"); pthread_mutex_unlock(&forks[1]); printf("Philosopher 2 puts down left fork\n"); } return NULL; } void* philo3(void* args) { while (1) { printf("Philosopher 3 is thinking\n"); sleep(1); pthread_mutex_lock(&forks[2]); printf("Philosopher 3 takes left fork\n"); pthread_mutex_lock(&forks[3]); printf("Philosopher 3 takes right fork\n"); printf("Philosopher 3 is eating\n"); sleep(1); pthread_mutex_unlock(&forks[3]); printf("Philosopher 3 puts down right fork\n"); pthread_mutex_unlock(&forks[2]); printf("Philosopher 3 puts down left fork\n"); } return NULL; } void* philo4(void* args) { while (1) { printf("Philosopher 4 is thinking\n"); sleep(1); pthread_mutex_lock(&forks[3]); printf("Philosopher 4 takes left fork\n"); pthread_mutex_lock(&forks[4]); printf("Philosopher 4 takes right fork\n"); printf("Philosopher 4 is eating\n"); sleep(1); pthread_mutex_unlock(&forks[4]); printf("Philosopher 4 puts down right fork\n"); pthread_mutex_unlock(&forks[3]); printf("Philosopher 4 puts down left fork\n"); } return NULL; } void* philo5(void* args) { while (1) { printf("Philosopher 5 is thinking\n"); sleep(1); pthread_mutex_lock(&forks[4]); printf("Philosopher 5 takes left fork\n"); pthread_mutex_lock(&forks[0]); printf("Philosopher 5 takes right fork\n"); printf("Philosopher 5 is eating\n"); sleep(1); pthread_mutex_unlock(&forks[0]); printf("Philosopher 5 puts down right fork\n"); pthread_mutex_unlock(&forks[4]); printf("Philosopher 5 puts down left fork\n"); } return NULL; } int main(void) { pthread_t ph[5]; pthread_create(&ph[0], NULL, philo1, NULL); pthread_create(&ph[1], NULL, philo2, NULL); pthread_create(&ph[2], NULL, philo3, NULL); pthread_create(&ph[3], NULL, philo4, NULL); pthread_create(&ph[4], NULL, philo5, NULL); pthread_join(ph[0], NULL); pthread_join(ph[1], NULL); pthread_join(ph[2], NULL); pthread_join(ph[3], NULL); pthread_join(ph[4], NULL); return 1; }

Each philosopher needs two forks to eat, a right and a left fork. The functions philo1, philo2, philo3, philo4, and philo5 represent the philosophers. Each function requires two pthread_mutex_t resources, representing the two forks required to eat. All five functions run at the same time in five concurrent threads.

However, a deadlock occurs in this example. When each philosopher picks up their first fork (each thread locks one pthread_mutex_t resource), all the forks are being used. So, the philosophers (threads) wait for their second fork (second pthread_mutex_t resource) to become available. However, all the forks (resources) are being held by the waiting philosophers (threads), causing a deadlock.

Naming Convention for Automatically Detected Threads

If you use a function such as pthread_create() to create new threads (tasks), each thread is associated with an unique identifier. For instance, in this example, two threads are created with identifiers id1 and id2.

pthread_t* id1, id2; void main() { pthread_create(id1, NULL, start_routine, NULL); pthread_create(id2, NULL, start_routine, NULL); }

If a data race occurs between the threads, the analysis can detect it. When displaying the results, the threads are indicated as task_id, where id is the identifier associated with the thread. In the preceding example, the threads are identified as task_id1 and task_id2.

If a thread identifier is:

• Local to a function, the thread name shows the function.

  For instance, the thread created below appears as task_f:id

  void f(void) { pthread_t* id; pthread_create(id, NULL, start_routine, NULL); }

• A field of a structure, the thread name shows the structure.

  For instance, the thread created below appears as task_a#id

  struct {pthread_t* id; int x;} a; pthread_create(a.id,NULL,start_routine,NULL);

• An array member, the thread name shows the array.

  For instance, the thread created below appears as task_tab[1].

  pthread_t* tab[10]; pthread_create(tab[1],NULL,start_routine,NULL);

If you create two threads with distinct thread identifiers, but you use the same local variable name for the thread identifiers, the name of the second thread is modified to distinguish it from the first thread. For instance, the threads below appear as task_func:id and task_func:id:1.

void func() { { pthread_t id; pthread_create(&id, NULL, &task, NULL); } { pthread_t id; pthread_create(&id, NULL, &task, NULL); } }

Limitations of Automatic Thread Detection

The multitasking model extracted by Polyspace does not include some features. Polyspace cannot model:

• Thread priorities and attributes — Ignored by Polyspace.

• Recursive semaphores.

• Unbounded thread identifiers, such as extern pthread_t ids[] — Warning.

• Calls to concurrency primitive through high-order calls — Warning.

• Aliases on thread identifiers — Polyspace over-approximates when the alias is used.

• Termination of threads — Polyspace ignores pthread_join and thrd_join. Polyspace replaces pthread_exit and thrd_exit by a standard exit.

• (Polyspace Bug Finder™ only) Creation of multiple threads through multiple calls to the same function with different pointer arguments.

   Example

  In this example, Polyspace considers that only one thread is created.

  pthread_t id1, id2; void start(pthread_t* id) { pthread_create(id, NULL, start_routine, NULL); } void main() { start(&id1); start(&id2); }

• (Polyspace Code Prover™ only) Shared local variables — Only global variables are considered shared. If a local variable is accessed by multiple threads, the analysis does not take into account the shared nature of the variable.

   Example

  In this example, the analysis does not take into account that the local variable x can be accessed by both task1 and task2 (after the new thread is created).

  #include <pthread.h> #include <stdlib.h> void* task2(void* args) { int* x = (int*) args; *x = 1; return (void*)x; } void task1() { int x; x = 2; pthread_t id; (void)pthread_create(&id, NULL, task2, (void*) &x); /* x (local var) passed to task2 */ x = 3 ; /* Unknown thread priority means x = 1 OR x = 3.*/ /* However, the analysis considers x = 3 */ /* Assertion below is green */ assert(x == 3); } int main(void) { task1(); return 0; }

• (Polyspace Code Prover only) Shared dynamic memory — Only global variables are considered shared. If a dynamically allocated memory region is accessed by multiple threads, the analysis does not take into account its shared nature.

   Example

  In this example, the analysis does not take into account that lx points to a shared memory region. The region can be accessed by both task1 and task2 (after the new thread is created). The Code Prover analysis also reports lx as a non-shared variable.

  #include <pthread.h> #include <stdlib.h> static int* lx; void* task2(void* args) { int* x = (int*) args; *x = 1; return (void*)x; } void task1() { pthread_t id; lx = (int*)malloc(sizeof(int)); if (lx == NULL) exit(1); (void)pthread_create(&id, NULL, task2, (void*) lx); *lx = 3 ; /* Unknown thread priority means *lx = 1 OR *lx = 3.*/ /* However, the analysis considers *lx = 3 */ /* Assertion below is green */ assert(*lx == 3); } int main(void) { task1(); return 0; }

• Number of tasks created with CreateThread when threadId is set to NULL— When you create multiple threads that execute the same function, if the last argument of CreateThread is NULL, Polyspace only detects one instance of this function, or task.

   Example

  In this example, Polyspace detects only one instance of thread_function1(), but 10 instances of thread_function2().

  #include <windows.h> #define MAX_LOOP_THREADS 10 DWORD WINAPI thread_function1(LPVOID data) {} DWORD WINAPI thread_function2(LPVOID data) {} HANDLE hds1[MAX_LOOP_THREADS]; HANDLE hds2[MAX_LOOP_THREADS]; DWORD threadId[MAX_LOOP_THREADS]; int main(void) { for (int i = 0; i < MAX_LOOP_THREADS; i++) { hds1[i] = CreateThread(NULL, 0, thread_function1, NULL, 0, NULL); hds2[i] = CreateThread(NULL, 0, thread_function2, NULL, 0, &threadId[i]); } return 0; }

• (C++11 only) If you use lambda expressions as start functions during thread creation, Polyspace does not detect shared variables in the lambda expressions.

   Example

  In this example, Polyspace does not detect that the variable y used in the lambda expressions is shared between two threads. As a result, Bug Finder, for instance, does not show a Data race defect.

  #include <thread> int y; int main() { std::thread t1([] {y++;}); std::thread t2([] {y++;}); t1.join(); t2.join(); return 0; }

• (C++11 threads with Polyspace Code Prover only) String literals as thread function argument — Code Prover shows a red Illegally dereferenced pointer error if the thread function has an std::string& parameter and you pass a string literal argument.

   Example

  In this example, the thread function foo has an std::string& parameter. When starting a thread, a string literal is passed as argument to this function, which undergoes an implicit conversion to std::string type. Code Prover loses track of the original string literal in this conversion. Therefore, a dashed red underline appears on operator<< in the body of foo and a red Illegally dereferenced pointer check in the body of operator<<.

  #include <iostream> #include <thread> using namespace std; void foo(const std::string& f) { std::cout << f; } void main() { std::thread t1(foo,"foo_arg"); }

  To work around this issue, assign the string literal to a temporary variable and pass the variable as argument to the thread function.

  #include <iostream> #include <thread> using namespace std; void foo(const std::string& f) { std::cout << f; } void main() { std::string str = "foo_arg"; std::thread t1(foo, str); }