Dala: A Simple Capability-Based Dynamic Language Design For Data-Race Freedom
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.
Kiko Fernandez-Reyes, Isaac Oscar Gariano, James Noble, Erin Greenwood-Thessman, Michael Homer, Tobias Wrigstad
ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!
The final copy of this publication is available from the publisher
- this page
Michael Homer — 2023