An Abort-Aware Model of Transactional Programming

Kousha Etessami, Patrice Godefroid

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

There has been a lot of recent research on transaction-based concurrent programming, aimed at offering an easier concurrent programming paradigm that enables programmers to better exploit the parallelism of modern multi-processor machines, such as multi-core microprocessors. 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 concurrent 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 simultaneously be executing inside transactions. It also allows nested transactions, transactions which may never terminate, and transactions which may be aborted explicitly, or aborted automatically by the run-time environment due to memory conflicts.

We show that concurrent executions of TSMs satisfy a correctness criterion 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.
Original languageEnglish
Title of host publicationVerification, Model Checking, and Abstract Interpretation
Subtitle of host publication10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings
EditorsNeil D. Jones, Markus Mueller-Olm
PublisherSpringer-Verlag GmbH
Number of pages15
ISBN (Electronic)978-3-540-93900-9
ISBN (Print)978-3-540-93899-6
Publication statusPublished - 2009

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Dive into the research topics of 'An Abort-Aware Model of Transactional Programming'. Together they form a unique fingerprint.

Cite this