The Taub Faculty of Computer Science Events and Talks

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.