Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models
summary
Generalizes recurrence sets from states to execution-based recurrence sets over axiomatic weak-memory execution graphs, proves soundness for all practical memory models and completeness on many, and gives a finite witness shape: a repeating execution infix (a lasso). Implements a lasso-finding algorithm in Dartagnan as an SMT-backed bounded checker, evaluates on CPU and GPU models and a lock/data-structure suite, automatically finds known liveness violations but reports many GPU litmus checks as unknown because those tests terminate, and observes identical results under SC for the evaluated GPU benchmarks.
AI-written summary · about
chapters (12)
- 0:00Fair non-termination basics
- 1:06Recurrent sets in sequential
- 2:50Execution graphs for weak memory
- 6:21Recurrent sets defined
- 7:46Peterson’s algorithm demo
- 9:53Finite representation via abstraction
- 13:44Abstracting with lassos
- 16:06Lasso detection with Data
- 18:52Evaluating concurrent data structures
- 20:34GPU testing under unfair schedulers
- 22:16Summary of results
- 22:40Question and answer session
related talks
26mKater: Automating Weak Memory Model Metatheory and Consistency Checking
20mDeciding Asynchronous Hyperproperties for Recursive Programs
16mModel Checking for a Multi-Execution Memory Model
19mSolving Infinite-State Games via Acceleration
15mTowards a Formal Foundation of Intermittent Computing
05mWelcome
25mMultiple Resumptions and Local Mutable State, Directly
25mSafe Replication through Bounded Concurrency Verification