<?xml version="1.0" encoding="UTF-8"?><xml><records><record><source-app name="Biblio" version="6.x">Drupal-Biblio</source-app><ref-type>47</ref-type><contributors><authors><author><style face="normal" font="default" size="100%">Ricardo Jorge Dias</style></author><author><style face="normal" font="default" size="100%">Dino Distefano</style></author><author><style face="normal" font="default" size="100%">João Costa Seco</style></author><author><style face="normal" font="default" size="100%">João Manuel Lourenço</style></author></authors></contributors><titles><title><style face="normal" font="default" size="100%">Verification of Snapshot Isolation in Transactional Memory Java Programs</style></title><secondary-title><style face="normal" font="default" size="100%">Proceedings of the 26th European Conference on Object-Oriented Programming</style></secondary-title><tertiary-title><style face="normal" font="default" size="100%">{ECOOP}</style></tertiary-title></titles><dates><year><style  face="normal" font="default" size="100%">2012</style></year><pub-dates><date><style  face="normal" font="default" size="100%">11-16 June</style></date></pub-dates></dates><urls><related-urls><url><style face="normal" font="default" size="100%">https://docentes.fct.unl.pt/sites/default/files/joao-lourenco/files/ecoop12.pdf</style></url></related-urls></urls><pub-location><style face="normal" font="default" size="100%">Beijing, China</style></pub-location><language><style face="normal" font="default" size="100%">eng</style></language><abstract><style face="normal" font="default" size="100%">&lt;p&gt;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.&amp;gt;&lt;/p&gt;
</style></abstract><notes><style face="normal" font="default" size="100%">&lt;p&gt;n/a&lt;/p&gt;
</style></notes></record></records></xml>