#include <pthread.h>
pthread_mutex_t lock1;
pthread_mutex_t lock2;
pthread_mutex_t lock3;
void t0 (void) {
pthread_mutex_lock (&lock1);
pthread_mutex_lock (&lock2);
pthread_mutex_lock (&lock3);
pthread_mutex_unlock (&lock2);
pthread_mutex_unlock (&lock1);
pthread_mutex_unlock (&lock3);
}
void t1 (void) {
pthread_mutex_lock (&lock1);
pthread_mutex_lock (&lock2);
pthread_mutex_destroy (&lock3);
pthread_mutex_unlock (&lock2);
pthread_mutex_unlock (&lock1);
}
In this example, after task t0 locks the
mutex lock3, task t1 can destroy
it. The destruction occurs if the following events happen in sequence:
t0 acquires lock3.
t0 releases lock2.
t0 releases lock1.
t1 acquires the lock lock1 released
by t0.
t1 acquires the lock lock2 released
by t0.
t1 destroys lock3.
For simplicity, this example uses a mix of automatic and
manual concurrency detection. The tasks t0 and t1 are
manually specified as entry points by using the option Tasks (-entry-points). For more information on analysis options, see the
documentation for Polyspace®
Bug Finder™ or Polyspace
Bug Finder
Server™.The critical sections are implemented through primitives
pthread_mutex_lock and pthread_mutex_unlock that the
software detects automatically. In practice, for entry point specification (thread creation),
you will use primitives such as pthread_create. The next example shows how
the defect can appear when you use pthread_create.
Correction — Place Lock-Unlock Pair Together in Same
Critical Section as DestructionThe locking and destruction of lock3 occurs
inside the critical section imposed by lock1 and lock2,
but the unlocking occurs outside. One possible correction is to place
the lock-unlock pair in the same critical section as the destruction
of the mutex. Use one of these critical sections:
In this corrected code, the lock-unlock pair and the destruction
is placed in the critical section imposed by lock1 and lock2.
When t0 acquires lock1 and lock2, t1 has
to wait for their release before it executes the instruction pthread_mutex_destroy
(&lock3);. Therefore, t1 cannot destroy
mutex lock3 in the locked state.
#include <pthread.h>
pthread_mutex_t lock1;
pthread_mutex_t lock2;
pthread_mutex_t lock3;
void t0 (void) {
pthread_mutex_lock (&lock1);
pthread_mutex_lock (&lock2);
pthread_mutex_lock (&lock3);
pthread_mutex_unlock (&lock3);
pthread_mutex_unlock (&lock2);
pthread_mutex_unlock (&lock1);
}
void t1 (void) {
pthread_mutex_lock (&lock1);
pthread_mutex_lock (&lock2);
pthread_mutex_destroy (&lock3);
pthread_mutex_unlock (&lock2);
pthread_mutex_unlock (&lock1);
}