pith. machine review for the scientific record. sign in

arxiv: 2604.06533 · v1 · submitted 2026-04-08 · 💻 cs.PL · cs.FL· cs.LO

Recognition: no theorem link

Parametrizing Reads-From Equivalence for Predictive Monitoring

Azadeh Farzan, Umang Mathur

Authors on Pith no claims yet

Pith reviewed 2026-05-10 18:32 UTC · model grok-4.3

classification 💻 cs.PL cs.FLcs.LO
keywords predictive runtime monitoringreads-from equivalenceMazurkiewicz tracessliced reorderingsstreaming algorithmsregular specificationsconcurrent program verificationreordering hierarchies
0
0 comments X

The pith

k-sliced reorderings let predictive monitoring of any regular property run in constant space for fixed k.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces sliced reorderings and their k-parameterized generalization as an intermediate notion between Mazurkiewicz trace equivalence and full reads-from equivalence. It proves that these reorderings form a strictly increasing hierarchy that converges to reads-from equivalence in the limit. For any fixed k the resulting predictive monitoring problem against a regular specification is solved by a constant-space streaming algorithm. This parametrization therefore supplies a tunable tradeoff between the limited predictive power of commutativity-based reorderings and the intractability of unrestricted reads-from reorderings.

Core claim

k-sliced reorderings form a strictly increasing hierarchy converging to reads-from equivalence as k grows, and for every fixed k predictive monitoring modulo k-sliced reorderings against any regular specification admits a constant-space streaming algorithm.

What carries the argument

k-sliced reorderings: executions partitioned into k+1 ordered subsequences whose concatenation yields the reordered trace while preserving program order and reads-from constraints.

If this is right

  • Monitoring becomes tractable for reorderings strictly more expressive than Mazurkiewicz traces.
  • A single framework lets practitioners choose k to balance predictive power against memory use.
  • The hierarchy supplies a sequence of intermediate equivalences with successively stronger predictive power.
  • Constant-space algorithms apply uniformly to every regular property once k is fixed.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same slicing idea might be adapted to obtain efficient monitors for certain non-regular properties by restricting the state space of the automaton.
  • Implementation of the streaming algorithm could be tested on existing concurrent benchmarks to measure how quickly the required k grows with realistic program size.
  • If the hierarchy converges quickly in practice, moderate fixed k values may already capture most of the predictive power of full reads-from equivalence.

Load-bearing premise

Regular specifications suffice for the constant-space streaming result and the k-sliced definition preserves exactly the constraints needed for soundness.

What would settle it

A concrete regular automaton for which, under some fixed k, every streaming algorithm for predictive monitoring requires unbounded memory would falsify the constant-space claim.

Figures

Figures reproduced from arXiv: 2604.06533 by Azadeh Farzan, Umang Mathur.

Figure 1
Figure 1. Figure 1: The wrong (a) and the right (b) slice choice for [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: ⇝∗ 𝑠 is strictly weaker than ≡rf . Definition 3.2 (Repeated sliced reordering). For concurrent program runs 𝜎 and 𝜌, we say that 𝜌 is a repeated sliced reordering of 𝜎, denoted 𝜎 ⇝∗ 𝑠 𝜌, if there exist 𝛾1,𝛾2, . . . ,𝛾𝑘 such that 𝜎 = 𝛾1⇝𝑠𝛾2⇝𝑠 . . . ⇝𝑠𝛾𝑘 = 𝜌 ⇝∗ 𝑠 is still not an equivalence relation, because it remains non-symmetric. We end this section by making two key observations about ⇝∗ 𝑠 , in the broa… view at source ↗
Figure 3
Figure 3. Figure 3: Illustrative example demonstrating the number of swaps required to witness trace equivalence. [PITH_FULL_IMAGE:figures/full_fig_p011_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Slice Reordering vs Scattered Grains. 𝑔5 are complete wrt 𝑥, i.e. they include all the read events that read from the included w(𝑥). 𝑔4 is complete wrt 𝑦. 𝑔1 and 𝑔4 are complete wrt both 𝑥 and 𝑦. 𝑔3 and 𝑔5 are contiguous, and the rest of the grains are scattered. However, no pairs of (scattered) grains commute. Remark 4.1. 𝜌 is not equivalent to 𝜎 (in fact, to anything other than itself!) using scattered g… view at source ↗
Figure 5
Figure 5. Figure 5: 𝜎 seq (left) and 𝜎 int (right) the slices and the resulting three subsequences 𝜎1, 𝜎2, 𝜎3 that witness this move. The subsequence 𝜎1 comprises the events above the innermost (green) curve, i.e., the first two events of 𝑇1 and the first 3 events of 𝑇2. The subsequence 𝜎2 comprises of next two events (⟨𝑇1, w(𝑡)⟩, ⟨𝑇1, r(𝑦)⟩) of thread 𝑇1 and the next two events (⟨𝑇2, w(𝑦)⟩, ⟨𝑇2, r(𝑥)⟩) of thread 𝑇2. while 𝜎3… view at source ↗
Figure 6
Figure 6. Figure 6: (𝑘) ⇝𝑠 is not transitive Proposition 5.3. [Lower-bound on 𝑚 for 𝑚-slice relations] For any 𝑚, there exists a pair of runs 𝜎 and 𝜌 such that 𝜎 (𝑚) ⇝𝑠 𝜌 and 𝜌 (𝑚) ⇝𝑠 𝜎 while 𝜎 (𝑚 − 1) ̸⇝ 𝑠 and 𝜌 (𝑚 − 1) ̸⇝ 𝑠 𝜎 Proof. Recall [PITH_FULL_IMAGE:figures/full_fig_p015_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Illustrating the construction of the automaton [PITH_FULL_IMAGE:figures/full_fig_p020_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Sequence of slice reorderings to transform [PITH_FULL_IMAGE:figures/full_fig_p035_8.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper introduces k-sliced reorderings (and their base sliced reorderings) as a parametrization of reads-from equivalence for predictive runtime monitoring of concurrent programs. It claims that these form a strictly increasing hierarchy converging to full reads-from equivalence as k grows, and that for any fixed k, predictive monitoring modulo k-sliced reorderings against any regular specification admits a constant-space streaming algorithm.

Significance. If the results hold, the work supplies a principled, tunable intermediate between the limited predictive power of Mazurkiewicz equivalence and the intractability of full reads-from equivalence. The hierarchy formalizes the expressiveness-tractability tradeoff, while the constant-space streaming result for fixed k and regular specifications would be a notable algorithmic contribution to runtime verification of concurrent systems.

major comments (2)
  1. Abstract: the central claim that k-sliced reorderings form a strictly increasing hierarchy converging to reads-from equivalence is asserted without any proof outline, key lemmas, or argument for strictness and convergence; this is load-bearing for the parametrization contribution.
  2. Abstract: the claim that predictive monitoring modulo k-sliced reorderings against regular specifications admits a constant-space streaming algorithm supplies no algorithm sketch, state-space construction, or complexity argument, preventing verification of the main algorithmic result.
minor comments (2)
  1. The definition of k-sliced reorderings is given only informally (partition into k+1 ordered subsequences preserving program order and reads-from); a formal definition with precise notation should appear in the main body.
  2. The abstract would benefit from a brief concrete example contrasting Mazurkiewicz, small-k sliced, and reads-from reorderings on a short execution trace.

Simulated Author's Rebuttal

2 responses · 0 unresolved

Thank you for your detailed review and valuable feedback on our manuscript. We appreciate the recognition of the potential significance of our work on parametrizing reads-from equivalence. We address each major comment point by point below. The full proofs and algorithmic constructions are detailed in the body of the paper, but we agree that adding outlines to the introduction will improve clarity and accessibility.

read point-by-point responses

  1. Referee: Abstract: the central claim that k-sliced reorderings form a strictly increasing hierarchy converging to reads-from equivalence is asserted without any proof outline, key lemmas, or argument for strictness and convergence; this is load-bearing for the parametrization contribution.

    Authors: We agree that the abstract, due to its brevity, presents the hierarchy result without a proof outline. The manuscript contains the formal definitions of sliced and k-sliced reorderings, along with theorems establishing monotonicity (every k-sliced reordering is also (k+1)-sliced), strictness (via explicit counterexample programs where increasing k enables new reorderings not possible at smaller k), and convergence (by showing that any reads-from reordering of a finite trace is k-sliced for k bounded by the number of reads-from violations or crossings in the reordering). To address the concern, we will revise the introduction to include a high-level proof sketch and reference to the key lemmas. revision: yes

  2. Referee: Abstract: the claim that predictive monitoring modulo k-sliced reorderings against regular specifications admits a constant-space streaming algorithm supplies no algorithm sketch, state-space construction, or complexity argument, preventing verification of the main algorithmic result.

    Authors: We acknowledge that the abstract summarizes the algorithmic result without a sketch. The manuscript provides the construction: for fixed k, the streaming monitor maintains a finite set of states representing the possible configurations of up to k 'slices' consistent with the observed prefix, program order, and reads-from relations, while tracking the specification automaton in parallel. The state space is finite and independent of trace length (depending only on the fixed k and the size of the regular specification), yielding constant space. We will add a concise algorithmic outline, including the state-space construction and complexity argument, to the introduction. revision: yes

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper introduces fresh definitions for sliced reorderings and k-sliced reorderings (partition into k+1 subsequences preserving program order and reads-from), then states two direct consequences: the hierarchy converges to reads-from equivalence by construction of the definition, and a constant-space streaming algorithm exists for fixed k against regular specifications. Neither claim reduces to a fitted parameter, a self-citation chain, or an input quantity renamed as output; the algorithmic result is presented as a new theorem resting on the parametrization rather than presupposing it. The derivation chain is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The central claims rest on the newly introduced definitions of sliced and k-sliced reorderings plus standard background assumptions about regular languages and concurrent execution semantics.

axioms (2)
  • standard math Regular specifications are recognized by finite automata
    Invoked when stating that monitoring works against any regular specification
  • domain assumption Program order and reads-from relations must be preserved by any valid reordering
    Stated as part of the definition of k-sliced reorderings
invented entities (1)
  • k-sliced reordering no independent evidence
    purpose: To provide an intermediate equivalence between Mazurkiewicz traces and full reads-from equivalence
    Newly defined concept that forms the hierarchy and enables the streaming algorithm

pith-pipeline@v0.9.0 · 5608 in / 1341 out tokens · 28018 ms · 2026-05-10T18:32:42.214065+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

57 extracted references · 38 canonical work pages

  1. [1]

    Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. 2017. Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction.J. ACM64, 4, Article 25 (Aug. 2017), 49 pages. doi:10.1145/3073408

    work page doi:10.1145/3073408 2017

  2. [2]

    Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, Magnus Lång, Tuan Phong Ngo, and Konstantinos Sagonas

  3. [3]

    ACM Program

    Optimal Stateless Model Checking for Reads-from Equivalence under Sequential Consistency.Proc. ACM Program. Lang.3, OOPSLA, Article 150 (oct 2019), 29 pages. doi:10.1145/3360576

    work page doi:10.1145/3360576 2019

  4. [4]

    Pratyush Agarwal, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis, and Viktor Toman. 2021. Stateless Model Checking Under a Reads-Value-From Equivalence. InComputer Aided Verification: 33rd International Conference, CA V 2021, Virtual Event, July 20–23, 2021, Proceedings, Part I. Springer-Verlag, Berlin, Heidelberg, 341–366. doi:10.1007/ 978-3-...

    2021

  5. [5]

    Zhendong Ang and Umang Mathur. 2024. Predictive Monitoring against Pattern Regular Languages.Proc. ACM Program. Lang.8, POPL, Article 73 (jan 2024). doi:10.1145/3632915 , Vol. 1, No. 1, Article . Publication date: April 2026. Parametrizing Reads-From Equivalence for Predictive Monitoring 31

    work page doi:10.1145/3632915 2024

  6. [6]

    Zhendong Ang and Umang Mathur. 2024. Predictive Monitoring with Strong Trace Prefixes. InComputer Aided Verification: 36th International Conference, CA V 2024, Montreal, QC, Canada, July 24–27, 2024, Proceedings, Part II (Montreal, QC, Canada). Springer-Verlag, Berlin, Heidelberg, 182–204. doi:10.1007/978-3-031-65630-9_9

    work page doi:10.1007/978-3-031-65630-9_9 2024

  7. [7]

    Stavros Aronis, Bengt Jonsson, Magnus Lång, and Konstantinos Sagonas. 2018. Optimal Dynamic Partial Order Reduction with Observers. InTools and Algorithms for the Construction and Analysis of Systems, Dirk Beyer and Marieke Huisman (Eds.). Springer International Publishing, Cham, 229–248

    2018

  8. [8]

    Bertoni, G

    A. Bertoni, G. Mauri, and N. Sabadini. 1989. Membership Problems for Regular and Context-Free Trace Languages.Inf. Comput.82, 2 (aug 1989), 135–150. doi:10.1016/0890-5401(89)90051-5

    work page doi:10.1016/0890-5401(89)90051-5 1989

  9. [9]

    Andreas Blass and Yuri Gurevich. 1984. Equivalence relations, invariants, and normal forms.SIAM J. Comput.13, 4 (1984), 682–689

    1984

  10. [10]

    Ahmed Bouajjani, Anca Muscholl, and Tayssir Touili. 2007. Permutation rewriting and algorithmic verification.Inf. Comput.205, 2 (Feb. 2007), 199–224. doi:10.1016/j.ic.2005.11.007

    work page doi:10.1016/j.ic.2005.11.007 2007

  11. [11]

    Sebastian Burckhardt, Pravesh Kothari, Madanlal Musuvathi, and Santosh Nagarakatte. 2010. A randomized scheduler with probabilistic guarantees of finding bugs.ACM SIGARCH Computer Architecture News38, 1 (2010), 167–178

    2010

  12. [12]

    Krishnendu Chatterjee, Andreas Pavlogiannis, and Viktor Toman. 2019. Value-centric Dynamic Partial Order Reduction. Proc. ACM Program. Lang.3, OOPSLA (2019), 124:1–124:29. doi:10.1145/3360550

    work page doi:10.1145/3360550 2019

  13. [13]

    Dmitry Chistikov, Rupak Majumdar, and Filip Niksic. 2016. Hitting Families of Schedules for Asynchronous Programs. InComputer Aided Verification, Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer International Publishing, Cham, 157–176

    2016

  14. [14]

    Tayfun Elmas, Shaz Qadeer, and Serdar Tasiran. 2007. Goldilocks: A Race and Transaction-aware Java Runtime. In Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation(San Diego, California, USA)(PLDI ’07). ACM, New York, NY, USA, 245–255. doi:10.1145/1250734.1250762

    work page doi:10.1145/1250734.1250762 2007

  15. [15]

    Madhusudan

    Azadeh Farzan and P. Madhusudan. 2006. Causal Atomicity. InComputer Aided Verification, Thomas Ball and Robert B. Jones (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 315–328

    2006

  16. [16]

    Madhusudan

    Azadeh Farzan and P. Madhusudan. 2008. Monitoring Atomicity in Concurrent Programs. InComputer Aided Verification, Aarti Gupta and Sharad Malik (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 52–65

    2008

  17. [17]

    Madhusudan, Niloofar Razavi, and Francesco Sorrentino

    Azadeh Farzan, P. Madhusudan, Niloofar Razavi, and Francesco Sorrentino. 2012. Predicting Null-pointer Dereferences in Concurrent Programs. InProceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering(Cary, North Carolina)(FSE ’12). ACM, New York, NY, USA, Article 47, 11 pages. doi:10.1145/ 2393596.2393651

    work page arXiv 2012

  18. [18]

    Azadeh Farzan and Umang Mathur. 2024. Coarser Equivalences for Causal Concurrency.Proc. ACM Program. Lang.8, POPL, Article 31 (Jan. 2024), 31 pages. doi:10.1145/3632873

    work page doi:10.1145/3632873 2024

  19. [19]

    Cormac Flanagan and Patrice Godefroid. 2005. Dynamic Partial-Order Reduction for Model Checking Software. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(Long Beach, California, USA)(POPL ’05). Association for Computing Machinery, New York, NY, USA, 110–121. doi:10.1145/1040305. 1040315

    work page doi:10.1145/1040305 2005

  20. [20]

    Kaan Genç, Jake Roemer, Yufan Xu, and Michael D. Bond. 2019. Dependence-aware, unbounded sound predictive race detection.Proc. ACM Program. Lang.3, OOPSLA, Article 179 (Oct. 2019), 30 pages. doi:10.1145/3360605

    work page doi:10.1145/3360605 2019

  21. [21]

    Gibbons and Ephraim Korach

    Phillip B. Gibbons and Ephraim Korach. 1994. On Testing Cache-Coherent Shared Memories. InProceedings of the Sixth Annual ACM Symposium on Parallel Algorithms and Architectures(Cape May, New Jersey, USA)(SPAA ’94). Association for Computing Machinery, New York, NY, USA, 177–188. doi:10.1145/181014.181328

    work page doi:10.1145/181014.181328 1994

  22. [22]

    Gibbons and Ephraim Korach

    Phillip B. Gibbons and Ephraim Korach. 1997. Testing Shared Memories.SIAM J. Comput.26, 4 (1997), 1208–1244. doi:10.1137/S0097539794279614 arXiv:https://doi.org/10.1137/S0097539794279614

    work page doi:10.1137/s0097539794279614 1997

  23. [23]

    Antonio Cano Gómez, Giovanna Guaiana, and Jean-Éric Pin. 2008. When Does Partial Commutative Closure Preserve Regularity?. InAutomata, Languages and Programming, Luca Aceto, Ivan Damgård, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir, and Igor Walukiewicz (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 209–220

    2008

  24. [24]

    Jeff Huang. 2018. UFO: Predictive Concurrency Use-after-Free Detection. InProceedings of the 40th International Conference on Software Engineering(Gothenburg, Sweden)(ICSE ’18). Association for Computing Machinery, New York, NY, USA, 609–619. doi:10.1145/3180155.3180225

    work page doi:10.1145/3180155.3180225 2018

  25. [25]

    Jeff Huang, Qingzhou Luo, and Grigore Rosu. 2015. GPredict: Generic Predictive Concurrency Analysis. InProceedings of the 37th International Conference on Software Engineering - Volume 1(Florence, Italy)(ICSE ’15). IEEE Press, 847–857

    2015

  26. [26]

    Jeff Huang, Patrick O’Neil Meredith, and Grigore Rosu. 2014. Maximal Sound Predictive Race Detection with Control Flow Abstraction. InProceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Imple- mentation(Edinburgh, United Kingdom)(PLDI ’14). ACM, New York, NY, USA, 337–348. doi:10.1145/2594291.2594315

    work page doi:10.1145/2594291.2594315 2014

  27. [27]

    Christian Gram Kalhauge and Jens Palsberg. 2018. Sound Deadlock Prediction.Proc. ACM Program. Lang.2, OOPSLA, Article 146 (Oct. 2018), 29 pages. doi:10.1145/3276516 , Vol. 1, No. 1, Article . Publication date: April 2026. 32 Azadeh Farzan and Umang Mathur

    work page doi:10.1145/3276516 2018

  28. [28]

    Dileep Kini, Umang Mathur, and Mahesh Viswanathan. 2017. Dynamic Race Prediction in Linear Time. InProceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation(Barcelona, Spain)(PLDI 2017). ACM, New York, NY, USA, 157–170. doi:10.1145/3062341.3062374

    work page doi:10.1145/3062341.3062374 2017

  29. [29]

    Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, and Viktor Vafeiadis. 2022. Truly Stateless, Optimal Dynamic Partial Order Reduction.Proc. ACM Program. Lang.6, POPL, Article 49 (jan 2022), 28 pages. doi:10.1145/3498711

    work page doi:10.1145/3498711 2022

  30. [30]

    Rucha Kulkarni, Umang Mathur, and Andreas Pavlogiannis. 2021. Dynamic Data-Race Detection Through the Fine- Grained Lens. In32nd International Conference on Concurrency Theory (CONCUR 2021) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 203), Serge Haddad and Daniele Varacca (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dags...

    work page doi:10.4230/lipics.concur.2021.16 2021

  31. [31]

    Martin Leucker and Christian Schallhart. 2009. A brief account of runtime verification.The Journal of Logic and Algebraic Programming78, 5 (2009), 293–303. doi:10.1016/j.jlap.2008.08.004 The 1st Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS’07)

    work page doi:10.1016/j.jlap.2008.08.004 2009

  32. [32]

    Roy Margalit, Michalis Kokologiannakis, Shachar Itzhaky, and Ori Lahav. 2025. Dynamic Robustness Verification against Weak Memory.Proc. ACM Program. Lang.9, PLDI, Article 174 (June 2025), 24 pages. doi:10.1145/3729277

    work page doi:10.1145/3729277 2025

  33. [33]

    Iason Marmanis, Michalis Kokologiannakis, and Viktor Vafeiadis. 2023. Reconciling Preemption Bounding with DPOR. InTools and Algorithms for the Construction and Analysis of Systems, Sriram Sankaranarayanan and Natasha Sharygina (Eds.). Springer Nature Switzerland, Cham, 85–104

    2023

  34. [34]

    Umang Mathur, Dileep Kini, and Mahesh Viswanathan. 2018. What Happens-after the First Race? Enhancing the Predictive Power of Happens-before Based Dynamic Race Detection.Proc. ACM Program. Lang.2, OOPSLA, Article 145 (Oct. 2018), 29 pages. doi:10.1145/3276515

    work page doi:10.1145/3276515 2018

  35. [35]

    Umang Mathur, Andreas Pavlogiannis, and Mahesh Viswanathan. 2020. The Complexity of Dynamic Data Race Prediction. InProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science(Saarbrücken, Germany) (LICS ’20). Association for Computing Machinery, New York, NY, USA, 713–727. doi:10.1145/3373718.3394783

    work page doi:10.1145/3373718.3394783 2020

  36. [36]

    Umang Mathur, Andreas Pavlogiannis, and Mahesh Viswanathan. 2021. Optimal Prediction of Synchronization- Preserving Races.Proc. ACM Program. Lang.5, POPL, Article 36 (Jan. 2021), 29 pages. doi:10.1145/3434317

    work page doi:10.1145/3434317 2021

  37. [37]

    Umang Mathur and Mahesh Viswanathan. 2020. Atomicity Checking in Linear Time Using Vector Clocks. InProceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems(Lausanne, Switzerland)(ASPLOS ’20). Association for Computing Machinery, New York, NY, USA, 183–199. doi:10.1145/3373376.3378475

    work page doi:10.1145/3373376.3378475 2020

  38. [38]

    A Mazurkiewicz. 1987. Trace Theory. InAdvances in Petri Nets 1986, Part II on Petri Nets: Applications and Relationships to Other Models of Concurrency. Springer-Verlag New York, Inc., 279–324

    1987

  39. [39]

    Edward Ochmański. 1985. Regular behaviour of concurrent systems.Bull. EATCS27 (1985), 56–67

    1985

  40. [40]

    Burcu Kulahcioglu Ozkan, Rupak Majumdar, and Simin Oraee. 2019. Trace aware random testing for distributed systems.Proceedings of the ACM on Programming Languages3, OOPSLA (2019), 1–29

    2019

  41. [41]

    Papadimitriou

    Christos H. Papadimitriou. 1979. The serializability of concurrent database updates.J. ACM26, 4 (1979), 631–653. doi:10.1145/322154.322158

    work page doi:10.1145/322154.322158 1979

  42. [42]

    Andreas Pavlogiannis. 2019. Fast, Sound, and Effectively Complete Dynamic Race Prediction.Proc. ACM Program. Lang.4, POPL, Article 17 (Dec. 2019), 29 pages. doi:10.1145/3371085

    work page doi:10.1145/3371085 2019

  43. [43]

    Shaz Qadeer and Jakob Rehof. 2005. Context-Bounded Model Checking of Concurrent Software. InTools and Algorithms for the Construction and Analysis of Systems, Nicolas Halbwachs and Lenore D. Zuck (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 93–107

    2005

  44. [44]

    Jake Roemer, Kaan Genç, and Michael D. Bond. 2018. High-coverage, Unbounded Sound Predictive Race Detection. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation(Philadelphia, PA, USA)(PLDI 2018). ACM, New York, NY, USA, 374–389. doi:10.1145/3192366.3192385

    work page doi:10.1145/3192366.3192385 2018

  45. [45]

    Mahmoud Said, Chao Wang, Zijiang Yang, and Karem Sakallah. 2011. Generating Data Race Witnesses by an SMT-based Analysis. InProceedings of the Third International Conference on NASA Formal Methods(Pasadena, CA)(NFM’11). Springer-Verlag, Berlin, Heidelberg, 313–327. http://dl.acm.org/citation.cfm?id=1986308.1986334

    work page arXiv 2011

  46. [46]

    Jacques Sakarovitch. 1992. The “last” decision problem for rational trace languages. InLATIN ’92, Imre Simon (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 460–473

    1992

  47. [47]

    Koushik Sen. 2007. Effective random testing of concurrent programs. InProceedings of the 22nd IEEE/ACM international conference on Automated software engineering. 323–332

    2007

  48. [48]

    Traian Florin ŞerbănuŢă, Feng Chen, and Grigore Roşu. 2013. Maximal Causal Models for Sequentially Consistent Systems. InRuntime Verification, Shaz Qadeer and Serdar Tasiran (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 136–150

    2013

  49. [49]

    Zheng Shi, Umang Mathur, and Andreas Pavlogiannis. 2024. Optimistic Prediction of Synchronization-Reversal Data Races. InProceedings of the IEEE/ACM 46th International Conference on Software Engineering(Lisbon, Portugal)(ICSE ’24). Association for Computing Machinery, New York, NY, USA, Article 134, 13 pages. doi:10.1145/3597503.3639099 , Vol. 1, No. 1, A...

    work page doi:10.1145/3597503.3639099 2024

  50. [50]

    Yannis Smaragdakis, Jacob Evans, Caitlin Sadowski, Jaeheon Yi, and Cormac Flanagan. 2012. Sound Predictive Race Detection in Polynomial Time. InProceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(Philadelphia, PA, USA)(POPL ’12). ACM, New York, NY, USA, 387–400. doi:10.1145/2103656. 2103702

    work page doi:10.1145/2103656 2012

  51. [51]

    Howard Straubing. 1981. A generalization of the Schützenberger product of finite monoids.Theoretical Computer Science13, 2 (1981), 137–150. doi:10.1016/0304-3975(81)90036-0

    work page doi:10.1016/0304-3975(81)90036-0 1981

  52. [52]

    Howard Straubing. 1985. Finite semigroup varieties of the form V*D.Journal of Pure and Applied Algebra36 (1985), 53–94. doi:10.1016/0022-4049(85)90062-3

    work page doi:10.1016/0022-4049(85)90062-3 1985

  53. [53]

    Denis Therien. 1981. Classification of finite monoids: the language approach.Theoretical Computer Science14, 2 (1981), 195–208. doi:10.1016/0304-3975(81)90057-8

    work page doi:10.1016/0304-3975(81)90057-8 1981

  54. [54]

    Hünkar Can Tunç, Umang Mathur, Andreas Pavlogiannis, and Mahesh Viswanathan. 2023. Sound Dynamic Deadlock Prediction in Linear Time.Proc. ACM Program. Lang.7, PLDI, Article 177 (jun 2023), 26 pages. doi:10.1145/3591291

    work page doi:10.1145/3591291 2023

  55. [55]

    Moshe Y. Vardi. 1989. A note on the reduction of two-way automata to one-way automata.Inform. Process. Lett.30, 5 (1989), 261–264. doi:10.1016/0020-0190(89)90205-6

    work page doi:10.1016/0020-0190(89)90205-6 1989

  56. [56]

    Duck, Umang Mathur, and Abhik Roychoudhury

    Dylan Wolff, Zheng Shi, Gregory J. Duck, Umang Mathur, and Abhik Roychoudhury. 2024. Greybox Fuzzing for Concurrency Testing. InProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2(La Jolla, CA, USA)(ASPLOS ’24). Association for Computing Machinery, New York, NY, USA, 482–4...

    work page doi:10.1145/3620665.3640389 2024

  57. [57]

    DEb13GLAjbhaXxpL0dum27MQxLA=

    Xinhao Yuan, Junfeng Yang, and Ronghui Gu. 2018. Partial order aware concurrency sampling. InComputer Aided Verification: 30th International Conference, CA V 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II 30. Springer, 317–335. , Vol. 1, No. 1, Article . Publication date: April 2026. 34 ...

    2018