Fixed Parameter Tractable Linearizability Monitoring
summary
Claims that linearizability monitoring is fixed‑parameter tractable parameterized by number of processes k for stacks, queues, priority queues and maps, giving an algorithm running in O(c^k · poly(n)) where n is history length; reduces monitoring to language reachability on a frontier graph whose size is linear in n and exponential only in k; defines classes (order‑oblivious, α‑extensions, CFL ADTs) that admit polynomial reachability; gives a two‑pointer streaming algorithm for queues; supplies an implemented tool with large practical speedups over prior tools.
AI-written summary · about
chapters (12)
- 0:00Linearizability monitoring intro
- 1:24FPT complexity for monitoring
- 2:06What is linearizability?
- 4:34Challenges in verification
- 6:20Unifying framework via graph reachability
- 7:22Frontier graph construction
- 9:49Order oblivious data types
- 11:55Context-free data structures
- 13:39Improved FPT for stacks/queues
- 15:23Linear-time streaming for queues
- 17:49Tool evaluation and performance
- 18:32Summary and availability
related talks
10mEfficient Decrease-And-Conquer Linearizability Monitoring
19mEfficient Linearizability Monitoring
25mThe Path to Durable Linearizability
24mA Compositional Theory of Linearizability
12mCompositionality and Observational Refinement for Linearizability with Crashes
22mContext-Bounded Verification of Thread Pools
25mParametrised Verification of Intel-x86 Programs
26mHigher-Order Leak and Deadlock Free Locks