High-level small-step operational semantics for transactions

Software transactions have received significant attention 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 transThese languages abstract away implementation details of transactional memory, providing high-level definitions suitable for programming languages. We use small-step semantics in order to represent explicitly the interleaved execution of threads that is necessary to investigate pertinent issues. 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 th...

• Type: Conference
• Year: 2008
• Where: POPL
• Authors: Katherine F. Moore, Dan Grossman
• Keywords: Key Language-equivalence Theorems, Mutable Memory Location, POPL 2008, Programming Languages, Sufficient Static Restrictions