Degrees of Separation: A Flexible Type System for Data Race Prevention
summary
Proposes Capture Separation Calculus (CSC) that lets aliasing remain common but tracks and restricts aliases only where races matter, proving type safety and data-race freedom by showing reduction confluence; implements CSC as a Scala 3 compiler extension with prototype support for separation degree inference and new capture-based types that record which variables a value can touch. Demonstrates examples where fresh allocations are treated as separated, parallel bindings are checked, and problematic concurrent read/write patterns are rejected.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 2:29Data races and prevention
- 7:28Flexible type system need
- 10:59Separation degrees in CSC
- 16:38Capability-based separation
- 18:23Formal system guarantees
- 20:50Gap in race prevention
- 21:12Q&A
related talks
20mDegrees of Separation: A Flexible Type System for Safe Concurrency
27mConcurrent Incorrectness Separation Logic
20mDisentanglement with Futures, State, and Interaction
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
21mFair Termination of Binary Sessions
21mCSL and relaxed memory
17mSSRD: Shapes and Summaries for Race Detection in Concurrent Data Structures
14mDala: A Simple Capability-Based Dynamic Language Design For Data Race-Freedom