Practical Concurrency Testing or: How I Learned to Stop Worrying and Love the Exponential Explosion

Concurrent programming presents a challenge to students and experts alike because of the complexity of multithreaded interactions and the difficulty of reproducing and reasoning about bugs. Stateless model checking is a testing approach which forces a program to interleave its threads in many different ways, checking for bugs each time. This technique is powerful, in principle capable of finding any nondeterministic bug in finite time, but suffers from exponential explosion as program size increases. Checking an exponential number of thread interleavings is not a practical or predictable approach for programmers to find concurrency bugs before their project deadlines.