Research Abstracts - 2007

Introduction

Open-nested transactions have been proposed as a loophole [6] for transactional memory (TM) to increase concurrency on highly contended resources in transactional programs. Programs that use open nesting can be difficult to reason about because open nesting breaks serializability at the level of memory semantics. Evidence suggests that an unconstrained use of open nesting cannot cannot be encapsulated, i.e., that programmers may need to be aware of whether subroutines contain open-nested transactions.

In [1], we define a framework for defining and exploring the memory semantics of open nesting in a transactional-memory setting. Our framework allows us to define the traditional model of serializability and two new transactional-memory models, race freedom and prefix race freedom. The weakest of these memory models, prefix race freedom, resembles the Stanford open-nesting semantics described in the TCC TM system [5]. We prove that these three memory models are equivalent for transactional-memory systems that support only closed nesting, as long as aborted transactions are ``ignored.'' We prove that for systems that support open nesting, however, the models of serializability, race freedom, and prefix race freedom are distinct. We show that the TCC system implements a model at least as strong as prefix race freedom and strictly weaker than race freedom. We also present examples which show that more generally, hardware proposals for open-nesting such as [5, 6] compromise serializability, the property traditionally used to reason about the correctness of transactions.

Background on Transactional Memory and Open Nesting

Atomic transactions represent a well-known and useful abstraction for programmers writing parallel code. Recently, transactional memory [4] has become an active area of research. Transactional memory (TM) describes a collection of hardware and software mechanisms that provide a transactional interface for accessing memory. A TM system guarantees that any section of code that the programmer has specified as a transaction either appears to execute atomically or appears not to happen at all, even though other transactions may be running concurrently. A TM system enforces atomicity by tracking the memory locations that each transaction in the system accesses, finding transaction conflicts, and aborting and possibly retrying transactions to resolve conflicts. In general, TM systems guarantee that transactions are serializable.

Although ordinary TM presents the programmer with simple semantics, these semantics provide no way for the programmer to tell the TM system to ignore a conflict which abstractly he/she deems as safe. Moss and Hosking in [6] proposed adapting the notion of open-nested transactions, an idea from database systems, for use in transactional memory. If a transaction A contains a subtransaction B which is open-nested inside A, then intuitively, the TM system "ignores" the memory locations accessed by B when checking for conflicts with A.

Proposed hardware support open nesting mechanisms (e.g., [5, 6]) allow programmers to avoid such conflicts by breaking physical serializability. By allowing some nonserializable behaviors, however, these mechanisms also permit other arguably anomalous behaviors, even in the case where all transactions commit [1]. For example, Figure 1 shows a program execution permitted by hardware open nesting mechanisms in which transaction A is not physically serializable. After A's open-nested transaction B commits, it is possible for a concurrent transaction C to depend on values committed by B (e.g., w ) and then itself commit and change values (e.g., y) which the remainder of A depends on. Existing hardware open nesting proposals do not detect a conflict between A and C; therefore, these systems permit a program execution in which A is neither physically serializable before or after C.

TM systems which guarantee only a transactional memory model of prefix race-freedom permit program executions such as the one in Figure 1. In [1], we formally define prefix race-freedom and show that [5]'s open-nesting semantics implements this memory model. We also prove that prefix race-freedom and serializability are equivalent for programs with only closed-nested transactions, but different for programs with open-nested transactions.

Unlike TM without open nesting, a system that guarantees only prefix race-freedom no longer provides guarantees of modularity and composability. With unconstrained sharing of data between transactions, the correctness of a transaction A with an open-nested transaction B no longer depends locally on A's code because other transactions C may interleave with A's execution. In fact, this problem extends to any of A's ancestor transactions. Thus, a programmer using a subroutine needs to be aware whether that subroutine contains open-nested transactions. Without higher-level abstractions, programmers can not easily reason about their code because the effects of open-nested transactions cannot be encapsulated.

Transactional Computation Framework

In [1], we describe a framework for transactional computations which permits an a posteriori analysis of a program's execution on a TM system. The framework assumes a program execution generates a trace which is abstractly represented as a pair (C, Φ), where C is a ``computation tree'' that summarizes both the information about the control structure of a program and the nesting structure of transactions, and Φ is an ``observer function'' that describes the behavior of read and write operations.

The computation tree C is an ordered tree with two types of nodes: memory-operation nodes as leaves and control nodes as internal nodes. Each memory operation node represents either a read from or a write to a single memory location l. Control nodes capture the computation's parallel structure. If X is labeled as an S-node, its children are executed in series from left to right. Otherwise, X is a P-node, and its children can be executed in parallel. As we describe in [1], from C we can construct a computation dag G(C). Intuitively, every internal node X corresponds to a subdag G(X) represented by the subtree of C rooted at X. In the framework, we mark some subset of internal nodes as transactions. If X is so marked, then G(X) is a transaction. Figure 2 illustrates an example computation tree C and its corresponding dag G(C).

Instead of specifying the value that an operation reads or writes to a memory location l, we follow the computation-centric framework described by Frigo and Luchangco in [2, 3] and abstract away the values entirely using an observer function Φ. In the computation dag, consider a memory operation v that either reads from or writes to a memory location l. The node Φ(v) is defined to be the operation that wrote the value of l that v sees.

In the framework, it turns out that a memory model is defined as a subset of traces ``allowed'' by that model. In [1], we define two transactional memory models, race-freedom and prefix race-freedom. We prove that these models are equivalent to serializability for computations with only closed-nested, committed transactions, but distinct when computations have open-nested transactions.

Informally, the memory model of prefix race-freedom is the set of all traces (C, Φ) such that there exists a topological sort S of the computation dag G(C) that satisfies two conditions. First, for all memory operations v that read from or write to a location l, the node Φ(v) is the last node in the sort order S which precedes v, writes to location l, and is not ``hidden from'' v because of an aborted transaction. Second, for every memory operation u ``belonging to'' a transaction T, in the order S there should be no operations w belonging to an independent transaction that appear between xbegin(T) and u which ``conflict'' with u. Race-freedom strengthens the second guarantee of prefix race-freedom, to require that there are no operations w between xbegin(T) and xend(T) which ``conflict'' with u. Serializability offers the strongest requirement, that no operations w from an independent transaction can appear between xbegin(T) and xend(T).

Future Work

The results in [1] suggests that an unconstrained use of open nesting cannot cannot be encapsulated, i.e., that programmers may need to be aware of whether subroutines contain open-nested transactions. It appears that higher-level abstractions are necessary for programmers to be able to abstractly recover serializability. For example, [7] describes a software TM implementation of open nesting which breaks physical serializability, but provides some high-level language constructs to enable encapsulation.

We hope to incorporate higher-level abstractions into our theoretical model for TM, and continue to explore loopholes such as open nesting. This exploration will hopefully facilitate the construction of a structured programming model which provides programmers with provable guarantees that they can use to reason about their code. We are optimistic that serializability can be recovered abstractly in a TM system by providing the programmer with simple but unobtrusive guidelines and language constructs that provably encapsulate the effects of open-nested transactions.

Research Support

This research was supported in part by NSF Grants CNS-0615215 and CNS-0540248, and a grant from Intel Corporation.

References:

[1] Kunal Agrawal, Charles E. Leiserson, and Jim Sukha. Memory Models for Open-Nested Transactions. In Proceedings of the ACM SIGPLAN Workshop on Memory Systems Performance and Correctness (MSPC), San Jose, CA USA, October 2006.

[2] Matteo Frigo. The Weakest Reasonable Memory Model. Master's thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, January 1998.

[3] Matteo Frigo and Victor Luchangco. Computation-Centric Memory Models. In Proceedings of the ACM Symposium on Parallel Algorithms and Architectures (SPAA), pages 240-249, 1998.

[4] Maurice Herlihy and J. Eliot B. Moss. Transactional Memory: Architectural Support for Lock-Free Data Structures. In Proceedings of the International Symposium on Computer Architecture (ISCA), pages 289 - 300, 2003.

[5] Austen McDonald, JaeWoong Chung, Brian D. Carlstrom, Chi Cao Minh, Hassan Chafi, Christos Kozyrakis, and Kunle Olukotun. Architectural Semantics for Practical Transactional Memory. In Proceedings of the International Symposium on Computer (ISCA), June 2006.

[6] J. Eliot B. Moss and Antony L. Hosking. Nested Transactional Memory: Model and Architecture Sketches. In Science of Computer Programming, volume 63, pages 186 - 201. Elsevier, Dec 2006.

[7] Yang Ni, Vijay Menon, Ali-Reza Adl-Tabatabai, Antony L. Hosking, Richard L. Hudson, J. Eliot B.Moss, Bratin Saha, and Tatiana Shpeisman. Open Nesting in Software Transactional Memory. In Proceedings of Principles and Practice of Parallel Programming (PPoPP), March 2007.