Dependence analysis for safe futures

Abstract

A future is a well-known programming construct used to introduce concurrency into sequential programs. Computations annotated as futures are executed asynchronously and run concurrently with their continuations. Typically, futures are not transparent annotations: a program with futures need not produce the same result as the sequential program from which it was derived. Safe futures guarantee that a future-annotated program produces the same result as its sequential counterpart. The safety property is trivially satisfied in languages without side-effects or exceptions. In the presence of mutable references and language abstractions, such as exceptions, which permit the expression of non-local control-flow, ensuring safety requires that the future-annotated program adhere to control and data dependences imposed by the program's sequential counterpart. In this paper, we present a formulation of safe futures for a higher-order functional language with first-class references and exceptions. Safety can be guaranteed at runtime by blocking a continuation from performing a potentially unsafe action before its futures have completed. To enable greater concurrency, we develop a static analysis and instrumentation and formalize the runtime behavior for instrumented programs that allows a continuation to proceed before its futures complete, as long as its actions are determined to be safe. A continuation's action is safe if it is not control or data dependent on actions that may subsequently be performed by its futures.