Transactional Events

• An implementation of Transactional Events in Haskell using the software transactional memory extensions of GHC.
  • tx-events-0.4.tgz

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

  • Documentation

    Library documentation, built using Haddock.

• ifl11.pdf techrpt.pdf (with Edward Amsden; Accepted to IFL'11 (post-proceedings))

  Transactional events are a recent concurrency abstraction that combines first-class synchronous message-passing events with all-or-nothing transactions. Transactional events provide both a sequencing combinator, which permits the description of behaviors in which multiple potential synchronization actions (including communications between threads) either all occur in sequence or none of them occur, and a non-deterministic choice combinator, which permits the description of behaviors in which exactly one of a set of potential synchronization actions occurs. While prior work gave a semantics and an implementation for transactional events, it provided no guarantees about which of the many non-deterministic executions might be exhibited by a program.

  For concurrent systems, like transactional events, it is natural to expect certain fairness conditions to hold on executions. Intuitively, fairness guarantees that any system component that could (sufficiently often) make progress does, in fact, make progress. In this work, we investigate fairness for transactional events. We give a rigorous definition of fair program executions in transactional events, describe a refined operational semantics that guarantees fair executions, and discuss restrictions and assumptions necessary for the correctness of an implementation based on the refined semantics.

• jfp08.pdf jfp08-appendix.pdf (with Kevin Donnelly; Appeared in the Journal of Functional Programming)

  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 transactional events and give a detailed account of an implementation.

• 20070510-CMSC32630.pdf (Presentation at UoC CMSC 32630)

• 20070209-PLLunch.pdf (Presentation at UoC & TTI-C Programming Languages Lunch)

• icfp06.pdf (with Kevin Donnelly; Appeared at ICFP'06; 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.

• 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.