DocumentCode :
555446
Title :
Scalable automatic linearizability checking
Author :
Zhang, Shao Jie
Author_Institution :
NUS Grad. Sch. for Integrative Sci. & Eng., Nat. Univ. of Singapore, Singapore, Singapore
fYear :
2011
fDate :
21-28 May 2011
Firstpage :
1185
Lastpage :
1187
Abstract :
Concurrent data structures are widely used but notoriously difficult to implement correctly. Linearizability is one main correctness criterion of concurrent data structure algorithms. It guarantees that a concurrent data structure appears as a sequential one to users. Unfortunately, linearizability is challenging to verify since a subtle bug may only manifest in a small portion of numerous thread interleavings. Model checking is therefore a potential primary candidate. However, current approaches of model checking linearizability suffer from severe state space explosion problem and are thus restricted in handling few threads and/or operations. This paper describes a scalable, fully automatic and general linearizability checking method based on [16] by incorporating symmetry and partial order reduction techniques. Our insights emerged from the observation that the similarity of threads using concurrent data structures causes model checking to generate large redundant equivalent portions of the state space, and the loose coupling of threads causes it to explore lots of unnecessary transition execution orders. We prove that symmetry reduction and partial order reduction can be combined in our approach and integrate them into the model checking algorithm. We demonstrate its efficiency using a number of real-world concurrent data structure algorithms.
Keywords :
data structures; formal verification; concurrent data structure algorithms; model checking; partial order reduction techniques; scalable automatic linearizability checking method; state space explosion problem; symmetry reduction; unnecessary transition execution orders; Computational modeling; Computer science; Computers; Conferences; Data structures; Instruction sets; Software algorithms; linearizability checking; model checking;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Software Engineering (ICSE), 2011 33rd International Conference on
Conference_Location :
Honolulu, HI
ISSN :
0270-5257
Print_ISBN :
978-1-4503-0445-0
Electronic_ISBN :
0270-5257
Type :
conf
DOI :
10.1145/1985793.1986037
Filename :
6032628
Link To Document :
بازگشت