As a requirement of my Algorithmic Software Verification course, I prepared a presentation of Koushik Sen‘s paper “Race Directed Random Testing of Concurrent Programs“.

The paper is basically introducing RaceFuzzer, an algorithm for determining real races in concurrent programs. RF uses a randomized scheduler to create real race conditions using as its input a list of potential races that has been found by an ordinary race detector. For each racing pair of statements in the list, RF postpones the thread that first tries to execute such a racing statement right before the execution. The thread is put on hold until some other thread tries to do the same, in which case the race is resolved by randomly selecting one of the two racing threads, to see if any error is created by the race.

The idea is really simple, but can have spectacular results. It gives no false positives, it has very high probability of actually creating race conditions even if the race in question has very low probability in happening with a fair scheduler, it is linearly parallelizable, it can replay interleavings based only on the random seed and it is in general very lightweight.

A more extensive argumentation can of course be found in the paper itself, but if anyone wants to take a look, my presentation slides can be found here.

Also, you might want to take a look here.