Transactional events for ML

ABSTRACT

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. Donnelly and Fluet (2006) 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 the 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.

REFERENCES

• 1: Joe Armstrong , Robert Virding , Claes Wikström , Mike Williams, Concurrent programming in ERLANG (2nd ed.), Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1996
• 2: Kevin Donnelly and Matthew Fluet. Transactional events. The Journal of Functional Programming, 2008. To appear.
• 3: Kevin Donnelly , Matthew Fluet, Transactional events, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, September 16-21, 2006, Portland, Oregon, USA
• 4: Matthew Flatt , Robert Bruce Findler, Kill-safe synchronization abstractions, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 5: Tim Harris , Keir Fraser, Language support for lightweight transactions, Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, October 26-30, 2003, Anaheim, California, USA
• 6: Tim Harris , Simon Marlow , Simon Peyton-Jones , Maurice Herlihy, Composable memory transactions, Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 15-17, 2005, Chicago, IL, USA [doi>10.1145/1065944.1065952]
• 7: Tim Harris , Simon Marlow , Simon Peyton Jones, Haskell on a shared-memory multiprocessor, Proceedings of the 2005 ACM SIGPLAN workshop on Haskell, p.49-61, September 30-30, 2005, Tallinn, Estonia [doi>10.1145/1088348.1088354]
• 8: C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
• 9: Suresh Jagannathan , Jan Vitek , Adam Welc , Antony Hosking, A transactional object calculus, Science of Computer Programming, v.57 n.2, p.164-186, August 2005 [doi>10.1016/j.scico.2005.03.001]
• 10: Alan Jeffrey, A Fully Abstract Semantics for a Concurrent Functional Language with Monadic Types, Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, p.255, June 26-29, 1995
• 11: Aaron Kimball and Dan Grossman. Software transactions meet first-class continuations. In 8th Annual Workshop on Scheme and Functional Programming, 2007.
• 12: Xavier Leroy. The Objective Caml system release 3.10, Event module, 2007. http://caml.inria.fr/pub/docs/manual-ocaml/libref/Event.html.
• 13: Katherine F. Moore , Dan Grossman, High-level small-step operational semantics for transactions, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 14: Prakash Panangaden and John Reppy. The essence of Concurrent ML. In Flemming Nielson, editor, ML with Concurrency: Design, Analysis, Implementation, and Application, Springer Monographs in Computer Science. Springer-Verlag, 1997.
• 15: John H. Reppy, Concurrent programming in ML, Cambridge University Press, New York, NY, 1999
• 16: John Reppy , Yingqi Xiao, Specialization of CML message-passing primitives, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 17: John Reppy and Yinqi Xiao. Toward a parallel implementation of Concurrent ML. In Workshop on Declarative Aspects of Multicore Programming, 2008.
• 18: Michael F. Ringenburg , Dan Grossman, AtomCaml: first-class atomicity via rollback, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 19: George Russell, Events in Haskell, and how to implement them, Proceedings of the sixth ACM SIGPLAN international conference on Functional programming, September 03-05, 2001, Florence, Italy
• 20: Yannis Smaragdakis , Anthony Kay , Reimer Behrends , Michal Young, Transactions with isolation and cooperation, Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications, October 21-25, 2007, Montreal, Quebec, Canada
• 21: Lukasz Ziarek and Suresh Jagannathan. Memoizing multi-threaded transactions. In Workshop on Declarative Aspects of Multicore Programming, 2008.
• 22: Lukasz Ziarek , Philip Schatz , Suresh Jagannathan, Stabilizers: a modular checkpointing abstraction for concurrent functional programs, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, September 16-21, 2006, Portland, Oregon, USA

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Concurrent programming structures

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming

General Terms:
Design, Languages

Keywords:
concurrency, synchronous message passing, transactional events