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.
Coq ProofOur proof of the equivalence of the high-level and low-level semantics has been encoded in Coq. You can download our Coq code here.
ImplementationWe 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 WorkOur work extends previous efforts by Donnelly and Fluet, which can be found here.