Semantics of transactional memory and automatic mutual exclusion

Authors:
Open Access
Publisher website
Google Scholar
Abstract
Software Transactional Memory (STM) is an attractive basis for the development of language features for concurrent programming. However, the semantics of these features can be delicate and prob- lematic. In this paper we explore the tradeoffs between semantic simplicity, the viability of efficient implementation strategies, and the flexibility of language constructs. Specifically, we develop se- mantics and type systems for the constructs of the Automatic Mu- tual Exclusion (AME) programming model; our results apply also to other constructs, such as atomic blocks. With this semantics as a point of reference, we study several implementation strategies. We model STM systems that use in-place update, optimistic con- currency, lazy conflict detection, and roll-back. These strategies are correct only under non-trivial assumptions that we identify and an- alyze. One important source of errors is that some efficient imple- mentations create dangerous "zombie" computations where a trans- action keeps running after experiencing a conflict; the assumptions confine the effects of these computations.

This publication has 20 references indexed in Scilit: