Document Open Access Logo

Godot: All the Benefits of Implicit and Explicit Futures

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

Thumbnail PDF


  • Filesize: 0.91 MB
  • 28 pages

Document Identifiers

Author Details

Kiko Fernandez-Reyes
  • Uppsala University, Sweden
Dave Clarke
  • Storytel, Stockholm, Sweden
Ludovic Henrio
  • Univ Lyon, EnsL, UCBL, CNRS, Inria, LIP, France
Einar Broch Johnsen
  • University of Oslo, Norway
Tobias Wrigstad
  • Uppsala University, Sweden

Cite AsGet BibTex

Kiko Fernandez-Reyes, Dave Clarke, Ludovic Henrio, Einar Broch Johnsen, and Tobias Wrigstad. Godot: All the Benefits of Implicit and Explicit Futures. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 2:1-2:28, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)


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.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Concurrency control
  • Software and its engineering → Concurrent programming languages
  • Software and its engineering → Concurrent programming structures
  • Futures
  • Concurrency
  • Type Systems
  • Formal Semantics


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail