Responsive Parallelism with Synchronization
summary
Claims a static type system plus runtime priority-ceiling prevents priority inversions across mutexes and condition variables, with a formal soundness proof via cost-graph semantics. Implements ownership-token rules and a runtime promote operation; encodings in Rust and C++ enforce the rules. Case study ports include a 20k-line Memcached where changes touch 57% of lines and required 80 person-hours, and the modified server runs under the policy; artifacts and proofs are available.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 0:28Priority inversions
- 1:51Unbounded priority inversions
- 2:54Priority inversion with mutexes
- 3:59Priority inversions with condition variables
- 5:02Type system for inversions
- 7:55Restrictions on spawned threads
- 8:36Introducing promote operation
- 9:59Ownership levels and safety
- 12:47Soundness proof overview
- 13:49Rust and C++ implementations
- 15:35Multi-user chat case study
- 16:43Memcached case study
- 18:09Future work and limitations
- 18:51Conclusion and Q&A
related talks
52mCoroutines: C++ vs Rust
57mInvited Talk: Bridging Safety and Performance
40mRetrofitting Concurrency – Lessons from the Engine Room
29mAsychronous programming in Rust
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
54mShared Session Types for Safe, Practical Concurrency
35mAutomatic Parallelism Management
01h 08mSimplifying Concurrent Programming via Synchronization Synthesis