Dala：一种简单的基于能力的数据无竞争动态语言设计
Dala: A Simple Capability-Based Dynamic Language Design For Data Race-Freedom
摘要：
Erlang、Clojure、JavaScript和E等动态语言在设计上采用了数据竞争自由。为了加强数据竞争自由，这些语言要么在参与者（线程）通信期间深度复制对象，要么代理回它们所属的线程。我们提出了达拉，一个简单的编程模型，确保数据竞争的自由，同时支持高效的线程间通信。Dala是一种动态的、并发的、基于能力的语言，它依赖于三个核心能力：不可变的值可以自由共享;孤立的可变对象可以在线程之间传输，但不能别名化;本地对象可以在其拥有的线程内别名化，但不能被其他线程解引用。具有功能的对象可以与不安全的对象共存，这些对象未经检查并且可能遭受数据竞争，而不会损害安全对象的安全性。我们提出了Dala的形式化模型，证明了数据竞争自由和状态，并证明了一个动态的渐进保证。这些定理保证了使用安全能力时的数据竞争自由，并表明能力的增加是语义保留模权限和转换错误。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
