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.

翻译：迹理论（由Mazurkiewicz于1987年提出）是一个基于单个程序线程执行的原子步骤集合上的交换关系，为并发程序运行设计等价关系的框架。它已被广泛应用于各种程序验证和测试技术中，具有简洁优雅的特性，并能生成在许多不同场景中广泛适用的高效算法。众所周知，等价类越大，使用它们的算法获得的收益就越多。本文研究了迹等价的松弛形式，旨在保持其算法优势。我们证明，在保持每个线程执行步骤顺序以及每个读操作观察到的写操作不变的前提下，迹等价的极大合适松弛——一种等价关系——无法产生高效算法。具体而言，我们证明了判断并发程序运行中的两个任意步骤是因果并发（即可在等价运行中重排序）还是因果有序（即所有等价运行中始终以相同顺序出现）的问题，具有线性空间下界。而对于迹等价，同一问题可在常数空间内判定。