000130152 001__ 130152
000130152 005__ 20190416055729.0
000130152 02470 $$2ISI$$a000272013800036
000130152 037__ $$aCONF
000130152 245__ $$aThe Semantics of Progress in Lock-Based Transactional Memory
000130152 269__ $$a2009
000130152 260__ $$bACM$$c2009
000130152 336__ $$aConference Papers
000130152 520__ $$aTransactional 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, on the one hand, a lock-based TM cannot be implemented using only read-write memory, but, on the other hand, it does not need very powerful instructions such as the commonly used compare-and-swap. We finally use our semantics to formally capture an inherent trade-off in the performance of lock-based TM implementations. Namely, we show that the space complexity of every lock-based software TM implementation that uses invisible reads is at least exponential in the number of objects accessible to transactions.
000130152 6531_ $$aTransactional memory
000130152 6531_ $$alock
000130152 6531_ $$atry-lock
000130152 6531_ $$aconsensus number
000130152 6531_ $$aimpossibility
000130152 6531_ $$alower bound
000130152 6531_ $$areduction
000130152 6531_ $$asemantics
000130152 700__ $$0240335$$aGuerraoui, Rachid$$g105326
000130152 700__ $$aKapalka, Michal
000130152 7112_ $$a36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)$$cSavannah, Georgia, USA$$dJanuary 21-23, 2009
000130152 773__ $$tProceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)
000130152 8564_ $$s218362$$uhttps://infoscience.epfl.ch/record/130152/files/popl096-kapalka.pdf$$zn/a
000130152 909C0 $$0252114$$pDCL$$xU10407
000130152 909CO $$ooai:infoscience.tind.io:130152$$pconf$$pIC$$qGLOBAL_SET
000130152 937__ $$aLPD-CONF-2008-039
000130152 973__ $$aEPFL$$rREVIEWED$$sPUBLISHED
000130152 980__ $$aCONF