POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Wed 17 Jan 2024 17:10 - 17:30 at Kelvin Lecture - Concurrency Chair(s): Sophia Drossopoulou

While current bug detection techniques for concurrent software focus on unearthing low-level issues such as data races or deadlocks, they often fall short of discovering more intricate temporal behaviors that can arise even in the absence of such low-level issues. In this paper, we focus on the problem of dynamically analyzing concurrent software against high-level temporal specifications such as LTL. 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 in conjunction with the analysis. Towards this, we study the problem of \emph{predictive runtime monitoring}, inspired by the analogous problem of \emph{predictive data race detection} studied extensively recently. The predictive runtime monitoring question asks, given an execution $\sigma$, if it can be soundly \emph{reordered} to expose violations of a specification. In general, this problem may become easily intractable when either the specifications or the notion of reorderings used is complex.

In this paper, we focus on specifications that are given in regular languages. Our notion of reorderings is \emph{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, even in this simplistic setting, the problem of predictive admits a super-linear lower bound of $O(n^\alpha)$, where $n$ is the number of events in the execution, and $\alpha$ is a parameter describing the degree of commutativity, and typically corresponds to the number of threads in the execution. As a result, predictive runtime monitoring even in this setting is unlikely to be efficiently solvable, unlike in the non-predictive setting where the problem can be checked using a deterministic finite automaton (and thus, a constant space streaming linear time algorithm).

Towards this, we identify a sub-class of regular languages, called \emph{pattern languages} (and their extension \emph{generalized pattern languages}). Pattern languages can naturally express specific ordering of some number of (labeled) events, and have been inspired by popular empirical hypotheses underlying many concurrency bug detection approaches such as 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. We implement and evaluate our algorithm PatternTrack on benchmarks from the literature and show that it is effective in monitoring large-scale applications.

Wed 17 Jan

Displayed time zone: London change

16:50 - 18:10
ConcurrencyPOPL at Kelvin Lecture
Chair(s): Sophia Drossopoulou Imperial College London
16:50
20m
Talk
A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability
POPL
Prasad Jayanti Department of Computer Science, Dartmouth College, USA, Siddhartha Jayanti Google Research, Ugur Y. Yavuz Boston University, Lizzie Hernandez Videa Microsoft
17:10
20m
Talk
Predictive Monitoring against Pattern Regular Languages
POPL
Zhendong Ang National University of Singapore, Umang Mathur National University of Singapore
Pre-print
17:30
20m
Talk
Commutativity Simplifies Proofs of Parameterized Programs
POPL
Azadeh Farzan University of Toronto, Dominik Klumpp University of Freiburg, Andreas Podelski University of Freiburg
Pre-print
17:50
20m
Talk
Coarser Equivalences for Causal Concurrency
POPL
Azadeh Farzan University of Toronto, Umang Mathur National University of Singapore
Pre-print