2021/09/15 by Kiko Fernandez-Reyes, Fernandez-Reyes, Kiko, Isaac Oscar Gariano +9 · 1 voice
Computer Science · #Advanced Data Storage Technologies #Distributed #Distributed systems and fault tolerance #FOS: Computer and information sciences #Parallel #Parallel Computing and Optimization Techniques #Programming Languages (cs.PL) #and Cluster Computing (cs.DC) #cs.DC #cs.PL
paper · pdf · doi:10.48550/arxiv.2109.07541
openalex publication_date 2021/09/15 · arxiv published 2021/09/15 · arxiv updated 2021/09/15 · openalex created_date 2022/07/25 · openalex updated_date 2026/07/28
Dynamic languages like Erlang, Clojure, JavaScript, and E adopted data-race\nfreedom by design. To enforce data-race freedom, these languages either deep\ncopy objects during actor (thread) communication or proxy back to their owning\nthread. We present Dala, a simple programming model that ensures data-race\nfreedom while supporting efficient inter-thread communication. Dala is a\ndynamic, concurrent, capability-based language that relies on three core\ncapabilities: immutable values can be shared freely; isolated mutable objects\ncan be transferred between threads but not aliased; local objects can be\naliased within their owning thread but not dereferenced by other threads.\nObjects with capabilities can co-exist with unsafe objects, that are unchecked\nand may suffer data races, without compromising the safety of safe objects. We\npresent a formal model of Dala, prove data race-freedom and state and prove a\ndynamic gradual guarantee. These theorems guarantee data race-freedom when\nusing safe capabilities and show that the addition of capabilities is semantics\npreserving modulo permission and cast errors.\n