Verification Tools for Transactional Programs
Published in Transactional Memory. Foundations, Algorithms, Tools, and Applications, Springer, 2015
Recommended citation: Adrian Cristal, Burcu Kulahcioglu Ozkan, Ernie Cohen, Gokcen Kestor, Ismail Kuru, Osman Unsal, Serdar Tasiran, Suha Orhun Mutluergil, Tayfun Elmas. "Verification Tools for Transactional Programs. Transactional Memory. Foundations, Algorithms, Tools, and Applications, Springer.
Abstract. While transactional memory has been investigated intensively, its use as a programming primitive by application and system builders is only recently becoming widespread, especially with the availability of hardware support in mainstream commercial CPUs. One key benefit of using transactional memory while writing applications is the simplicity of not having to reason at a low level about synchronization. For this to be possible, verification tools that are aware of atomic blocks and their semantics are needed. While such tools are clearly needed for the adoption of transactional memory in real systems, research in this area is quite preliminary. In this chapter, we provide highlights of our previous work on verification tools for transactional programs.