pith. sign in

arxiv: 2509.05586 · v3 · submitted 2025-09-06 · 💻 cs.PL · cs.CC

Fixed Parameter Tractable Linearizability Monitoring

Lee Zheng Han , Umang Mathur This is my paper

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

classification 💻 cs.PL cs.CC
keywords linearizabilityfixed-parameter tractabilitylanguage reachabilityconcurrent data structuresmonitoring algorithmsparameterized complexityhistory graphs
0
0 comments X

The pith

Linearizability monitoring for stacks, queues, and maps is fixed-parameter tractable in the number of processes.

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

The paper establishes that checking whether a concurrent history of common data structures is linearizable can be solved efficiently when parameterized by the number of processes. It reduces the monitoring task to a language reachability query on a graph built from the history, where the target language is fixed and captures the sequential specification of the data structure. This produces an algorithm whose runtime is exponential only in the process count and polynomial in the history length. A sympathetic reader would care because linearizability is a standard correctness criterion for concurrent objects, yet the problem is NP-hard in general and prior tractable cases were limited to special history shapes.

Core claim

For data structures whose sequential specifications are captured by fixed languages L, linearizability monitoring reduces to language reachability on the graphs induced by concurrent histories; when reachability on those graphs is efficiently solvable, the monitoring problem is fixed-parameter tractable parameterized by the number of processes k, with an algorithm running in O(c^k · poly(n)) time.

What carries the argument

Reduction of linearizability monitoring to language reachability on graphs derived from concurrent histories, using fixed languages L that encode the sequential specifications of stacks, queues, priority queues, and maps.

If this is right

  • Linearizability can be decided in time exponential only in the process count for histories of stacks, queues, priority queues, and maps.
  • The same algorithmic framework unifies several previously separate tractable subclasses while complementing known NP-hardness results.
  • Practical implementations can replace exponential-in-history algorithms with ones that scale well when the number of processes remains small.

Where Pith is reading between the lines

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

  • The same reduction technique could be tested on other concurrency properties that also reduce to reachability over history graphs.
  • Runtime monitors for multi-threaded code could adopt this approach when the thread count is bounded in advance.
  • Identifying additional languages with efficient reachability on history graphs would extend the method to more object types.

Load-bearing premise

The sequential specifications of the considered data structures can be captured by fixed languages L for which language reachability is efficiently solvable on the graph structures induced by concurrent histories.

What would settle it

A concrete concurrent history with small k for one of the listed data structures in which the language-reachability procedure returns the wrong answer about linearizability.

Figures

Figures reproduced from arXiv: 2509.05586 by Lee Zheng Han, Umang Mathur.

Figure 1
Figure 1. Figure 1: Linearizable history 𝐻pqueue Example. Priority queue is a anagram-agnostic data type as its state can be determined by its contents. Take the history 𝐻pqueue = {⟨1, enq, 1, 1, 4⟩, ⟨2, enq, 2, 2, 5⟩, ⟨3, enq, 3, 3, 6⟩, ⟨2, deq, 3, 7, 8⟩} (Refer to [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
read the original abstract

We study the linearizability monitoring problem, which asks whether a given concurrent history of a data structure is equivalent to some sequential execution of the same data structure. In general, this problem is $\textsf{NP}$-hard, even for simple objects such as registers. Recent work has identified tractable cases for restricted classes of histories, notably unambiguous and differentiated histories. We revisit the tractability boundary from a fine-grained, parameterized perspective. We show that for a broad class of data structures -- including stacks, queues, priority queues, and maps -- linearizability monitoring is fixed-parameter tractable when parameterized by the number of processes. Concretely, we give an algorithm running in time $O(c^{k} \cdot \textsf{poly}(n))$, where $n$ is the history size, $k$ is the number of processes, and $c$ is a constant, yielding efficient performance when $k$ is small. Our approach reduces linearizability monitoring to a language reachability problem on graphs, which asks whether a labeled graph admits a path whose label sequence belongs to a fixed language $L$. We identify classes of languages that capture the sequential specifications of the above data structures and show that language reachability is efficiently solvable on the graph structures induced by concurrent histories. Our results complement prior hardness results and existing tractable subclasses, and provide a unified algorithmic framework. We implement our approach and demonstrate significant runtime improvements over existing algorithms, which exhibit exponential worst-case behavior.

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 claims that linearizability monitoring for data structures including stacks, queues, priority queues, and maps is fixed-parameter tractable when parameterized by the number of processes k. It reduces the problem to language reachability on graphs induced by concurrent histories and gives an algorithm running in time O(c^k · poly(n)), where the fixed languages L capture the sequential specifications; an implementation is provided that shows runtime improvements over prior exponential algorithms.

Significance. If the reduction holds, the result is significant: it supplies a unified FPT framework that complements existing NP-hardness results and tractable subclasses for restricted histories. The implementation and empirical improvements constitute a concrete strength, offering practical verification for small k without requiring parameter-free derivations or machine-checked proofs.

major comments (2)
  1. [§3] §3 (Reduction to language reachability): the argument that the graphs induced by k-process real-time orders admit O(c^k poly(n)) reachability for the specific languages L of stacks, queues, priority queues, and maps is load-bearing; the manuscript must explicitly exhibit the graph construction and the reachability procedure that exploits the real-time partial order to obtain the stated bound, as the abstract alone leaves open whether the special structure is sufficient for all four data structures.
  2. [§4] §4 (Algorithm and complexity): the claim that language reachability is efficiently solvable relies on the languages L being fixed and the graphs having bounded treewidth or similar structure linear in k; a concrete example or lemma showing how the real-time order bounds the search space for, e.g., the stack language is required to confirm the FPT result is not merely inherited from generic parameterized reachability.
minor comments (2)
  1. The constant c is described as independent of n but possibly dependent on the data structure; a brief table or remark clarifying its value for each of the four objects would improve clarity.
  2. Figure captions and experimental setup should state the range of k values tested and whether the observed runtimes match the predicted c^k dependence.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the positive assessment and the recommendation of minor revision. The comments highlight opportunities to strengthen the clarity of the reduction and algorithmic arguments. We address each major comment below and will revise the manuscript to provide more explicit constructions, lemmas, and examples.

read point-by-point responses

  1. Referee: [§3] §3 (Reduction to language reachability): the argument that the graphs induced by k-process real-time orders admit O(c^k poly(n)) reachability for the specific languages L of stacks, queues, priority queues, and maps is load-bearing; the manuscript must explicitly exhibit the graph construction and the reachability procedure that exploits the real-time partial order to obtain the stated bound, as the abstract alone leaves open whether the special structure is sufficient for all four data structures.

    Authors: We agree that greater explicitness will strengthen the presentation. Section 3 constructs the history-induced graph with vertices for each operation event and directed edges labeled by operation types (push, pop, etc.), where the real-time partial order is encoded as precedence constraints between events from different processes. The reachability procedure computes whether there exists a path whose label sequence is accepted by the fixed automaton for L, using dynamic programming that tracks the set of 'live' processes (at most k) consistent with the partial order; this yields the c^k factor because the frontier of unresolved operations is bounded by the number of processes. We will add an explicit lemma in the revision that states the construction and the DP recurrence uniformly for stacks, queues, priority queues, and maps, confirming that the real-time order supplies the necessary structure for the bound. revision: yes

  2. Referee: [§4] §4 (Algorithm and complexity): the claim that language reachability is efficiently solvable relies on the languages L being fixed and the graphs having bounded treewidth or similar structure linear in k; a concrete example or lemma showing how the real-time order bounds the search space for, e.g., the stack language is required to confirm the FPT result is not merely inherited from generic parameterized reachability.

    Authors: We welcome the request for a concrete illustration. The languages L are indeed fixed and independent of k, but the graphs are not arbitrary: the real-time order induces a partial order whose width is at most k, so that any linear extension respects per-process total orders and cross-process precedence. For the stack language (a variant of Dyck words), this restricts the possible push-pop matchings; we will insert a worked example with a 3-process history of size 8 in the revision, together with a lemma showing that the DP state space for reachability is bounded by O(4^k · n) rather than relying on generic treewidth results. This demonstrates that the FPT bound derives directly from the interplay between the fixed L and the k-bounded real-time structure. revision: yes

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The derivation reduces linearizability monitoring to language reachability on history-induced graphs and invokes standard FPT results for reachability parameterized by the number of processes k. The languages L capturing sequential specifications of stacks, queues, priority queues and maps are fixed and independent of any fitted input; the O(c^k poly(n)) bound follows from known parameterized graph algorithms applied to the real-time order structure, without any equation or step that equates the claimed runtime to a self-defined or fitted quantity. No load-bearing self-citation chain or ansatz smuggling is present; the central claim remains self-contained against external parameterized-complexity benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on standard results from parameterized complexity and automata theory; no new free parameters, ad-hoc axioms, or invented entities are introduced.

axioms (1)
  • domain assumption Language reachability on graphs induced by concurrent histories is solvable in the stated time bound for the languages capturing the sequential specifications of stacks, queues, priority queues, and maps.
    Invoked in the reduction step described in the abstract.

pith-pipeline@v0.9.0 · 5792 in / 1261 out tokens · 31377 ms · 2026-05-18T18:52:31.559968+00:00 · methodology

discussion (0)

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

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

12 extracted references · 12 canonical work pages

  1. [1]

    Josh Alman, Ran Duan, Virginia Vassilevska Williams, Yinzhan Xu, Zixuan Xu, and Renfei Zhou. 2025. More asymmetry yields faster matrix multiplication. InProceedings of the 2025 Annual ACM-SIAM Symposium on Discrete Algorithms (SODA). SIAM, 2005–2039

    work page 2025

  2. [2]

    1969.Programming languages and their compilers: Preliminary notes

    John Cocke. 1969.Programming languages and their compilers: Preliminary notes. New York University. 12 Zheng Han Lee and Umang Mathur

    work page 1969

  3. [3]

    Ulrich Finkler and Kurt Mehlhorn. 1999. Checking priority queues. InProceedings of the tenth annual ACM-SIAM symposium on Discrete algorithms. 901–902

    work page 1999

  4. [4]

    Gerald Gazdar. 1988. Applicability of indexed grammars to natural languages. InNatural language parsing and linguistic theories. Springer, 69–94

    work page 1988

  5. [5]

    Phillip B Gibbons, John L Bruno, and Steven Phillips. 2002. Black-Box Correctness Tests for Basic Parallel Data Structures.Theory of Computing Systems35, 4 (2002), 391–432

    work page 2002

  6. [6]

    Gibbons and Ephraim Korach

    Phillip B. Gibbons and Ephraim Korach. 1997. Testing Shared Memories.Society for Industrial and Applied Mathematics 26, 4 (1997), 1208–1244. https://doi.org/10.1137/S0097539794279614

    work page doi:10.1137/s0097539794279614 1997

  7. [7]

    Aravind K Joshi, S Rao Kosaraju, and H Yamada. 1969. String adjunct grammars. In10th Annual Symposium on Switching and Automata Theory (swat 1969). IEEE, 245–262

    work page 1969

  8. [8]

    Tadao Kasami. 1966. An efficient recognition and syntax-analysis algorithm for context-free languages.Coordinated Science Laboratory Report no. R-257(1966)

    work page 1966

  9. [9]

    Moni Naor and Vanessa Teague. 2001. Anti-persistence: History independent data structures. InProceedings of the thirty-third annual ACM symposium on Theory of computing. 492–501

    work page 2001

  10. [10]

    Marc Shapiro, Nuno Preguiça, Carlos Baquero, and Marek Zawirski. 2011. Conflict-free replicated data types. In Stabilization, Safety, and Security of Distributed Systems: 13th International Symposium, SSS 2011, Grenoble, France, October 10-12, 2011. Proceedings 13. Springer, 386–400

    work page 2011

  11. [11]

    Leslie Valiant. 1974. General context-free recognition in less than cubic time. (1974)

    work page 1974

  12. [12]

    Daniel H Younger. 1967. Recognition and parsing of context-free languages in time n3.Information and control10, 2 (1967), 189–208. Fixed Parameter Tractable Linearizability Monitoring for Stack, Queue and Anagram Agnostic Data Types 13 A PROOFS FOR STACK SECTION Lemma A.1.Given a non-empty well-matched stack history 𝐻 with no failed operations. Let 𝑀 + be...

    work page 1967