In this paper, we focus on the problem of dynamically analysing concurrent software against high-level temporal specifications. Existing techniques for runtime monitoring against such specifications are primarily designed for sequential software and remain inadequate in the presence of concurrency -- violations may be observed only in intricate thread interleavings, requiring many re-runs of the underlying software. Towards this, we study the problem of predictive runtime monitoring, inspired by the analogous problem of predictive data race detection studied extensively recently. The predictive runtime monitoring question asks, given an execution $σ$, if it can be soundly reordered to expose violations of a specification. In this paper, we focus on specifications that are given in regular languages. Our notion of reorderings is trace equivalence, where an execution is considered a reordering of another if it can be obtained from the latter by successively commuting adjacent independent actions. We first show that the problem of predictive admits a super-linear lower bound of $O(n^α)$, where $n$ is the number of events in the execution, and $α$ is a parameter describing the degree of commutativity. As a result, predictive runtime monitoring even in this setting is unlikely to be efficiently solvable. Towards this, we identify a sub-class of regular languages, called pattern languages (and their extension generalized pattern languages). Pattern languages can naturally express specific ordering of some number of (labelled) events, and have been inspired by popular empirical hypotheses, the `small bug depth' hypothesis. More importantly, we show that for pattern (and generalized pattern) languages, the predictive monitoring problem can be solved using a constant-space streaming linear-time algorithm.

翻译：本文聚焦于针对高级时序规约的动态并发软件分析问题。现有的运行时监控技术主要针对顺序软件设计，在并发场景下仍存在不足——违规行为可能仅在复杂的线程交错中显现，需要对底层软件进行多次重新运行。为此，我们研究预测性运行时监控问题，其灵感来源于近期被广泛研究的预测性数据竞争检测类比问题。预测性运行时监控的核心问题是：给定执行轨迹$σ$，能否通过可验证的重排序揭示规约违规。本文重点关注以正则语言描述的规约。我们采用迹等价作为重排序准则，即若某执行轨迹可通过连续交换相邻独立操作从另一轨迹获得，则视为其重排序版本。我们首先证明预测性监控问题存在$O(n^α)$的超线性下界，其中$n$是执行事件数，$α$是描述交换性程度的参数。这表明即使在此设定下，预测性运行时监控也难以高效求解。为此，我们识别出正则语言的一个子类——模式语言（及其扩展广义模式语言）。模式语言可自然表达若干（带标签）事件的特定顺序，其设计灵感来源于"小缺陷深度"这一经典实证假设。更重要的是，我们证明对于模式语言（及广义模式语言），预测性监控问题可通过恒定空间流式线性时间算法求解。