一句话：提出比迹等价更粗的 grain 等价，并给出判定因果并发性的常数空间流式算法。
迹理论基于原子步骤间的交换性为并发程序运行定义等价关系，其等价类越大，对验证与测试越有利。本文研究迹等价的松弛。作者首先证明，保留各线程步骤顺序以及读所观察写操作的最大合适松弛，在流式设置下判定任意两步是因果并发还是因果有序，需要线性空间下界；而迹等价可用常数空间判定。随后提出 grain 等价：在标准原子步骤交换性之外，还利用由原子步骤序列构成的 grain 的交换性，因此严格粗于迹等价，但仍可用常数空间判定同一问题。文章区分 grain 为连续子词与非连续子词两种情形，分别给出因果并发的精确定义，并证明二者均可在常数空间内判定。
Trace theory (formulated by Mazurkiewicz in 1987) 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. It is well-understood that the larger the equivalence classes are, the more benefits they would bring to the algorithms and applications that use them. In this paper, 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. Specifically, 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.