  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.
