The semantics and analysis of safe futures

A future is a well-known programming construct used to introduce concurrency to sequential programs. A computation annotated as a future executes asynchronously and concurrently with the computation that follows (called the future’s continuation). In the absence of side-effects, futures satisfy a simple safety property: a program with futures produces the same result as the sequential program from which it was derived. As such, futures are a simple and transparent annotation on sequential programs, visible only in the form of improved concurrency. In languages with support for side-effects, futures are not transparent annotations: a program with futures may not produce the same result as the sequential program from which it was derived. Without the safety property, many of the benefits from using futures are significantly weakened. In such languages, safe futures guarantee that a future-annotated program produces the same result as its sequential counterpart. The focus of this dissertation is developing a semantic framework for safe futures that effectively extracts concurrency in languages with abstractions commonly found in modern programming languages. 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. The approach taken is to use static analysis to approximate sequential program dependences and use the results of the analysis during program evaluation to maximize concurrency while ensuring safety. Safety can be guaranteed by blocking a future’s continuation from violating a potential sequential dependence (i.e. performing an action that depends on an action yet to be performed by its future), as determined by the static analysis. Thus, the amount of concurrency extracted by an operational semantics for safe futures depends on how precisely the semantics can identify when it is safe for a future’s continuation to proceed with evaluation. The contributions of the dissertation are a set of operational semantics and supporting static analyses for safe futures for a higher-order functional language with first-class references and exceptions. For a given formulation, the results of the static analysis are used to instrument the program and an operational semantics for the instrumented program is presented. The semantics are introduced in order of increasing concurrency extracted. Greater concurrency is achieved by using increasingly precise static analysis techniques to approximate sequential dependences