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.

翻译：预测运行时监控询问：能否利用并发程序的执行迹σ，*可可靠地预测*是否存在满足性质φ的σ的重排序ρ。其有效性与效率取决于两个因素：(a) φ的复杂度，以及(b)所考虑重排序的表达能力。极端情况下，允许由*读-源自等价关系*导出的所有重排序会使预测监控难以处理，即使对于数据竞争等简单性质也是如此。另一极端情况下，限制为基于交换性的重排序（Mazurkiewicz迹等价关系）虽能为简单性质提供高效算法，但对于一般正则规约仍难以处理，且预测能力有限。我们通过*参数化*来应对这一权衡。我们引入*切片重排序*及其推广形式——*k-切片重排序*。直观而言，若可将σ划分为k+1个有序子序列，且这些子序列拼接后得到ρ，同时保持程序顺序和读-源自约束，则称ρ为σ的k-切片重排序。我们的成果有两方面：第一，k-切片重排序构成严格递增的层级结构，随k增大逐渐收敛至读-源自等价关系；第二，对于任意固定k，基于k-切片重排序的预测监控（针对任意正则规约）可设计常量空间流式算法。这些成果共同确立了k-切片重排序作为现有等价关系的系统性替代方案，构建了一个统一的参数化框架，可在其中系统性地权衡表达能力与计算成本。