Abstract:

Guerraoui and Kapalka defined opacity as a safety criterion for transactional memory algorithms in 2008.

Researchers have shown how to prove opacity, while little is known about pitfalls that can lead to non-opacity. We identify two problems that lead to non-opacity, we present automatic tool support for finding those problems, and we prove an impossibility result.

We first show that the well-known TM algorithms DSTM and McRT don't satisfy opacity. DSTM suffers from a write-skew anomaly, while McRT suffers from a write- exposure anomaly.

We then prove that for direct-update TM algorithms, opacity is incompatible with a liveness criterion called local progress, even for fault-free systems. Our result implies that if TM algorithm designers want both opacity and local progress, they should avoid direct-update algorithms. Joint work with Mohsen Lesani that we will present at DISC 2013 and have presented at TRANSACT 2013 under the title "Proving non-opacity".

About the speaker: 

Jens Palsberg is Professor and Chair of Computer Science at UCLA, University of California, Los Angeles. His research interests span the areas of compilers, embedded systems, programming languages, software engineering, and information security. He is the editor-in-chief of ACM Transactions of Programming Languages and Systems, a member of the editorial board of Information and Computation, a former member of the editorial board of IEEE Transactions on Software Engineering, and a former conference program chair of ACM Symposium on Principles of Programming Languages (POPL), Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), the Static Analysis Symposium (SAS), Conference on Embedded Systems Software (EMSOFT), Conference on Formal Methods and Programming Models for Co-Design (MEMOCODE), ACM Workshop on Program Analysis for Software Tools and Engineering (PASTE), and Symposium on Requirements Engineering for Information Security (SREIS).In 2012 he received the ACM SIGPLAN Distinguished Service Award.