Shared Session Types for Safe, Practical Concurrency

on YouTube ↗54m

" summary

Introduces a type system that layers linear and shared session types with up/down modalities to enforce an acquire-release discipline and an equi-synchronizing constraint so shared channels become temporarily linear; this yields compile-time protocol adherence and absence of high-level and low-level data races. The original shared design permits deadlocks, then an extension called manifest deadlock freedom removes them by construction. Prototype work targets Rust/Servo integration via libraries; tradeoffs include locking overhead and scalability concerns versus the strong static guarantees.

AI-written summary · about

" chapters (14)

1. 0:00Start
2. 1:35Title
3. 3:36The Shared Memory Approach
4. 4:45Research
5. 5:37The Notion of Shared Session Types
6. 6:43Introduction to Session Types
7. 7:36Image Loader
8. 12:30Introduction into Session Types
9. 29:51How Can We Restore Protocol Adherents in the Presence of Aliasing
10. 30:01Ingredients to the Solution
11. 38:28Manifest Sharing
12. 43:25Deadlock Freedom
13. 50:34But I Don't Have Time Anymore in this Talk so in Order Also To Give You the Possibility To Ask Me some More Questions Let Me Basically Briefly Tell You that that We Are Transposing those Ideas Also to Other Domains in Particular We Right Now Work on Introducing Shared Session Types with Resource Analysis in Digital Contracts and Then Let Me Finish Up and Take Questions I'M Basically Just Showing Here on the Slide Where You the Papers You Can Read Up on the Work I'Ve Presented Perfect Let's all Thank Stephanie for the Wonderful Keynote
14. 51:07And Then Let Me Finish Up and Take Questions I'M Basically Just Showing Here on the Slide Where You the Papers You Can Read Up on the Work I'Ve Presented Perfect Let's all Thank Stephanie for the Wonderful Keynote I Have the Mic Thank You It's a Very Good Talk I Really Enjoyed It I'M Wondering if It Will Just Solve the Problem of Protocol Adherence and Race Conditions but Don't We Introduce the Concurrency Forgotten Currency Scalability Problem because You Now Have Floating on the Whole Resources or Channels How Will It Scale Okay so that's a Very Good Question and I Think I Understand Why You'Re Asking this because Yes as You Observed

" related talks

• 50mSession Types Meet Polymorphism and Dependent TypesPeter Thiemann · PLMW @ POPL 2023
• 15mBorrowing From Session TypesHannes Saffrich, Janek Spaderna, Peter Thiemann · OOPSLA 2025
• 25mResponsive Parallelism with SynchronizationUmut A. Acar, Stefan K. Muller, Kyle Singer, Devyn Terra Keeney, Andrew Neth, Kunal Agrawal, I-Ting Angelina Lee · PLDI 2023
• 35mAsynchronous and Synchronous Mixed SessionsNobuko Yoshida, Kirstin Peters · ST30 2023
• 32mIntrinsically Typed Sessions with CallbacksPeter Thiemann · ICFP 2023
• 51mMemory Model: Get your shared data under controlJana Machutová · NDC TechTown 2024
• 23mPrecise Subtyping for Asynchronous Multiparty SessionsNobuko Yoshida, Alceste Scalas, Silvia Ghilezan, Ivan Prokić, Jovanka Pantović · POPL 2021
• 28mDependent Session Protocols in Separation Logic from First PrinciplesRobbert Krebbers, Jonas Kastberg Hinrichsen, Jules Jacobs · ICFP 2023