An Abort-Aware Model of Transactional Programming

Abstract. There has been a lot of recent research on transaction-based concurrent programming, aimed at offering an easier concurrent pro-gramming paradigm that enables programmers to better exploit the par-allelism of modern multi-processor machines, such as multi-core micro-processors. We introduce Transactional State Machines (TSMs) as an abstract finite-data model of transactional shared-memory concurrent programs. TSMs are a variant of concurrent boolean programs (or con-current extended recursive state machines) augmented with additional constructs for specifying potentially nested transactions. Namely, some procedures (or code segments) can be marked as transactions and are meant to be executed “atomically”, and there are also explicit commit and abort operations for transactions. The TSM model is non-blocking and allows interleaved executions where multiple processes can simulta-neously be executing inside transactions. It also allows nested transac-tions, transactions which may never terminate, and transactions which may be aborted explicitly, or aborted automatically by the run-time en-vironment due to memory conflicts. We show that concurrent executions of TSMs satisfy a correctness crite-rion closely related to serializability, which we call stutter-serializability, with respect to shared memory. We initiate a study of model checking problems for TSMs. Model checking arbitrary TSMs is easily seen to be undecidable, but we show it is decidable in the following case: when recursion is exclusively used inside transactions in all (but one) of the processes, we show that model checking such TSMs against all stutter-invariant ω-regular properties of shared memory is decidable.