On the Correctness of Transactional Memory

Transactional memory (TM) is perceived as an appealing alternative to critical sections for general purpose concurrent programming. Despite the large amount of recent work on TM implementations, however, very little effort has been devoted to precisely define what guarantees these implementations should provide. A formal description of such guarantees is necessary in order to check the correctness of TM systems, as well as to establish TM optimality results and inherent trade-offs. This paper presents opacity, a candidate correctness criterion for TM implementations. We define opacity as a property of concurrent transaction histories and give its graph theoretical interpretation. Opacity captures precisely the correctness requirements that have been intuitively described by many TM designers. Most TM systems we know of do ensure opacity. At a very first approximation, opacity can be viewed as an extension of the classical database serializability property with the additional requirement that even non-committed transactions are prevented from accessing inconsistent states. Capturing this requirement precisely, in the context of general objects, and without precluding pragmatic strategies that are often used by modern TM implementations, such as versioning, invisible reads, lazy updates, and open nesting, is not trivial. As a use case of opacity, we prove the first lower bound on the complexity of TM implementations. Basically, we show that every single-version TM system that uses invisible reads and does not abort non-conflicting transactions requires, in the worst case, Ω(k) steps for an operation to terminate, where k is the total number of objects shared by the transactions. This (tight) bound precisely captures an inherent trade-off in the design of TM systems. The bound also highlights a fundamental gap between systems in which transactions can be fully isolated from the outside environment, e.g., databases or certain specialized transactional languages, and systems that lack such isolation capabilities, e.g., general TM frameworks.

Why STM can be more than a Research Toy

Aleksandar Dragojevic, Pascal Felber, Vincent Gramoli, Rachid Guerraoui

Software Transactional Memory (STM) promises to simplify concurrent programming without requiring speciﬁc hardware support. Yet, STM’s credibility lies on the extent to which it can leverage multi-cores to outperform sequential code. A recent CACM paper [8] questioned however the ability of STMs to provide good performance and suggested their conﬁnement to a research toy. This paper revisits those conclusions through the most to date extensive comparison of STM performance to sequential code. We evaluate a state-of- the-art STM system, SwissTM, on a wide range of benchmarks and two different multicore systems. We dissect the inherent costs of synchronization as well as the overheads of compiler instrumentation and transparent privatization. Our results show that an STM with manually instrumented benchmarks and explicit privatization outperforms sequential code by up to 29 times on SPARC with 64 concurrent threads and by up to 9 times on x86 with 16 concurrent threads. Indeed the overheads of compiler instrumentation and transparent privatization are substantial, yet they do not prevent STM from generally outperforming sequential code.

2009

Why STM can be more than a Research Toy

Aleksandar Dragojevic, Pascal Felber, Vincent Gramoli, Rachid Guerraoui

Software Transactional Memory (STM) promises to simplify concurrent programming without requiring specific hardware support. Yet, STM’s credibility lies on the extent to which it enables to leverage multicores and outperform sequential code. A recent CACM paper [3] questioned this ability and suggested the confinement of STM to a research toy. We revisit these conclusions through the most to date extensive comparison of STM performance to sequential code. We evaluate a state-of-the-art STM system, SwissTM, on a wide range of benchmarks and two different multicore systems. We dissect the inherent costs of synchronization as well as the overheads of compiler instrumentation and transparent privatization. Our results show that an STM with manually instrumented benchmarks and explicit privatization outperforms sequential code by up to 29 times on SPARC with 64 concurrent threads and by up to 9 times on x86 with 16 concurrent threads. Indeed the overheads of compiler instrumentation and transparent privatization are substantial, yet they do not prevent STM from generally outperforming sequential code.

2011

Opacity: A Correctness Condition for Transactional Memory

Rachid Guerraoui, Michal Kapalka

Transactional memory is perceived as an appealing alternative to critical sections for general purpose concurrent programming. Despite the large amount of recent work on transactional memory implementations, however, its actual specification has never been precisely defined. This paper presents \emph{opacity}, a new correctness criterion for transactional memory systems. Opacity extends the notion of strict serializability, itself a strong form of the classical serializability property, with the requirement that even \emph{non-committed} transactions are prevented from accessing inconsistent state. Yet opacity does not preclude versioning, invisible reads and lazy updates, often used by modern TM implementations. In fact, most transactional memory systems we know of ensure opacity. We prove a tight bound on the inherent cost of implementing opacity. The bound highlights a trade-off that explains some of the differences between current transactional memory systems, and also draws a sharp complexity line between opacity on one hand, and the combination of strict serializability and strict recoverability on the other hand.

2007