Degrees of Separation: A Flexible Type System for Safe Concurrency
summary
A new calculus, Capture Separation Calculus (System CSC), tracks aliases via capturing types and lets code run unmodified by default but enforces separation degrees (annotations) when parallelism is used; the prototype targets Scala-style code and models fork‑join parallelism. The paper proves progress, preservation and confluence, giving a formal data‑race‑freedom guarantee, and reports a motivating real bug where parallel compiler tests failed in 10–50% of runs and were fixed by rejecting unintended global mutables.
AI-written summary · about
chapters (11)
- 0:00Safe concurrency research intro
- 1:50Preventing data races challenge
- 3:39Rust ownership clashes
- 5:26Flexible type system intro
- 6:56Separation degrees for safety
- 9:23Tracking aliases with captures
- 10:27Safety in parallel ops
- 13:58Reader capabilities
- 14:42Formal guarantees and prototype
- 15:04Key takeaways and compatibility
- 15:28Q&A: Moved refs and annotations
related talks
26mDegrees of Separation: A Flexible Type System for Data Race Prevention
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
20mDisentanglement with Futures, State, and Interaction
20mDeadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-O...
54mShared Session Types for Safe, Practical Concurrency
27mConcurrent Incorrectness Separation Logic
54mStructured Concurrency: Hierarchical Cancellation & Error Handling
50mStructured Concurrency: Managing the Hierarchical Cancelation and Error Handling