Trace theory is a principled framework for defining equivalence relations for concurrent program runs based on a commutativity relation over the set of atomic steps taken by individual program threads. Its simplicity, elegance, and algorithmic efficiency makes it useful in many different contexts including program verification and testing. We study relaxations of trace equivalence with the goal of maintaining its algorithmic advantages. We first 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. We prove a linear space lower bound for the problem of checking, in a streaming setting, 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. Next, we propose a new commutativity-based notion of equivalence called grain equivalence that is strictly more relaxed than trace equivalence, and yet yields a constant space algorithm for the same problem. This notion of equivalence uses commutativity of grains, which are sequences of atomic steps, in addition to the standard commutativity from trace theory. We study the two distinct cases when the grains are contiguous subwords of the input program run and when they are not, formulate the precise definition of causal concurrency in each case, and show that they can be decided in constant space, despite being strict relaxations of the notion of causal concurrency based on trace equivalence.

翻译：迹理论是一种基于程序各线程原子步之间的交换关系来定义并发程序运行间等价关系的形式化框架。其简洁性、优雅性和算法高效性使其广泛应用于程序验证与测试等领域。本文研究迹等价的松弛化形式，旨在保留其算法优势。首先证明迹等价的最大合理松弛——即保持各线程步骤顺序及读操作所观测写操作关系的等价关系——无法产生高效算法。我们证明在流式场景下，判断并发程序运行中任意两步骤是因果并发（即在等价运行中可重排序）还是因果顺序（即在所有等价运行中顺序固定）需要线性空间下界，而相同问题在迹等价中仅需常数空间即可判定。为此，我们提出一种新的基于交换关系的等价概念——粒度等价，该等价关系比迹等价更松弛，却能为相同问题提供常数空间算法。该等价概念除利用迹理论中的标准交换关系外，还引入了粒度（原子步序列）的交换性。我们分别研究了粒度构成输入程序运行的连续子串及非连续子串两种情形，给出了各情形下因果并发的精确定义，并证明尽管这些定义是迹等价基础上因果并发概念的严格松弛化，仍可在常数空间内判定。