Dala: A Simple Capability-Based Dynamic Language Design For Data Race-Freedom
summary
Dala is a dynamic capability model that guarantees data-race freedom for safe objects while allowing unsafe objects to coexist. It defines three runtime-enforced capabilities — immutable, isolated, local — where immutable is freely shared, isolated is transferred with destructive nullification, and local cannot be dereferenced off-thread; unsafe objects remain unchecked. The authors present a formal model with proofs of data-race freedom and a dynamic gradual guarantee and report a working prototype runtime called prototype Moth that implements the checks and exceptions.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 0:19Starting Points
- 2:50Data Race
- 3:52Data Race Freedom
- 5:52Object Capabilities
- 7:35Structural Restrictions
- 9:13Safety of the Heap
- 11:16Unsafe Data
- 12:47Conclusion
related talks
32mExploring The Design Space For Runtime Enforcement of Dynamic Capabilities
18mDynamic Region Ownership for Concurrency Safety
26mDegrees of Separation: A Flexible Type System for Data Race Prevention
22mData race detection
20mDegrees of Separation: A Flexible Type System for Safe Concurrency
20mDisentanglement with Futures, State, and Interaction
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
30mA Tale of Shared Memory Concurrency in Programming Languages