Dala: A Simple Capability-Based Dynamic Language Design For Data Race-Freedom

TL;DR

Dala is a dynamic, capability-based programming language designed to ensure data-race freedom efficiently during inter-thread communication, combining formal guarantees with practical flexibility.

Contribution

It introduces a simple, formal capability model for dynamic languages that guarantees data-race freedom while supporting efficient communication.

Findings

Proves data race-freedom and gradual guarantee for Dala

Demonstrates safe coexistence of safe and unsafe objects

Provides a formal model and semantics-preserving extensions

Abstract

Dynamic languages like Erlang, Clojure, JavaScript, and E adopted data-race freedom by design. To enforce data-race freedom, these languages either deep copy objects during actor (thread) communication or proxy back to their owning thread. We present Dala, a simple programming model that ensures data-race freedom while supporting efficient inter-thread communication. Dala is a dynamic, concurrent, capability-based language that relies on three core capabilities: immutable values can be shared freely; isolated mutable objects can be transferred between threads but not aliased; local objects can be aliased within their owning thread but not dereferenced by other threads. Objects with capabilities can co-exist with unsafe objects, that are unchecked and may suffer data races, without compromising the safety of safe objects. We present a formal model of Dala, prove data race-freedom and state and prove a dynamic gradual guarantee. These theorems guarantee data race-freedom when using safe capabilities and show that the addition of capabilities is semantics preserving modulo permission and cast errors.