Treffer: Localization of Linearizability Faults on the Coarse-Grained Level.

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. [ABSTRACT FROM AUTHOR]

Copyright of International Journal of Software Engineering & Knowledge Engineering is the property of World Scientific Publishing Company and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)