Atomic

We are investigating issues related to software transactional memory, a concurrency primitive that is easier-to-use and harder-to-implement than locks. Our work has considered language design, semantics, (software) implementation, and evaluation (for reliability and performance). Prior work has resulted in several publications and prototypes from the group; see below.

Currently, we are considering two questions that are important for integrating transactions with sensible semantics and efficient implementations into modern programmling langauges.

• Region-Based Dynamic Separation for STM Haskell: We have implemented dynamic separation in Haskell. Dynamic separation is a recent approach to software transactional memory (STM) that achieves strongly-atomic semantics with performance comparable to that of a weakly-atomic STM. STM Haskell, a lazy-versioning STM library for Haskell, previously supported strongly-atomic semantics via static separation, and we have found dynamic separation to be a natural extension of the library's interface. Our approach to dynamic separation makes several advances over previous work. First, we use a notion of regions to allow entire data structures to share a protection state, which avoids expensive and unnecessary data-structure traversals. Second, we enrich the set of protection states with a "thread-local" state that allows data to be used inside and outside transactions. Third, we support static and dynamic separation, and in particular use a well-typed interface to allow all dynamic-separation code to be safely composed with static-separation code.

  This work will appear in TRANSACT at FCRC 2011. PDF, PDF with full semantics, Coq code. (That tarball includes a copy of the Metatheory library for Coq 8.2 (available here) - we had to make a one-line change in order to get it working with Coq's FMap library.)

• Abstract Signatures for Proving Escape Actions are Unobservable: Many transactional-memory systems include "back doors" that let programmers include code that is not part of the transaction and is not undone if the transaction fails to commit. Open nesting and escape actions are similar constructs that achieve this effect. These constructs are difficult to use correctly. We are proposing one quite-strict definition of correctness: that outside of some abstraction boundary, the code with an escape action should be observationally equivalent to similar code where the action is part of the transaction. We are identifying proof techniques for establishing correctness under this definition. Like in representation-independence proofs, the use of abstract signatures is essential.

Current contacts: Laura Effinger-Dean, Matthew Kehrt, Dan Grossman

Relevant publications:

• High-Level Small-Step Operational Semantics for Transactions (POPL 2008)
      Katherine F. Moore and Dan Grossman
  Note: An earlier version was presented informally at TRANSACT 2007.
• Software Transactions Meet First-Class Continuations (SCHEME 2007)
      Aaron Kimball and Dan Grossman
• The Transactional Memory / Garbage Collection Analogy (OOPSLA 2007)
      Dan Grossman
• Enforcing Isolation and Ordering in STM (PLDI 2007)
      Tatiana Shpeisman, Vijay Menon, Ali-Reza Adl-Tabatabai, Steve Balensiefer, Dan Grossman, Richard Hudson, Katherine F. Moore, and Bratin Saha
• Atomicity via Source-to-Source Translation (MSPC 2006)
      Benjamin Hindman and Dan Grossman
  Note: TR 2006-05-01 is an expanded description of this work.
• What Do High-Level Memory Models Mean for Transactions? (MSPC 2006)
      Dan Grossman, Jeremy Manson, and William Pugh
  
• AtomCaml: First-Class Atomicity via Rollback (ICFP 2005)
      Michael F. Ringenburg and Dan Grossman

Available software (download after following links):

• AtomCaml
• AtomEclipse
• AtomJava
• AtomScheme