Systematic Concurrency Testing with Maximal Causality

We propose the first systematic concurrent program testing approach that is able to cover the entire scheduling space with a provably minimal number of test runs. Each run corresponds to a distinct maximal causal model extracted from a given execution trace, which captures the largest possible set of causally equivalent legal executions. The maximal causal models can be represented using first-order logic constraints, and testing all the executions comprised by a maximal causal model reduces to offline constraint solving. Based on the same constraint model, we also develop a schedule generation algorithm that iteratively generates new casually different schedules. The core idea is to systematically force previous read operations to read different values, thus enumerating all the causal models. We have implemented our approach in an explicit stateless model checker, and our eval- uation showed that our technique is able to 1) find concurrency bugs faster; 2) finish state space exploration with much fewer schedules than previous techniques.