A Domain Specific Language for Testing Concurrent Programs

We present Concurrit, a novel testing technique and domain-specific language (DSL) for unit and system testing of concurrent programs. Using Concurrit, a programmer can control and guide the thread schedule of the software-under-test (SUT) in both a formal and concise way to examine only the intended interleavings of threads. Our DSL provides constructs to express nondeterministic choice, with which one can specify a set of thread schedules to be systematically enumerated similarly to model checking. In contrast with the traditional notion of model checking, we find some uncontrolled nondeterminism natural and unavoidable in real software. In our approach, the programmer can write a Concurrit test that describes the controlled-nondeterminism for part of the thread schedule, leaving the rest of the schedule unspecified. We call the result tolerant model checking, where a search of thread schedules in the presence of uncontrolled nondeterminism can still be systematic and exhaustive with respect to the Concurrit test. We applied our testing technique in both unit and system testing of a collection of benchmarks including the Mozilla’s SpiderMonkey JavaScript engine, Memcached, the Apache HTTP server, and MySQL. We were able to use Concurrit to write concise tests to reproduce concurrency bugs in these benchmarks.