📝 SummarXiv

Abstract

Verifying linearizability of concurrent data structures is NP-hard, even for simple types. We present fixed-parameter tractable algorithms for monitoring stacks, queues, and anagram-agnostic data types (AADTs), parameterized by the maximum concurrency. Our approach leverages frontier graphs and partition states to bound the search space. For AADTs, equivalence of linearizations enables monitoring in log-linear time. For stacks, we introduce a grammar-based method with a sub-cubic reduction to matrix multiplication, and for queues, a split-sequence transition system supporting efficient dynamic programming. These results unify tractability guarantees for both order-sensitive and anagram-agnostic data types under bounded concurrency.