Transactional Events for ML (original) (raw)

Transactional events (TE) are an approach to concurrent programming that enriches the first-class synchronous message-passing of Concurrent ML (CML) with a combinator that allows multiple messages to be passed as part of one all-or-nothing synchronization. Donnely and Fluet designed and implemented TE as a Haskell library and demonstrated that it enables elegant solutions to programming patterns that are awkward or impossible in CML. However, both the definition and the implementation of TE relied fundamentally on the code in a synchronization not using mutable memory, an unreasonable assumption for mostly functional languages like ML where functional interfaces may have impure implementations.

We present a definition and implementation of TE that supports ML-style references and nested synchronizations, both of which were previously unnecessary due to Haskell's more restrictive type system. As in prior work, we have a high-level semantics that makes nondeterministic choices such that synchronizations succeed whenever possible and a low-level semantics that uses search to implement the high-level semantics soundly and completely. The key design trade-off in the semantics is to allow updates to mutable memory without requiring the implementation to consider all possible thread interleavings. Our solution uses first-class heaps and allows interleavings only when a message is sent or received. We have used Coq to prove our high- and low-level semantics equivalent.

We have implemented our approach by modifying the Objective Caml run-time system. By modifying the run-time system, rather than relying solely on a library, we can eliminate the potential for nonterminating computations within unsuccessful synchronizations to run forever.

Papers

• Transactional Events for ML.
  Laura Effinger-Dean, Matthew Kehrt, Dan Grossman.
  Presented at ICFP 2008, Victoria, BC. Slides
• Programming Idioms for Transactional Events.
  Matthew Kehrt, Laura Effinger-Dean, Michael Schmitz, Dan Grossman.
  Presented at PLACES 2009, York, UK. Slides (PDF) Slides (Keynote)

Coq Proof

Our proof of the equivalence of the high-level and low-level semantics has been encoded in Coq. You can download our Coq code here.

Implementation

We have implemented transactional events for ML as a modification to OCaml 3.08.1. A patch to this version of OCaml can be found here.

To use TE Caml, programs must be compiled with the -vmthread and the -custom flags.

Previous Work

Our work extends previous efforts by Donnelly and Fluet, which can be found here.