Parameterized Model Checking of Fine Grained Concurrency

Autor:	Daniel Schwartz-Narbonne, Muralidhar Talupur, Divjyot Sethi, Sharad Malik
Rok vydání:	2012
Předmět:	Model checking Programming language Computer science Concurrent data structure Concurrency Parameterized complexity Thread (computing) Parallel computing Separation logic computer.software_genre Data structure computer Cache coherence
Zdroj:	Model Checking Software ISBN: 9783642317583 SPIN
DOI:	10.1007/978-3-642-31759-0_15
Popis:	Concurrent data structures are provided in libraries such as Intel Thread Building Blocks and Java.util.concurrent to enable efficient implementation of multi-threaded programs. Their efficiency is achieved by using fine grained synchronization which creates less constrained interaction between the threads. This leads to a large number of possible interleavings and makes concurrent data structures hard to verify. In this paper, we describe our key insights from Murphi based parameterized model checking of these data structures. In particular, we describe the first model checking based framework to handle an unbounded number of threads for these data structures. This framework uses the CMP (CoMPositional) method which has been used in verifying cache coherence protocols. The CMP method requires the user to supply lemmas for abstraction refinement. A further contribution of our work is to show how a significant subset of these lemmas can be generated automatically.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::ffe5e13242dd22503b82758401a4e3a9 https://doi.org/10.1007/978-3-642-31759-0_15 Zobrazit plný text záznamu