Efficient Decrease-and-Conquer Linearizability Monitoring

Watch this 10-minute conference presentation from OOPSLA 2025 that introduces a novel algorithmic framework for efficiently monitoring linearizability in concurrent data structures. Learn about the decrease-and-conquer approach that identifies special linearizability-preserving values in execution histories to determine if concurrent data structure implementations are correct. Discover how this framework addresses the computational intractability of linearizability monitoring by systematically identifying when the problem becomes tractable through the presence or absence of these special values. Explore polynomial-time algorithms derived for popular concurrent data types including registers, sets, stacks, queues, and priority queues under unambiguity restrictions where each insertion adds a distinct value. Understand the optimization techniques that achieve log-linear running time through efficient data structures that amortize the cost of solving induced sub-problems. Examine evaluation results demonstrating how this approach scales to very large execution histories and significantly outperforms existing state-of-the-art linearizability monitoring tools, making it a promising solution for early problem detection in concurrent data structure development and stress testing implementations.