Coarser Equivalences for Concurrent Program Runs

Trace theory (formulated by Mazurkiewicz in 1987) is a framework for designing 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 widely used in a variety of program verification and testing techniques. It is simple and elegant, and it yields efficient algorithms that are broadly useful in many different contexts. It is well-understood that the larger the equivalence classes are, the more benefits they would bring to the algorithms that use them. In this paper, we study relaxations of trace equivalence with the goal of maintaining its algorithmic advantages. We prove that the largest appropriate relaxation of trace equivalence, an equivalence relation that preserves the order of steps taken by each thread and what write operation each read operation observes, does not yield efficient algorithms. Specifically, we prove a linear space lower bound for the problem of checking if two arbitrary steps of a concurrent program run are causally concurrent (i.e. they can be reordered in an equivalent run) or causally ordered (i.e. they always appear in the same order in all equivalent runs). The same problem can be decided in constant space for trace equivalence.