Recent work has proposed a memory property for parallel programs, called disentanglement, and showed that it is pervasive in a variety of programs, written in different languages, ranging from C/C++ to Parallel ML, and showed that it can be exploited to improve the performance of parallel functional programs. All existing work on disentanglement, however, considers the “fork/join” model for parallelism and does not apply to ``futures'', the more powerful approach to parallelism. This is not surprising: fork/join parallel programs exhibit a reasonably strict dependency structure (e.g., series-parallel DAGs), which disentanglement exploits. In contrast, with futures, parallel computations become first-class values of the language, and thus can be created, and passed between functions calls or stored in memory, just like any other ordinary value, resulting in complex dependency structures, especially in the presence of mutable state. For example, parallel programs with futures can have deadlocks, which is impossible with fork-join parallelism.
In this paper, we are interested in the theoretical question of whether disentanglement may be extended beyond fork/join parallelism, and specifically to futures. We consider a functional language with futures, Input/Output (I/O), and mutable state (references) and show that a broad range of programs written in this language are disentangled. We start by formalizing disentanglement for futures and proving that purely functional programs written in this language are disentangled. We then generalize this result in three directions. First, we consider state (effects) and prove that stateful programs are disentangled if they are race free. Second, we show that race freedom is sufficient but not a necessary condition and non-deterministic programs, e.g. those that use atomic read-modify-operations and some non-deterministic combinators, may also be disentangled. Third, we prove that disentangled task-parallel programs written with futures are free of deadlocks, which arise due to interactions between state and the rich dependencies that can be expressed with futures. Taken together, these results show that disentanglement generalizes to parallel programs with futures and, thus, the benefits of disentanglement may go well beyond fork-join parallelism.
Thu 18 JanDisplayed time zone: London change
15:30 - 16:50 | |||
15:30 20mTalk | Pipelines and Beyond: Graph Types for ADTs with Futures POPL Francis Rinaldi Illinois Institute of Technology, june wunder Boston University, Arthur Azevedo de Amorim Rochester Institute of Technology, USA, Stefan K. Muller Illinois Institute of Technology | ||
15:50 20mTalk | Disentanglement with Futures, State, and Interaction POPL Jatin Arora Carnegie Mellon University, Stefan K. Muller Illinois Institute of Technology, Umut A. Acar Carnegie Mellon University | ||
16:10 20mTalk | DisLog: A Separation Logic for Disentanglement POPL Alexandre Moine Inria, Sam Westrick Carnegie Mellon University, Stephanie Balzer Carnegie Mellon University Pre-print | ||
16:30 20mTalk | Automatic Parallelism ManagementDistinguished Paper POPL Sam Westrick Carnegie Mellon University, Matthew Fluet Rochester Institute of Technology, Mike Rainey Carnegie Mellon University, Umut A. Acar Carnegie Mellon University |