Commutativity in Automated Verification

Trace theory (formulated by Mazurkiewicz in 1987) is a framework for formalizing equivalence relations for concurrent program runs based on a commutativity relation over the set of atomic steps taken by individual program threads. It has been implicitly or explicitly used in a broad set of program analysis techniques, such as predictive testing for atomicity or data race violations, static and dynamic partial order reduction in model checking (particularly stateless model checking), and reasoning about distributed programs. In this paper, we introduce a different line of work that uses traces for the purpose of proof simplification for a broad set of automated verification goals. The long term thesis of this line of work has been that by taking advantage of commutativity, one can discover a substantially simpler verification task to replace the original one, and succeed at it despite the inevitability of the failure of the original one. The idea is to verify a different program in place of the original one and use commutativity as a way of soundly carrying the verification results over to the original one. We discuss hypersafety verification of sequential and concurrent programs, and safety and liveness verification of concurrent and distributed programs. We show how commutativity can be incorporated into a new verification algorithm which enumerates infinitely many possibilities for alternative programs to be verified instead of the original one. We conclude with an overview of some open research questions in this area.