TY - GEN
T1 - Parameterized model checking of fine grained concurrency
AU - Sethi, Divjyot
AU - Talupur, Muralidhar
AU - Schwartz-Narbonne, Daniel
AU - Malik, Sharad
PY - 2012
Y1 - 2012
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84864830016&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84864830016&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-31759-0_15
DO - 10.1007/978-3-642-31759-0_15
M3 - Conference contribution
AN - SCOPUS:84864830016
SN - 9783642317583
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 208
EP - 226
BT - Model Checking Software - 19th International Workshop, SPIN 2012, Proceedings
T2 - 19th International Workshop on Model Checking Software, SPIN 2012
Y2 - 23 July 2012 through 24 July 2012
ER -