We have a long-standing interest in using atomic blocks (e.g., atomic { s }), where s is a statement as a synchronization primitive that is easier-to-use but harder-to-implement than conventional synchronization primitivites, such as mutual-exclusion locks. Atomic blocks are often implemented using transactional memory. Many language design and semantics isssues arise from their interaction with other language features. We have done work on design, theory, and implementation for a variety of languages, including Caml, Java, Haskell, Scheme, and x86 assembly.

Some of this work was done in collaboration with Intel, AMD, and the University of Maryland.

Available software (download after following links):

Additional materials from the work on region-based dynamic separation for STM Haskell (as presented at TRANSACT 2011): PDF with full semantics, Coq code. (That tarball includes a copy of the Metatheory library for Coq 8.2 - we had to make a one-line change in order to get it working with Coq's FMap library.)