An Abort-Aware Model of Transactional Programming

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 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, ...

• Type: Conference
• Year: 2009
• Where: VMCAI
• Authors: Kousha Etessami, Patrice Godefroid
• Keywords: Concurrent Programming, Model Checking, Nested Transactions, Software Engineering, VMCAI 2009