Completeness and nondeterminism in model checking transactional memories Conference Paper


Author(s): Guerraoui, Rachid; Henzinger, Thomas A; Singh, Vasu
Title: Completeness and nondeterminism in model checking transactional memories
Title Series: LNCS
Affiliation
Abstract: 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.
Keywords: model checking; correctness; STM
Conference Title: CONCUR: Concurrency Theory
Volume: 5201
Conference Dates: August 19-22, 2008
Conference Location: Toronto, Canada
ISBN: 978-3-95977-017-0
Publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik  
Location: Berlin, Heidelberg
Date Published: 2008-07-30
Start Page: 21
End Page: 35
Sponsor: This research was supported by the Swiss National Science Foundation.
URL:
DOI: 10.1007/978-3-540-85361-9_6
Open access: no
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
  2. Vasu Singh
    17 Singh
Related IST Austria Work