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 implementation of dynamic separation had several novel extensions. First, we improved support for mutable data structures by providing protection regions, special objects that hold the protection state for multiple references. Second, we expanded the set of protection states so that the interface is more expressive. Third, we allowed transactions to modify the protection state of references.
- 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