Parameterized model checking of fine grained concurrency

Divjyot Sethi, Muralidhar Talupur, Daniel Schwartz-Narbonne, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationModel Checking Software - 19th International Workshop, SPIN 2012, Proceedings
Pages208-226
Number of pages19
DOIs
StatePublished - Aug 15 2012
Event19th International Workshop on Model Checking Software, SPIN 2012 - Oxford, United Kingdom
Duration: Jul 23 2012Jul 24 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7385 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other19th International Workshop on Model Checking Software, SPIN 2012
CountryUnited Kingdom
CityOxford
Period7/23/127/24/12

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Parameterized model checking of fine grained concurrency'. Together they form a unique fingerprint.

Cite this