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