Detect races in a Makefile-based project

This tutorial shows how to use Coderrect to detect races in a Makefile-based project using pbzip2-0.9.4 as the example. pbzip2 is a parallel implementation of the bzip2 file compressor, and it contains a known race condition in version 0.9.4.

git clone https://github.com/sctbenchmarks/sctbenchmarks.git
cd sctbenchmarks/1CB-0-2/pbzip2-0.9.4/bzip2-1.0.6
make clean
make
cd ..
cd pbzip2-0.9.4
make clean
coderrect make

Prerequisites

This tutorial assumes you have successfully installed the Coderrect software following the quick start.


Background

In pbzip2, the program will spawn consumer threads that (de)compress the input file and spawn an output thread that writes data to the output file. However, the main thread only joins the output thread but does not join the consumer threads. So there is an order violation bug between the time when the main thread is destroying resources and the time when consumer threads are using the resources.

An interleaving that triggers the error looks like:

void main(...) { 
  ...
  for (i=0; i < numCPU; i++) {              
    ret = pthread_create(..., consumer, 
                              fifo);  
    ...             
  }
  ret = pthread_create(..., fileWriter, 
                            OutFilename);
  ...
  // start reading in data
  producer(..., fifo);
  ...
  // wait until exit of thread
  pthread_join(output, NULL);
  ...
  fifo->empty = 1;
  ...
  // reclaim memory
  queueDelete(fifo);
  fifo = NULL;



}
void *decompress_consumer(void *q) {
  ...
  for (;;) {


















    pthread_mutex_lock(fifo->mut);
    ...
  }
}

Since queueDelete will release the fifo queue used by consumer threads, the access on fifo->mut will result in a segmentation fault.


Detect the race using Coderrect

Make sure the code can be compiled

cd sctbenchmarks/1CB-0-2/pbzip2-0.9.4/pbzip2-0.9.4
make

You should see a pbzip2 executable under the same folder.


Run Coderrect

make clean 
coderrect -t -o report make

NOTE: The make clean command is to ensure there is no pre-built binaries so that Coderrect is able to analyze every piece of source code in the project.

The coderrect -t -o report make command will compile and analyze the problem, the reported races is stored under ./report directory as specified by -o option.

-t switch is used to generate a quick summary report in terminal.


Interpret the Results

The coderrect tool reports a quick summary of the most interesting races directly in the terminal for quick viewing. The tool also generates a more comprehensive report that can be viewed in the browser.

Terminal Report

The terminal races reports looks like following:

==== Found a race between: 
line 1048, column 3 in pbzip2.cpp  AND  line 553, column 28 in pbzip2.cpp
Shared variable: 
 at line 991 of pbzip2.cpp
 991|	q = new queue;
Thread 1: 
pbzip2.cpp@1048:3
Code snippet: 
 1046|		pthread_mutex_destroy(q->mut);
 1047|		delete q->mut;
>1048|		q->mut = NULL;
 1049|	}
 1050|
>>>Stack Trace:
>>>main
>>>  queueDelete(queue*) [pbzip2.cpp:1912]
Thread 2: 
pbzip2.cpp@553:28
Code snippet: 
 551|	for (;;)
 552|	{
>553|		pthread_mutex_lock(fifo->mut);
 554|		while (fifo->empty)
 555|		{
>>>Stack Trace:
>>>pthread_create [pbzip2.cpp:1818]
>>>  consumer_decompress(void*) [pbzip2.cpp:1818]

Each reported race starts with a summary of where the race was found.

==== Found a race between: 
line 1048, column 3 in pbzip2.cpp  AND  line 553, column 28 in pbzip2.cpp

Next the report shows the name and location of the variable on which the race occurs.

Shared variable: 
 at line 991 of pbzip2.cpp
 991|	q = new queue;

This shows that the race occurs on the variable queue allocated at line 991.

Next the tool reports information about the two unsynchronized accesses to queue.
For each of the two accesses a location, code snippet, and stack trace is shown.

The location shows the file, line, and column of the access.

Thread 1: 
pbzip2.cpp@1048:3

So the above access occurs in pbzip2.cpp at line 1048 column 3.
The report also shows a preview of the file at that location.

Code snippet: 
 1046|		pthread_mutex_destroy(q->mut);
 1047|		delete q->mut;
>1048|		q->mut = NULL;
 1049|	}
 1050|

The code snippet shows that this access is a write to q->mut (set it to NULL).

HTML Report

The terminal is great to get a quick idea about what races are reported, but the full report can be viewed in a browser.