Localization of Linearizability Faults on the Coarse-Grained Level

Zhenya Zhang, Peng Wu, Yu Zhang

Research output: Contribution to journalArticlepeer-review

2 Citations (Scopus)


Linearizability is an important correctness criterion that guarantees the safety of concurrent data structures. Due to the nondeterminism of concurrent executions, reproduction and localization of a linearizability fault still remain challenging. The existing works mainly focus on model checking the thread schedule space of a concurrent program on a fine-grained (state) level, and hence suffer from the severe problem of state space explosion. This paper presents a tool called CGVT to build a small test case that is sufficient enough for reproducing a linearizability fault. Given a possibly long history that has been detected nonlinearizable, CGVT first locates the operations causing a linearizability violation and then synthesizes a minimum test case for further investigation. Moreover, we present several optimization techniques to improve the effectiveness and efficiency of CGVT. We have applied CGVT to 10 concurrent objects, while the linearizability of some of the objects is unknown yet. The experiments show that CGVT is powerful and efficient enough to build the test cases more adaptable for fine-grained fault localization.

Original languageEnglish
Pages (from-to)1483-1505
Number of pages23
JournalInternational Journal of Software Engineering and Knowledge Engineering
Issue number9-10
Publication statusPublished - Dec 1 2017
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Networks and Communications
  • Computer Graphics and Computer-Aided Design
  • Artificial Intelligence


Dive into the research topics of 'Localization of Linearizability Faults on the Coarse-Grained Level'. Together they form a unique fingerprint.

Cite this