TY - GEN
T1 - Model checking unbounded concurrent lists
AU - Sethi, Divjyot
AU - Talupur, Muralidhar
AU - Malik, Sharad
N1 - Copyright:
Copyright 2021 Elsevier B.V., All rights reserved.
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84884938264&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84884938264&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-39176-7_20
DO - 10.1007/978-3-642-39176-7_20
M3 - Conference contribution
AN - SCOPUS:84884938264
SN - 9783642391750
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 320
EP - 340
BT - Model Checking Software - 20th International Symposium, SPIN 2013, Proceedings
PB - Springer Verlag
T2 - 20th International Symposium on Model Checking Software, SPIN 2013
Y2 - 8 July 2013 through 9 July 2013
ER -