Testing concurrent programs on relaxed memory models
Jacob S. Burnim, Koushik Sen, Christos L. Stergiou · 2011
High-performance concurrent libraries, such as lock-free data structures and custom synchronization primitives, are notoriously difficult to write correctly. Such code is often implemented without locks, instead using plain loads and stores and low-level operations like atomic compare-and-swaps and explicit memory fences. Such code must run correctly despite the relaxed memory model of the underlying compiler, virtual machine, and/or hardware. These memory models may reorder the reads and writes issued by a thread, greatly complicating parallel reasoning. We propose RELAXER, a combination of predictive dynamic analysis and software testing, to help programmers write correct, highly-concurrent programs. Our technique works in two phases. First, RELAXER examines a sequentially-consistent run of a program under test and dynamically detects potential data races. These races are used to predict possible violations of sequential consistency under alternate executions on a relaxed memory model. In the second phase, RELAXER re-executes the program with a biased random scheduler and with a conservative simulation of a relaxed memory model in order to create with high probability a predicted sequential consistency violation. These executions can be used to test whether or not a program works as expected when the underlying memory model is not sequentially consistent. We have implemented RELAXER for C and have evaluated it on several synchronization algorithms, concurrent data structures, and parallel applications. RELAXER generates many executions of these benchmarks with violations of sequential consistency, highlighting a number of bugs under relaxed memory models.