Reasoning about Progress of Concurrent Objects
summary
Introduces a Hoare‑style program logic that proves termination properties of concurrent objects by separating two concrete causes of nontermination — blocking and delay — and tracking them with resource tokens. The logic adds loop/delay tokens to bound spin loops and a notion of definite actions to break circular blocking arguments (used to reason about ticket locks, CAS counters, lock‑coupling lists). It claims a uniform derivation of wait‑freedom, lock‑freedom, obstruction‑freedom, starvation‑free and deadlock‑free guarantees, is not automated, and is intentionally not complete.
AI-written summary · about
chapters (11)
- 0:00Start
- 2:06What Is a Concurrent Object
- 2:51World Examples of a Concurrent Object
- 9:40Environmental Behaviors
- 13:02Algorithm Blocking Errors
- 17:42Obstruction Free Algorithm
- 24:14Definition of Establishing Freedom
- 27:22Verify the Progress
- 28:07Sequential Verification for Loops in Sequential Programs
- 30:11How Do We Verify this Concurrent Algorithm
- 48:02Summary
related talks
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
24mA Concurrent Program Logic with a Future and History
20mDeadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-O...
01h 01mThe Future of Concurrency and Parallelism
19mScenario-based Proofs for Concurrent Objects
23mProbabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and(…)
28mReasoning about Distributed Reconfigurable Systems
26mConcurrency: Unlocking a Solution