Semantics of Transactional Memory and Automatic Mutual Exclusion
Martín Abadi, Andrew Birrell, Tim Harris and Michael Isard
Proc. Symp. Principles of Programming Languages, 63-74 (2008)
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 problematic. 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 semantics and type
systems for the constructs of the Automatic Mutual 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 concurrency, lazy conflict detection, and
roll-back. These strategies are correct only under non-trivial
assumptions that we identify and analyze. One important source of
errors is that some efficient implementations create dangerous
"zombie" computations where a transaction keeps running after
experiencing a conflict; the assumptions confine the effects of these
computations.
Click here for a pdf
version
Back to
Michael Isard's home page