Transactional Events

• icfp06.pdf (with Kevin Donnelly; Appeared at ICFP'06; ICFP06/20060919-ICFP06.ppt)

  Concurrent programs require high-level abstractions in order to manage complexity and enable compositional reasoning. In this paper, we introduce a novel concurrency abstraction, dubbed transactional events, which combines first-class synchronous message-passing events with all-or-nothing transactions. This combination enables simple solutions to interesting problems in concurrent programming. For example, guarded synchronous receive can be implemented as an abstract transactional event, whereas in other languages it requires a non-abstract, non-modular protocol. Likewise, three-way rendezvous can also be implemented as an abstract transactional event, which is impossible using first-class events alone. Both solutions are easy to code and easy to reason about.

  The expressive power of transactional events arises from a sequencing combinator whose semantics enforces an all-or-nothing transactional property -- either both of the constituent events synchronize in sequence or neither of them synchronizes. This sequencing combinator, along with a non-deterministic choice combinator, gives transactional events the compositional structure of a monad-with-plus. We provide a formal semantics for and a preliminary implementation of transactional events.

  Supporting materials:

  • A "proof-of-concept" implementation of Transactional Events in Haskell using the software transactional memory extensions of GHC.

    • TxEvent.tgz

      Library source, documentation, and examples. Install using Cabal.

    • Documentation

      Library documentation, built using Haddock.

    • ImplDynamics.pdf

      A high-level overview of the implementation, given via a semi-formal small-step operational semantics. I find the semantics helpful in understanding the implementation, but your mileage may vary. Some points of comparison: (1) In the Haskell implementation, we use a CPS-like encoding of the monad in order to spawn search threads; in the semantics, I use a more direct style with multiple kinds of threads in the thread soup. (2) In the Haskell implementation, we use the STM monad to atomically access shared mutable state; in the semantics, I simply manipulate a global heap, using the convention that all antecedents in a transition rule must happen atomically with respect to other transitions that modify the heap.

• cs257.pdf (Written for CS257; 20060117-CS257.pdf)

  The event type constructor and combinators of Reppy's Concurrent ML bear a superficial resemblance to the MonadPlus type-class of Haskell. However, it is easy to demonstrate that the most natural means of extending CML events to an instance of MonadPlus fail to satisfy the necessary monad laws.

  In this work, we will review the monad laws and the reasons that CML events do not naturally form a MonadPlus instance. This investigation reveals that the essential missing component is an event combinator (thenEvt) which combines a sequence of events into a single event and whose semantics ensure an "all-or-nothing" property -- either all of the constituent events synchronize in sequence or none of them synchronize.

  We propose a new concurrency calculus that draws inspiration from both Concurrent ML and Concurrent Haskell. Like Concurrent ML, it includes first-class synchronous events and event combinators, extended with the thenEvt combinator in a manner that forms a MonadPlus. Like Concurrent Haskell, it includes first-class IO actions and IO combinators, forming a Monad.