TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
summary
TaDA Live claims compositional proofs of termination for blocking fine‑grained concurrent programs by extending separation logic with a semantic model of layered subjective obligations and a sound proof system. It uses obligation tokens (u), two assertions for local obligations and environment obligations, an environment liveness condition for loops, and obligation layers plus logical atomicity to avoid deadlock and preserve modular specs. The logic verifies library implementations and client code modularly; case studies and a full soundness proof are provided.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 4:52Standard Specification Format
- 6:58The Live
- 12:13Obligations
- 16:22Logical Atomicity
- 17:11Atomic Triples
- 19:45Implementation Proof
- 21:23Questions
related talks
54mReasoning about Progress of Concurrent Objects
31mTermination in Concurrency, Revisited
21mA Semantic Logical Relation for Termination of Intuitionistic Linear Logic Session Types
20mTrillium: Higher-Order Concurrent and Distributed Separation Logic for Intension...
28mReasoning about Distributed Reconfigurable Systems
01h 01mThe Future of Concurrency and Parallelism
23mStratified Commutativity in Verification Algorithms for Concurrent Programs
24mProving False in Object Oriented Verification Programs by Exploiting Non-Termination