Interleaving-Tree Based Fine-Grained Linearizability Fault Localization

Yang Chen, Zhenya Zhang, Peng Wu, Yu Zhang

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish
Title of host publicationDependable Software Engineering. Theories, Tools, and Applications - 4th International Symposium, SETTA 2018, Proceedings
EditorsZijiang Yang, Xinyu Feng, Markus Müller-Olm
PublisherSpringer Verlag
Pages108-126
Number of pages19
ISBN (Print)9783319999326
DOIs
Publication statusPublished - 2018
Externally publishedYes
Event4th International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, SETTA 2018 - Beijing, China
Duration: Sep 4 2018Sep 6 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10998 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference4th International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, SETTA 2018
Country/TerritoryChina
CityBeijing
Period9/4/189/6/18

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Interleaving-Tree Based Fine-Grained Linearizability Fault Localization'. Together they form a unique fingerprint.

Cite this