License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2019.2
URN: urn:nbn:de:0030-drops-107949
Go to the corresponding LIPIcs Volume Portal

Fernandez-Reyes, Kiko ; Clarke, Dave ; Henrio, Ludovic ; Johnsen, Einar Broch ; Wrigstad, Tobias

Godot: All the Benefits of Implicit and Explicit Futures

LIPIcs-ECOOP-2019-2.pdf (0.9 MB)


Concurrent programs often make use of futures, handles to the results of asynchronous operations. Futures provide means to communicate not yet computed results, and simplify the implementation of operations that synchronise on the result of such asynchronous operations. Futures can be characterised as implicit or explicit, depending on the typing discipline used to type them.
Current future implementations suffer from "future proliferation", either at the type-level or at run-time. The former adds future type wrappers, which hinders subtype polymorphism and exposes the client to the internal asynchronous communication architecture. The latter increases latency, by traversing nested future structures at run-time. Many languages suffer both kinds.
Previous work offer partial solutions to the future proliferation problems; in this paper we show how these solutions can be integrated in an elegant and coherent way, which is more expressive than either system in isolation. We describe our proposal formally, and state and prove its key properties, in two related calculi, based on the two possible families of future constructs (data-flow futures and control-flow futures). The former relies on static type information to avoid unwanted future creation, and the latter uses an algebraic data type with dynamic checks. We also discuss how to implement our new system efficiently.

BibTeX - Entry

  author =	{Kiko Fernandez-Reyes and Dave Clarke and Ludovic Henrio and Einar Broch Johnsen and Tobias Wrigstad},
  title =	{{Godot: All the Benefits of Implicit and Explicit Futures}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{2:1--2:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Alastair F. Donaldson},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-107949},
  doi =		{10.4230/LIPIcs.ECOOP.2019.2},
  annote =	{Keywords: Futures, Concurrency, Type Systems, Formal Semantics}

Keywords: Futures, Concurrency, Type Systems, Formal Semantics
Collection: 33rd European Conference on Object-Oriented Programming (ECOOP 2019)
Issue Date: 2019
Date of publication: 10.07.2019
Supplementary Material: ECOOP 2019 Artifact Evaluation approved artifact available at

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI