Transactions in the jungle

Transactional memory (TM) has shown potential to simplify the task of writing concurrent programs. Inspired by classical work on databases, formal definitions of the semantics of TM executions have been proposed. Many of these definitions assumed that accesses to shared data are solely performed through transactions. In practice, due to legacy code and concurrency libraries, transactions in a TM have to share data with non-transactional operations. The semantics of such interaction, while widely discussed by practitioners, lacks a clear formal specification. Those interactions can vary, sometimes in subtle ways, between TM implementations and underlying memory models. We propose a correctness condition for TMs, parametrized opacity, to formally capture the now folklore notion of strong atomicity by stipulating the two following intuitive requirements: first, every transaction appears as if it is executed instantaneously with respect to other transactions and non-transactional oper...

• Type: Conference
• Year: 2010
• Where: SPAA
• Authors: Rachid Guerraoui, Thomas A. Henzinger, Michal Kapalka, Vasu Singh
• Keywords: Distributed And Parallel Computing, Memory Models, Non-transactional Operations, Parametrized Opacity, SPAA 2010