Developing correct, scalable and efficient concurrent programs is a complex and difficult task, due to the large number of possible concurrent executions that need to be taken into account. Modern multi-core processors with weak memory models and lock-free algorithms make this task even more difficult, as they introduce additional executions that confound the developers' reasoning. Because of these complex interactions, concurrent programs often contain bugs that are difficult to find, reproduce, and fix. Stress testing is known to be very ineffective in detecting rare concurrency bugs as all possible executions of the programs have to be explored explicitly. Consequently, testing by itself is often inadequate for concurrent programs and ne...