ECOOP 2012 - Object-Oriented Programming
ECOOP 2012 - Object-Oriented Programming
复制标题
ECOOP 2012 - 面向对象编程
DOI：
10.1007/978-3-642-31057-7_28
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Dias R
中科院分区：
文献类型：
--
作者：
Dias R
本文提出了一种在快照隔离级别下执行的事务内存 Java 程序的自动验证技术。我们验证程序中的哪些事务可以在快照隔离下安全执行，而不会触发写入偏斜异常，从而为运行时优化开辟了道路，从而可能带来显着的性能增强。我们的工作建立在一种新颖的深堆分析技术之上，该技术基于分离逻辑，静态地近似事务内存 Java 程序的读取和写入集。我们实现了我们的技术，并将我们的工具应用于一组微基准测试和 也是 STAMP 包的一项基准。我们证实了已知的结果，通过证明不存在写入偏斜异常来验证一些在快照隔离下安全执行的示例。在其他情况下，我们的分析发现了可能触发先前未知的写入偏斜异常的事务。
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 thewrite-skewanomaly, 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 ofwrite-skewanomalies. In other cases our analysis has identified transactions that potentially trigger previously unknownwrite-skewanomalies.