Combining Shared State with Speculative Parallelism in a Functional Language

Purely functional programming languages have proven to be an attractive option for implementing parallel applications. The absence of mutable state eliminates the possibility for race conditions, which relieves programmers from reasoning about the exponential interleavings of threads and nondeterministic behavior. Unfortunately, there are applications that, by making use of shared state, can achieve significant constant factor speedups compared to their purely functional counterparts. IVars have been proposed as a possible solution, allowing threads to share information via write-once references, while preserving a deterministic semantics. However, in the presence of speculative parallelism (cancelation), this determinism guarantee is lost. In this work we show how to go about combining these two features by proposing a dynamic rollback mechanism for enforcing determinism. We have formalized the semantics of a parallel functional language extended with IVars, speculative parallelism, and our proposed rollback mechanism using the Coq proof assistant and have proven that it preserves determinism. Additionally, we describe a preliminary implementation in the context of the Manticore project and give some initial performance results.