@booklet {DDLS2011, title = {StarTM: Automatic Verification of Snapshot Isolation in Transactional Memory Java Programs}, number = {UNL-DI-6-2011}, year = {2011}, note = {

n/a

}, publisher = {Departamento de Inform{\'a}tica FCT/UNL}, abstract = {

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.

}, attachments = {https://docentes.fct.unl.pt/sites/default/files/joao-lourenco/files/ddls11.pdf}, author = {Ricardo J. Dias and Dino Distefano and Jo{\~a}o M. Louren{\c c}o and Jo{\~a}o Costa Seco} }