Model checking unbounded concurrent lists

Divjyot Sethi, Muralidhar Talupur, Sharad Malik

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

2 Scopus citations

Abstract

We present a model checking based method for verifying list-based concurrent data structures. Concurrent data structures are notorious for being hard to get right and thus, their verification has received significant attention from the verification community. These data structures are unbounded in two dimensions: the list size is unbounded and an unbounded number of threads access them. Thus, their model checking requires abstraction to a model bounded in both the dimensions. In previous work, we showed how the unbounded number of threads can be model checked by reduction to a finite model. In that work, we used the CMP (CoMPositional) method which abstracts the unbounded threads by keeping one thread as is (concrete) and abstracting all the other threads to a single environment thread. Next, this abstraction was iteratively refined by the user in order to prove correctness. However, in that work we assumed that the number of list elements was bounded by a fixed value. In practice this fixed value was small; model checking could only complete for small sized lists. In this work, we overcome this limitation and model check the unbounded list as well. While it is possible to show correctness for unbounded threads by keeping one concrete thread and abstracting others, this is not directly possible in the list dimension as the nodes pointed to by the threads change during list traversal. Our method addresses this challenge by constructing an abstraction for which the concrete nodes can change with program execution and allowing for refinement of this abstraction to prove invariants. We show the soundness of our method and establish its utility by model checking challenging concurrent listbased data structure examples.

Original languageEnglish (US)
Title of host publicationModel Checking Software - 20th International Symposium, SPIN 2013, Proceedings
Pages320-340
Number of pages21
DOIs
StatePublished - Oct 8 2013
Event20th International Symposium on Model Checking Software, SPIN 2013 - Stony Brook, NY, United States
Duration: Jul 8 2013Jul 9 2013

Publication series

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

Other

Other20th International Symposium on Model Checking Software, SPIN 2013
CountryUnited States
CityStony Brook, NY
Period7/8/137/9/13

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Model checking unbounded concurrent lists'. Together they form a unique fingerprint.

  • Cite this

    Sethi, D., Talupur, M., & Malik, S. (2013). Model checking unbounded concurrent lists. In Model Checking Software - 20th International Symposium, SPIN 2013, Proceedings (pp. 320-340). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7976 LNCS). https://doi.org/10.1007/978-3-642-39176-7-20