000128696 001__ 128696
000128696 005__ 20190416220443.0
000128696 037__ $$aREP_WORK
000128696 245__ $$aThe Semantics of Progress in Lock-Based Transactional Memory
000128696 269__ $$a2008
000128696 260__ $$c2008
000128696 336__ $$aReports
000128696 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 lock-based 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 the verification of any set of transactions accessing an arbitrarily large set of shared variables can be reduced to the verification of 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.
000128696 6531_ $$aTransactional memory
000128696 6531_ $$alock
000128696 6531_ $$atry-lock
000128696 6531_ $$aconsensus number
000128696 6531_ $$aimpossibility
000128696 6531_ $$alower bound
000128696 6531_ $$areduction
000128696 6531_ $$asemantics
000128696 700__ $$0240335$$g105326$$aGuerraoui, Rachid
000128696 700__ $$aKapalka, Michal
000128696 8564_ $$uhttps://infoscience.epfl.ch/record/128696/files/lock-tm-progress-techreport08.pdf$$zn/a$$s198499
000128696 909C0 $$xU10407$$0252114$$pDCL
000128696 909CO $$ooai:infoscience.tind.io:128696$$qGLOBAL_SET$$pIC$$preport
000128696 937__ $$aLPD-REPORT-2008-015
000128696 973__ $$sPUBLISHED$$aEPFL
000128696 980__ $$aREPORT