Search papers, labs, and topics across Lattice.
This paper introduces $k$-sliced reorderings, a novel parametrization of reads-from equivalence for predictive runtime monitoring of concurrent programs. $k$-sliced reorderings offer a tunable trade-off between the expressiveness of allowed reorderings and the computational cost of predictive monitoring. The authors demonstrate that $k$-sliced reorderings form a hierarchy converging to full reads-from equivalence and that predictive monitoring with fixed $k$ admits a constant-space streaming algorithm for regular specifications.
Unlock a sweet spot in predictive monitoring: $k$-sliced reorderings let you smoothly dial between expressiveness and cost when predicting concurrency issues.
Predictive runtime monitoring asks whether an execution $蟽$ of a concurrent program can be used to \emph{soundly predict} the existence of a reordering $蟻$ of $蟽$ that satisfies a property $\varphi$. Its effectiveness and efficiency depend on two factors: (a) the complexity of $\varphi$, and (b) the expressive power of the reorderings considered. At one extreme, allowing all reorderings induced by \emph{reads-from equivalence} makes predictive monitoring intractable, even for simple properties such as data races. At the other extreme, restricting to commutativity-based reorderings (Mazurkiewicz trace equivalence) yields efficient algorithms for simple properties, but remains intractable for general regular specifications and offers limited predictive power. We address this tradeoff via \emph{parametrization}. We introduce \emph{sliced reorderings} and their generalization, \emph{$k$-sliced reorderings}. Informally, $蟻$ is a $k$-sliced reordering of $蟽$ if $蟽$ can be partitioned into $k+1$ ordered subsequences whose concatenation yields $蟻$, while preserving program order and reads-from constraints. Our results are twofold. First, $k$-sliced reorderings form a strictly increasing hierarchy that converges to reads-from equivalence as $k$ grows. Second, for any fixed $k$, predictive monitoring modulo $k$-sliced reorderings against any regular specification admits a constant-space streaming algorithm. Together, these results establish $k$-sliced reorderings as a principled alternative to existing equivalences, enabling a uniform parametrized framework where expressive power can be systematically traded off against computational cost.