Tutorial: Analyzing a Subtle Bug

This tutorial assumes that you have already read the man pages. It also assumes that you are familiar with condition variables.

A subtle bug involving two condition variables

This tutorial is based on a buggy program that appeared in stackoverflow:

https://stackoverflow.com/questions/30554292/c-uninitialized-mutex-works-and-initialized-mutex-fails

Here, we use a slightly modified version of the code that is semantically equivalent, but it makes the logic clearer, and easier to analyze.

The original program had the goal of solving a producer-consumer problem by using two condition variables, instead of the traditional two semaphores. The key to understanding it is to recognize the two structs, inEvents (for producers that add to the buffer), and outEvents (for consumers that remove from the buffer. When a producer or consumer has no more tasks to do, it calls await(), which calls pthread_cond_Wait. When a producer or consumer wants to signal to its pair, it calls advance(), which calls pthread_cond_signal.

As noted in the stackoverflow page referred to, above, the bug is that in the while loop that calls pthread_cond_wait, the predicate being checked is a local variable private to that thread, instead of a global variable.

Nevertheless, the goal of this tutorial is to show how to use McMini in a semi-automated fashion to lead us to the bug. So, we ignore the analysis in stackoverflow, and treat this bug as if it was newly discovered in some legacy code, when a user ran this code for more than 30 seconds.

The revised version to be referenced here is found below, and also in the sidebar. The code has been modified slightly to make clear which code refers producer threads, and which refers to consumer threads.

In addition, the ‘main’ routine has been modified to take a single argument, the bufferSize. As with all debugging of multi-threaded code, the difficulty lies in the combinatorial explosion of possible executions. So, we look for the simplest case exhibiting the bug. To do this, we add the argument bufferSize, instead of accepting the original buffer size of 10.

If you wish to reproduce the results of this tutorial, then copy the tutorial code, above, into subtle.c, and compile it locally.

Note

The first principle is to use a small test case, to limit the combinatorial explosion of traces (thread schedules) to search. In this case, the bufferSize was originally 10. Our version of the program lowers the bufferSize to 1 in the initialization of allVars in ‘main’. After that, we compile the code and run with McMini.

Analyzing the bug for bufferSize==1

Next, we turn our attention to tuning the ‘-m’ parameter. This is important: too large and it runs forever; too small and the trace with the bug doesn’t execute long enough to see the bug.

By trial and error, we found ‘-m 18’ to suffice to show the bug, although a little large is also fine. When we use ‘-m 30’, we find a trace with a bug using 54 transitions. But when reducing this to ‘-m 18’, we find a trace with a bug by using only 28 transitions. Notice that McMini identifies two possible lost wakeups in the trace. (See this web page for a definition of a “lost wakeup”.) The trace is printed below:

In order to see the transitions that result in deadlock, we do:

./mcmini -f -m18 -v ./subtle 1

And the final trace is shown here:

We examine the trace sequence for this program when it reaches deadlock:

./mcmini-gdb -f -m18 ./subtle 1
(gdb) mcmini forward end
(gdb) set paginsation off
(gdb) mcmini printTransitions
...
0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
 1, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 2, 2, 2, 2, 2, 2,
mcmini transitions at end of subtle

From here, we wish to see why Thread 1 executes again during transitions 37 and 38. So, we navigate to just before that transition. To do this, we navigate from transtion 44 to 36, or in other words, mcmini back 8.

./mcmini-gdb -f -m18 ./subtle 1
(gdb) set pagination off
(gdb) mcmini forward end
(gdb) mcmini back 8
(gdb) mcmini printTransitions
...
0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
 1, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,

Now we see that Threads 1 and 2 are both enabled, and the asterisk indicated that the current trace sequence would execute Thread 1 next:

mcmini transitions in middle of subtle

Since both threads are enabled, we experiment by forcing Thread 2 to continue executing. We replace ‘1’ by ‘2’ repeatedly in the trace sequence.

% ./mcmini -t0 -t' 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1,'\
'1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,'\
'2, 2, 2, 2, 2, 2,' ./subtle 1
...
34. thread 2: pthread_mutex_unlock(mut:3)
35. thread 2: pthread_mutex_lock(mut:4)
36. thread 2: pthread_cond_signal(cond:2) [Lost wakeup? (No thread waiting on cond) ]
37. thread 2: pthread_mutex_unlock(mut:4)
38. thread 2: pthread_mutex_lock(mut:3)
39. thread 2: pthread_mutex_unlock(mut:3)
40. thread 2: pthread_mutex_lock(mut:1)
41. thread 2: pthread_mutex_unlock(mut:1)
42. thread 2: pthread_mutex_lock(mut:2)
43. thread 2: pthread_cond_wait(cond:1, mut:2) (awake -> asleep)
44. thread 1: pthread_mutex_lock(mut:4)
45. thread 1: pthread_cond_wait(cond:2, mut:4) (awake -> asleep)
0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1,
END
THREAD PENDING OPERATIONS
 * thread 0: pthread_join(thr:1, _) [ Blocked ]
   thread 1: pthread_cond_wait(cond:2, mut:4) (asleep -> awake) [ Blocked ]
   thread 2: pthread_cond_wait(cond:1, mut:2) (asleep -> awake) [ Blocked ]
END
***** Model checking completed! *****
*** DEADLOCK DETECTED ***
...

This shows us the deadlock with a simple pattern: Thread 1 repeatedly executes until reaching a “Lost wakeup”, and then Thread 2 repeatedly executes until reaching “Lost wakeup”.

Next, analyzing the trace, we see that Thread 1 calls pthread_cond_signal(cond:1) and Thread 2 calls pthread_cond_wait(cond:1, mut:2). In both cases, they are executed in a critical section enforced by the mut:2 mutex.

Thus, the natural solution is to add a global variable “protected” by mut:2, which is initialized to 0, and incremented just before pthread_cond_signal(cond:1). In this case, before executing pthread_cond_wait(cond:1, mut:2), one first tests the global variable. If it is greater than 0, than we decrement, and omit calling pthread_cond_wait(cond:1, mut:2). Otherwise, we decrement after calling pthread_cond_wait(cond:1, mut:2).

Thus, the “lost wakeup” will never happen by using this global variable as the “count” of an implicit semaphore.

Similarly, we see calls to pthread_cond_signal(cond:2) and thread_cond_wait(cond:2, mut:4), where both are protected by the mut:4 mutex. Thus, we can here also create a global variable “protected” by mut:4, which acts as the count of an implicit semaphore. After making this modification, there are no more “lost wakeups”, and the deadlock no longer occurs.

TODO: Implement this solution, and demonstrate it in McMini.

Analyzing the bug for bufferSize==2 and larger

Next, we have found a bug. But for intellectual curiosity, let’s look at how the bug exhibits itself when bufferSize==2. Does the bug now require more lost wakeups, or still the same number? This will give us a good clue why the native execution (with the original ‘bufferSize==10’) tends to deadlock only after about 30 seconds.

For ‘bufferSize==2’, we see that ‘-m 28’ yields the bug of smallest depth. In this deadlock, there are 37 transitions to produce the bug. There are no additional lost wakeups. Instead, the producer now executes much longer during which time the consumer halts just before calling pthread_cond_wait. As before, the consumer finally calls pthread_cond_wait, thereby creating a deadlock.

Since bufferSize==2 might take longer, one could consider the McMini verbose mode, to directly observe the trace sequences being searched, in lexicographic order, as follows:

./mcmini -q -f -m28 -v ./subtle 2

Just for fun, one can click on the sidebar for bufferSize==5, and see a trace. By trial and error, a flag of -m117 was found to be of sufficient length to show deadlock. A total of 206 traces were examined in 5 seconds.

./mcmini -q -f -m117 ./subtle 5