Parametrizing Reads-From Equivalence for Predictive Monitoring

TL;DR

This paper introduces a parametrized framework for predictive runtime monitoring that balances expressive power and computational efficiency by using $k$-sliced reorderings, generalizing existing equivalences.

Contribution

It defines $k$-sliced reorderings, forming a hierarchy that converges to reads-from equivalence, and provides a constant-space streaming algorithm for monitoring with these reorderings.

Findings

$k$-sliced reorderings form a hierarchy converging to reads-from equivalence.

Predictive monitoring with $k$-sliced reorderings admits a constant-space streaming algorithm.

The framework enables systematic tradeoff between expressiveness and computational cost.

Abstract

Predictive runtime monitoring asks whether an execution $\sigma$ of a concurrent program can be used to \emph{soundly predict} the existence of a reordering $\rho$ of $\sigma$ 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, $\rho$ is a $k$-sliced reordering of $\sigma$ if $\sigma$ can be partitioned into $k+1$ ordered subsequences whose concatenation yields $\rho$, 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.