The semantics of progress in lock-based transactional memory

Transactional memory (TM) is a promising paradigm for concurrent programming. Whereas the number of TM implementations is growing, however, little research has been conducted to precisely define TM semantics, especially their progress guarantees. This paper is the first to formally define the progress semantics of lockbased TMs, which are considered the most effective in practice. We use our semantics to reduce the problems of reasoning about the correctness and computability power of lock-based TMs to those of simple try-lock objects. More specifically, we prove that checking the progress of any set of transactions accessing an arbitrarily large set of shared variables can be reduced to verifying a simple property of each individual (logical) try-lock used by those transactions. We use this theorem to determine the correctness of state-of-the-art lock-based TMs and highlight various configuration ambiguities. We also prove that lock-based TMs have consensus number 2. This means that,...

• Type: Conference
• Year: 2009
• Where: POPL
• Authors: Rachid Guerraoui, Michal Kapalka
• Keywords: Lock-based Tm Implementations, POPL 2009, Programming Languages, TM Implementations, TM Semantics