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.
] 