Digitala Vetenskapliga Arkivet

Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Dala: A Simple Capability-Based Dynamic Language Design For Data-Race Freedom
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.ORCID iD: 0000-0001-8654-118x
Victoria University of Wellington, Wellington, New Zealand.ORCID iD: 0000−0001−9036−5692
Victoria University of Wellington, Wellington, New Zealand.
Victoria University of Wellington, Wellington, New Zealand.
Show others and affiliations
(English)Manuscript (preprint) (Other academic)
Abstract [en]

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 capa- bilities: 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. The addition of a fourth capability, unsafe, allows data races and we show how data-race free programs interact with unsafe programs. We present a formal model of Dala, prove data race-freedom and the dynamic gradual guarantee. These theorems guarantee data race-freedom when using safe capabilities and show that the addition of capabili- ties is semantics preserving modulo permission and cast errors.

National Category
Computer Systems
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-425127OAI: oai:DiVA.org:uu-425127DiVA, id: diva2:1500578
Available from: 2020-11-12 Created: 2020-11-12 Last updated: 2021-01-29Bibliographically approved
In thesis
1. Abstractions to Control the Future
Open this publication in new window or tab >>Abstractions to Control the Future
2021 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Multicore and manycore computers are the norm nowadays, and users have expectations that their programs can do multiple things concurrently. To support that, developers use concur- rency abstractions such as threads, promises, futures, and/or channels to exchange information. All these abstractions introduce trade-offs between the concurrency model and the language guarantees, and developers accept these trade-offs for the benefits of concurrent programming.

Many concurrent languages are multi-paradigm, e.g., mix the functional and object-oriented paradigms. This is beneficial to developers because they can choose the most suitable approach when solving a problem. From the point of view of concurrency, purely functional programming languages are data-race free since they only support immutable data. Object-oriented languages do not get a free lunch, and neither do multi-paradigm languages that have imperative features.

The main problem is uncontrolled concurrent access to shared mutable state, which may inadvertently introduce data-races. A data-race happens when two concurrent memory operations target the same location, at least one of them is a write, and there is no synchronisation operation involved. Data-races make programs to exhibit (unwanted) non-deterministic behaviour.

The contribution of this thesis is two-fold. First, this thesis introduces new concurrent abstractions in a purely functional, statically typed programming language (Paper I – Paper III); these abstractions allow developers to write concurrent control- and delegation-based patterns. Second, this thesis introduces a capability-based dynamic programming model, named Dala, that extends the applicability of the concurrent abstractions to an imperative setting while maintaining data-race freedom (Paper IV). Developers can also use the Dala model to migrate unsafe programs, i.e., programs that may suffer data-races, to data-race free programs.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2021. p. 85
Series
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 1986
Keywords
concurrent, programming, type system, future, actors, active objects
National Category
Computer Systems
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-425128 (URN)978-91-513-1062-6 (ISBN)
Public defence
2021-01-18, Room 2446, ITC, Lägerhyddsvägen 2, hus 2, Uppsala, 16:00 (English)
Opponent
Supervisors
Available from: 2020-12-21 Created: 2020-11-18 Last updated: 2021-01-25

Open Access in DiVA

No full text in DiVA

Search in DiVA

By author/editor
Fernandez-Reyes, KikoNoble, JamesHomer, MichaelWrigstad, Tobias
By organisation
Computing Science
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

urn-nbn
Total: 241 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf