Completeness and Nondeterminism in Model Checking Transactional Memories

Software transactional memory (STM) offers a disciplined concurrent programming model for exploiting the parallelism of modern processor architectures. This paper presents the first \emph{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 \emph{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 \emph{nondeterministic} and establishes correctness for all possible contention management schemes.

Published in:
Proceedings of the 19th International Conference on Concurrency Theory
Presented at:
19th International Conference on Concurrency Theory, Toronto, August 19–22, 2008

 Record created 2008-07-17, last modified 2018-11-26

Download fulltextPDF
External link:
Download fulltextURL
Rate this document:

Rate this document:
(Not yet reviewed)