Kate Moore, University of Washington

High-Level, Small-Step Operational Semantics for Software Transactions


Abstract:

Software transactions have received significant attentions as a way to
simplify shared-memory concurrent programming, but insufficient focus
has been given to the precise meaning of software transactions or
their interaction with other language features.  This work begins to
rectify that situation by presenting a family of formal languages that
model a wide variety of behaviors for software transactions.  These
languages abstract away implementation details of transactional
memory, providing high-level definitions suitable for programming
languages.  We demonstrate the value of our core approach to modeling
transactions by investigating two issues in depth.
First, we consider parallel nesting, in which parallelism and
transactions can nest arbitrarily.  Second, we present multiple models
for weak isolation, in which nontransactional code can violate the
isolation of a transaction.  For both, type-and-effect systems let us
soundly and statically restrict what computation can occur inside or
outside a transaction.