000125895 001__ 125895
000125895 005__ 20190316234317.0
000125895 02470 $$2ISI$$a000259487000002
000125895 037__ $$aCONF
000125895 245__ $$aCompleteness and Nondeterminism in Model Checking Transactional Memories
000125895 269__ $$a2008
000125895 260__ $$c2008
000125895 336__ $$aConference Papers
000125895 520__ $$aAbstract. Software transactional memory (STM) offers a disciplined concurrent programming model for exploiting the parallelism of modern processor architectures. This paper presents the first deterministic specification automata for strict serializability and opacity in STMs. Using an antichain-based tool, we show our deterministic specifications to be equivalent to more intuitive, nondeterministic specification automata (which are too large to be determinized automatically). Using deterministic specification automata, we obtain a complete verification tool for STMs. We also show how to model and verify contention management within STMs. We automatically check the opacity of popular STM algorithms, such as TL2 and DSTM, with a universal contention manager. The universal contention manager is nondeterministic and establishes correctness for all possible contention management schemes.
000125895 700__ $$0240335$$g105326$$aGuerraoui, Rachid
000125895 700__ $$aHenzinger, Thomas A.
000125895 700__ $$aSingh, Vasu
000125895 7112_ $$dAugust 19-22 2008$$aConcur 2008
000125895 773__ $$tProceedings of the 19th International Conference on Concurrency Theory
000125895 8564_ $$uhttps://infoscience.epfl.ch/record/125895/files/concur2008.pdf$$zn/a$$s225659
000125895 909C0 $$xU10407$$0252114$$pDCL
000125895 909CO $$ooai:infoscience.tind.io:125895$$qGLOBAL_SET$$pconf$$pIC
000125895 937__ $$aLPD-CONF-2008-028
000125895 973__ $$rREVIEWED$$sPUBLISHED$$aEPFL
000125895 980__ $$aCONF