An Abort-Aware Modelof Transactional Programming

摘要

There has been a lot of recent research on transaction-basedconcurrent programming, aimed at offering an easier concurrentprogramming paradigm that enables programmers to better exploit theparallelism of modern multi-processor machines, such as multi-core mi-croprocessors. We introduce Transactional State Machines (TSMs) as anabstract finite-data model of transactional shared-memory concurrentprograms. TSMs are a variant of concurrent boolean programs (or con-current extended recursive state machines) augmented with additionalconstructs for specifying potentially nested transactions. Namely, someprocedures (or code segments) can be marked as transactions and aremeant to be executed "atomically", and there are also explicit commitand abort operations for transactions. The TSM model is non-blockingand 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 whichmay be aborted explicitly, or aborted automatically by the run-time en-vironment due to memory conflicts.