Coarser Equivalences for Causal Concurrency

TL;DR

This paper introduces grain equivalence, a new relaxed form of trace equivalence for concurrent programs, enabling constant space algorithms for causal concurrency detection, unlike previous relaxations that are computationally infeasible.

Contribution

It proposes grain equivalence, a novel relaxation of trace equivalence, and demonstrates its efficiency with constant space algorithms for causal concurrency analysis.

Findings

Linear space lower bound for checking causal concurrency in streaming setting

Constant space algorithms for grain equivalence in contiguous and non-contiguous cases

Grain equivalence is more relaxed than trace equivalence and computationally efficient

Abstract

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.