The Taub Faculty of Computer Science Events and Talks

Transactional memory is a promising mechanism for synchronizing concurrent programs. There has been a lot of research in the past decade in implementing transactional memory. However, relatively little attention has been paid to precisely specifying what it means for them to be correct, which is necessary to reason rigorously about transactional memory.

I will discuss some of the issues with such specifications, and why there is not a single "correct" specification. I will present several specifications, including formal specifications that we have used to formally verify transactional memory algorithms. I will also describe work on a proposal for adding transactional memory support to C++, and discuss some of the pragmatic issues that arise in developing such a proposal. Bio:
Victor Luchangco is a Principal Member of Technical Staff in the Scalable Synchronization and Programming Languages Research Groups of Oracle Labs. His research focuses on developing algorithms and mechanisms to support concurrent programming on large-scale distributed systems. A theoretician by disposition and training, Victor is also interested in practical aspects of computing. In particular, he would like to design mechanisms that practical for real computers. In addition, he is interested in exploring how to make proofs for concurrent systems easier, both by changing how people design these systems and by using tools to aid in formal verification. Victor received an Sc.D. in Computer Science from MIT in 2001, with a dissertation on models for weakly consistent memories.