A Design Space Exploration of Async/Await

In recent years, programming languages have started incorporating async/await keywords for expressing concurrency. The rationale behind this design choice is to make concurrent programs resemble straight-line code, as seen in languages like Python, Rust, and Swift. This concept is referred to as straight-line asynchrony, as opposed to using event loops or callbacks. Over the past 15 years, language designers have been developing models for straight-line asynchrony.

The goal of this project was to explore the similarities and differences in async/await implementations across various languages. Contrary to expectations, the findings reveal that async/await can vary significantly across languages. To illustrate this, a simple async program was written in pseudocode, featuring a function that writes to a log and another that sends the log write as a background task while continuing execution.

Interestingly, seven modern async runtimes exhibited vastly different behaviors for this seemingly straightforward program.

The paper, "A Design Space Exploration of Async/Await", delves into these staggering variations. The authors present four different answers for the program's output, noting that no two runtimes produced the same result for three variations of the simple program. This disparity highlights the importance of understanding a language's async semantics.

The authors explore nine design dimensions that affect the observable semantics of program execution. These dimensions are categorized into three groups: Start of Life, End of Life, and Cancellation. Two of these dimensions, Eagerness and Destruction, are particularly relevant to the example program. Languages with Dynamic Extent, such as Swift and Python+Trio, do not permit tasks to outlive the functions in which they were spawned.

Swift implements Dynamic Extent with Cancelled Destruction, while Trio uses Awaited Destruction, resulting in different outputs for the example program.

Overall, the authors emphasize that there is no universally "right" or "wrong" choice in async programming. Each language's design rationale is unique, and the resulting variations showcase the complexity of explaining output for even simple programs. To better understand the design space, the authors have translated it into a formal semantics on a core calculus of asynchronous programs, which can be used to trace the execution and explain the divergent outcomes.