TY - GEN
T1 - Interleaving-Tree Based Fine-Grained Linearizability Fault Localization
AU - Chen, Yang
AU - Zhang, Zhenya
AU - Wu, Peng
AU - Zhang, Yu
N1 - Funding Information:
Acknowledgements. We thank the anonymous referees for their valuable comments. This work is partially supported by the National Key Basic Research Program of China under the Grant No. 2014CB340701, the National Key Research and Development Program of China under the Grant No. 2017YFB0801900, the CAS-INRIA Joint Research Program under the Grant No. GJHZ1844, and the ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST.
Funding Information:
We thank the anonymous referees for their valuable comments. This work is partially supported by the National Key Basic Research Program of China under the Grant No. 2014CB340701, the National Key Research and Development Program of China under the Grant No. 2017YFB0801900, the CAS-INRIA Joint Research Program under the Grant No. GJHZ1844, and the ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST.
Publisher Copyright:
© 2018, Springer Nature Switzerland AG.
PY - 2018
Y1 - 2018
N2 - Linearizability is an important correctness criterion for concurrent objects. Existing work mainly focuses on linearizability verification of coarse-grained traces with operation invocations and responses only. However, when linearizability is violated, such coarse-grained traces do not provide sufficient information for reasoning about the underlying concurrent program faults. In this paper, we propose a notion of critical data race sequence (CDRS), based on our fine-grained trace model, to characterize concurrent program faults that cause violation of linearizability. We then develop a labeled tree model of interleaved program executions and show how to identify CDRSes and localize concurrent program faults automatically with a specific node-labeling mechanism. We also implemented a prototype tool, FGVT, for real-world Java concurrent programs. Experiments show that our localization technique is effective, i.e., all the CDRSes reported by FGVT indeed reveal the root causes of linearizability faults.
AB - Linearizability is an important correctness criterion for concurrent objects. Existing work mainly focuses on linearizability verification of coarse-grained traces with operation invocations and responses only. However, when linearizability is violated, such coarse-grained traces do not provide sufficient information for reasoning about the underlying concurrent program faults. In this paper, we propose a notion of critical data race sequence (CDRS), based on our fine-grained trace model, to characterize concurrent program faults that cause violation of linearizability. We then develop a labeled tree model of interleaved program executions and show how to identify CDRSes and localize concurrent program faults automatically with a specific node-labeling mechanism. We also implemented a prototype tool, FGVT, for real-world Java concurrent programs. Experiments show that our localization technique is effective, i.e., all the CDRSes reported by FGVT indeed reveal the root causes of linearizability faults.
UR - http://www.scopus.com/inward/record.url?scp=85053064515&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85053064515&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-99933-3_7
DO - 10.1007/978-3-319-99933-3_7
M3 - Conference contribution
AN - SCOPUS:85053064515
SN - 9783319999326
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 108
EP - 126
BT - Dependable Software Engineering. Theories, Tools, and Applications - 4th International Symposium, SETTA 2018, Proceedings
A2 - Yang, Zijiang
A2 - Feng, Xinyu
A2 - Müller-Olm, Markus
PB - Springer Verlag
T2 - 4th International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, SETTA 2018
Y2 - 4 September 2018 through 6 September 2018
ER -