关于预测性监控中读取等价参数化的研究

预测性运行时监控旨在询问并发程序的一次执行 $\sigma$ 是否可以**准确预测**是否存在一个满足属性 $\varphi$ 的重排 $\rho$。其有效性和效率依赖于两个因素：(a) 属性 $\varphi$ 的复杂度，以及 (b) 所考虑的重排的表达力。至少在简单属性如数据竞争的情况下，允许所有由**读取等价**诱导的重排都会导致预测性监控变得不可计算。在另一极端，限制为基于交换性的重排（mazurkiewicz trace 等价）则可获得简单属性的高效算法，但对于一般正则规范仍然不可计算，且预测能力有限。我们通过**参数化**来解决这一取舍问题。我们引入**分片重排**及其推广形式**$k$-分片重排**。形式上，若 $\sigma$ 可划分为 $k+1$ 个有序子序列，其拼接结果为 $\rho$，且保持程序顺序和读取约束，则 $\rho$ 为 $\sigma$ 的 $k$-分片重排。我们的研究结果有两方面：第一，$k$-分片重排形成严格递增的等级体系，随着 $k$ 的增大而收敛于读取等价。第二，对于任意固定的 $k$，基于 $k$-分片重排进行的预测性监控对于任意正则规范都 admits 一个常数空间复杂度的流式算法。这些结果将 $k$-分片重排确立为现有等价性质的一个原则性替代方案，使我们能够在表达力和计算成本之间系统性地进行权衡。