Skip to content (access key 's')
Logo of Technion
Logo of CS Department
Logo of CS4People

The Taub Faculty of Computer Science Events and Talks

CSL Luncheon: A Programming Language Perspective on Transactional Memory Consistency
event speaker icon
Sandeep Hans
event date icon
Thursday, 30.05.2013, 12:30
event location icon
Room 337-8 Taub Bld.
Advisor: Hagit Attiya
Transactional memory (TM) has been hailed as a paradigm for simplifying concurrent programming. While several consistency conditions have been suggested for TM, they are stated as conditions on possible histories that implementations may export. This leaves a striking disconnect with programming language abstractions providing atomic blocks to the programmer. This paper presents the first connection between the observations exported by histories satisfying TM consistency conditions and those expected with a simple programming abstraction using atomic blocks. We prove that a variant of opacity is a necessary and sufficient condition for providing observational refinement that preserves the views of every thread. These results provide a new way to evaluate and compare TM consistency conditions. Further, they also reduce the effort of verifying that a TM satisfies the language abstractions, relying instead on proving only that it ensures opacity, as was already done for many TM implementations.