Implementations of Software Transactional Memory (STM) algorithms associate metadata with the memory locations accessed during a transaction’s lifetime. This metadata may be stored either in-place, by wrapping every memory cell in a container that includes the memory cell itself and the corresponding metadata; or out-place (also called external), by resorting to a mapping function that associates the memory cell address with an external table entry containing the corresponding metadata. The implementation techniques for these two approaches are very different and each STM framework is usually biased towards one of them, only allowing the efficient implementation of STM algorithms following that approach, hence inhibiting the fair comparison with STM algorithms falling into the other. In this paper we introduce a technique to implement in-place metadata that does not wrap memory cells, thus overcoming the bias by allowing STM algorithms to directly access the transactional metadata. The proposed technique is available as an extension to the DeuceSTM framework, and enables the efficient implementation of a wide range of STM algorithms and their fair (unbiased) comparison in a common STM infrastructure. We illustrate the benefits of our approach by analyzing its impact in two popular TM algorithms with two different transactional workloads, TL2 and multi-versioning, with bias to out-place and in-place respectively.

Typical Distributed Transactional Memory (DTM) systems provide serializability by detecting read-write conflicts between accesses to shared data objects. Detecting read-write conflicts requires the bookkeeping of all the read and write accesses to the shared objects made inside the transaction, and the validation of all these accesses in the end of a transaction. For most DTM algorithms, the validation of a transaction requires the broadcast of its read-set to all the nodes of the distributed system during the commit phase. Since applications tend to read more than write, the overhead associated with the bookkeeping of read accesses, and the amount of network traffic generated during the commit, is a main performance problem in DTM systems. Database systems frequently rely on weaker isolation models to improve performance. In particular, Snapshot Isolation (SI) is widely used in industry. An interesting aspect of SI is that only write-write conflicts are checked at commit time and considered for detecting conflicting transactions. As main result, a DTM using this isolation model does not need to keep track of the read accesses, considerably reducing the bookkeeping overhead, and also eliminates the need of broadcasting the read-set at transaction commit time, thus reducing the network traffic and considerably increase the scalability of the whole system. By only detecting write-write conflicts, this isolation model allows a much higher commit rate, which comes at the expense of allowing some real conflicting transactions to commit. Thus, relaxing the isolation of a transactional program may lead previously correct programs to misbehave due to the anomalies resulting from malign data-races that are now allowed by the relaxed transactional run-time. These anomalies can be precisely characterized, and are often called in the literature as write-skew anomalies. Write-skew anomalies can be avoided dynamically with the introduction of algorithms that verify the serializability of running transactions, which may result in a non-negligible overhead. Our approach is to avoid the run-time overhead by statically asserting that a DTM program will execute without generating write-skew anomalies at runtime, while only verifying write-write conflicts. Conflicting transactions can be made “safe” by code rewriting using well known techniques. Our verification technique uses separation logic, a logic for verifying intensive heap manipulation programs, which was extended to construct abstract read- and write-sets for each transaction in the DTM program. This verification technique is implemented in the StarTM tool, which analyzes transactional Java bytecode programs. The transactions that cannot be verified by our tool are executed under serializable isolation (detecting read-write conflicts), while for the “safe” transactions we only detect write-write conflicts. The results of our experiments when verifying micro-benchmarks, such as linked lists and binary trees, and partially verifying some macro-benchmarks, such as the STAMP benchmark, strongly encourage the ongoing work for the application of this technique to DTM.

n/a

n/a

Several Software Transactional Memory (STM) algorithms have been developed in the last few years. These algorithms differ in many different properties, such as progress and safety guarantees, contention management, etc. Some STM frameworks (DSTM2, DeuceSTM) were developed to allow the implementation and comparison of many different algorithms using the same transactional interface. The information required by an STM algorithm is either associated with the execution of a transaction (frequently referred as transaction descriptor), or associated with each memory location (or object reference) accessed within the transaction. The transaction descriptor is typically stored in a thread-local memory space and maintains the information necessary to validate and commit a memory transaction. The information associated with each memory location depends on the nature of the STM algorithm, which we will henceforth refer to as metadata, and may be composed by e.g. locks, timestamps or version lists. Since metadata is associated with each memory location, there are two main strategies regarding the location for storing such metadata: The metadata is stored either near each memory location (in-place strategy); or in a mapping table that associates the metadata with the corresponding memory location (out- place strategy). DeuceSTM is one of the most efficient STM frameworks available for the Java programming language and provides a well defined interface that allows to implement several STM algorithms using an out-place strategy. This work describes the adaptation and extension of DeuceSTM to support the in-place metadata strategy. Our approach complies to the following properties: Efficiency –- The STM implementation does not rely on an auxiliary mapping table, thus providing faster direct access to the transactional metadata; Non-transactional code is oblivious to the presence of metadata in objects, hence there is no performance overhead whatsoever for non-transactional code; Transactional code avoids the extra memory dereference imposed by the decorator pattern; Primitive types are fully supported, even in transactional code; And we provide a solution for fully supporting transactional N-dimensional arrays, which again impose no overhead on non-transactional code. Transparency –- The STM implementation automatically identifies, creates and initializes the necessary additional metadata fields in the objects; Non-transactional code is oblivious to the presence of metadata in objects, hence no code changes are required; The new transactional array types (supporting metadata for individual cells) are compatible with the standard arrays, hence not requiring any pre-/post- processing of the arrays when invoking standard or third-party non-transactional libraries. Performance benchmarking has confirmed that our approach for supporting in-place metadata in DeuceSTM, alongside with the existing out-place strategy, is a valid functional complement, widening the range of algorithms that can be efficiently implemented in DeuceSTM, enabling their fair comparison in a common infrastructure.

This paper presents StarTM , an automatic verification tool for transactional memory Java programs executing under relaxed isolation levels. We certify which transactions in a program are safe to execute under Snapshot Isolation without triggering the write-skew anomaly, opening the way to run-time optimizations that may lead to considerable performance enhancements.
Our tool builds on a novel shape analysis technique based on Separation Logic to statically approximate the read- and write-sets of a transactional memory Java program. This technique is particularly challenging due to the presence of dynamically allocated memory.
We implement our technique and apply our tool to a set of intricate examples. We corroborate known results, certifying some of the examples for safe execution under Snapshot Isolation by proving the absence of write-skew anomalies. In other cases we identify transactions that potentially trigger the write-skew anomaly.

Software Transactional Memory algorithms associate metadata with the memory locations accessed during a transaction’s lifetime. This metadata may be stored in an external table and accessed by way of a function that maps the address of each memory location with the table entry that keeps its metadata (this is the out-place or external scheme); or alternatively may be stored adjacent to the associated memory cell by wrapping them together (the in-place scheme). In transactional memory multi-version algorithms, several versions of the same memory location may exist. The efficient implementation of these algorithms requires a one-to-one correspondence between each memory location and its list of past versions, which is stored as metadata. In this chapter we address the matter of the efficient implementation of multi-version algorithms in Java by proposing and evaluating a novel in-place metadata scheme for the Deuce framework. This new scheme is based in Java Bytecode transformation techniques and its use requires no changes to the application code. Experimentation indicates that multi-versioning STM algorithms implemented using our new in-place scheme are in average 6× faster than when implemented with the out-place scheme.

This paper presents an automatic verification technique for transactional memory Java programs executing under snapshot isolation level. We certify which transactions in a program are safe to execute under snapshot isolation without triggering the write-skew anomaly, opening the way to run-time optimizations that may lead to considerable performance enhancements. Our work builds on a novel deep-heap analysis technique based on separation logic to statically approximate the read- and write-sets of a transactional memory Java program. We implement our technique and apply our tool to a set of micro benchmarks and also to one benchmark of the STAMP package. We corroborate known results, certifying some of the examples for safe execution under snapshot isolation by proving the absence of write-skew anomalies. In other cases our analysis has identified transactions that potentially trigger previously unknown write-skew anomalies.

Concurrent programs may suffer from concurrency anomalies that may lead to erroneous and unpredictable program behaviors. To ensure program correctness, these anomalies must be diagnosed and corrected. This paper addresses the detection of both low- and high-level anomalies in the Transactional Memory setting. We propose a static analysis procedure and a framework to address Transactional Memory anomalies. We start by dealing with the classic case of low-level dataraces, identifying concurrent accesses to shared memory cells that are not protected within the scope of a memory transaction. Then, we address the case of high-level dataraces, bringing the programmer's attention to pairs of memory transactions that were misspecified and should have been combined into a single transaction. Our framework was applied to a set of programs, collected form different sources, containing well known low- and high-level anomalies. The framework demonstrated to be accurate, confirming the effectiveness of using static analysis techniques to precisely identify concurrency anomalies in Transactional Memory programs.