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.

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.