Interleaving-Tree Based Fine-Grained Linearizability Fault Localization

Yang Chen, Zhenya Zhang, Peng Wu, Yu Zhang

研究成果: 書籍/レポート タイプへの寄稿会議への寄与

抄録

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.

本文言語英語
ホスト出版物のタイトルDependable Software Engineering. Theories, Tools, and Applications - 4th International Symposium, SETTA 2018, Proceedings
編集者Zijiang Yang, Xinyu Feng, Markus Müller-Olm
出版社Springer Verlag
ページ108-126
ページ数19
ISBN(印刷版)9783319999326
DOI
出版ステータス出版済み - 2018
外部発表はい
イベント4th International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, SETTA 2018 - Beijing, 中国
継続期間: 9月 4 20189月 6 2018

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
10998 LNCS
ISSN(印刷版)0302-9743
ISSN(電子版)1611-3349

会議

会議4th International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, SETTA 2018
国/地域中国
CityBeijing
Period9/4/189/6/18

!!!All Science Journal Classification (ASJC) codes

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)

フィンガープリント

「Interleaving-Tree Based Fine-Grained Linearizability Fault Localization」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル