Predicting and Witnessing Data Races Using CSP

被引：0

作者：

Carril, Luis M. ^{[1
]}

Tichy, Walter F. ^{[1
]}

机构：

[1] Karlsruhe Inst Technol, Inst Program Struct & Data Org IPD, D-76131 Karlsruhe, Germany

来源：

NASA FORMAL METHODS (NFM 2015) | 2015年 / 9058卷

关键词：

Data race; Concurrent programs; Debug; CSP;

D O I：

10.1007/978-3-319-17524-9_28

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Detecting and debugging data races is a complex task due to the large number of interleavings possible in a parallel program. Most tools can find the data races reliably in an observed execution, but they miss errors in alternative reorderings of events. In this paper we describe an automated approach to generate, from a single program trace, a model in CSP with alternative interleavings. We check for data races patterns and obtain a witness that allows the reproduction of errors. Reproduction reduces the developer effort to correct the error.

引用

页码：400 / 407

页数：8

共 50 条

[41] DR.FIX: Automatically Fixing Data Races at Industry Scale [J].

Behrang, Farnaz ;

Zhang, Zhizhou ;

Saioc, Georgian-Vlad ;

Liu, Peng ;

Chabbi, Milind .

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2025, 9 (PLDI)

[42] Detecting Data Races Caused by Inconsistent Lock Protection in Device Drivers [J].

Chen, Qiu-Liang ;

Bai, Jia-Ju ;

Jiang, Zu-Ming ;

Lawall, Julia ;

Hu, Shi-Min .

2019 IEEE 26TH INTERNATIONAL CONFERENCE ON SOFTWARE ANALYSIS, EVOLUTION AND REENGINEERING (SANER), 2019, :366-376

[43] Modeling and Verifying Identity Authentication Security of HDFS using CSP [J].

Xu, Chao ;

Zhu, Huibiao ;

Xie, Wanling .

2017 24TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2017), 2017, :259-268

[44] Formalization and Verification of the PKMv3 Protocol Using CSP [J].

Xu, Yuanmin ;

Zhu, Huibiao ;

Zhu, Xiaoran ;

Wu, Xi ;

Guo, Jian ;

Lu, Gang .

2017 IEEE 41ST ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), VOL 1, 2017, :499-504

[45] Supporting rescheduling using CSP, RMS and POB - an example application [J].

Kelleher, G ;

Cavichiollo, P .

JOURNAL OF INTELLIGENT MANUFACTURING, 2001, 12 (04) :343-357

[46] Analysing time dependent security properties in CSP using PVS [J].

Evans, N ;

Schneider, S .

COMPUTER SECURITY - ESORICS 2000, PROCEEDINGS, 2000, 1895 :222-237

[47] Supporting rescheduling using CSP, RMS and POB—an example application [J].

G. Kelleher ;

P. Cavichiollo .

Journal of Intelligent Manufacturing, 2001, 12 :343-357

[48] Simulation of a CSP Solar Steam Generator, Using Machine Learning [J].

Gonzalez Gonzalez, Adrian ;

Alvarez Cabal, Jose Valeriano ;

Vigil Berrocal, Miguel Angel ;

Peon Menendez, Rogelio ;

Riesgo Fernandez, Adrian .

ENERGIES, 2021, 14 (12)

[49] Refinement and Verification of Sequence Diagrams Using the Process Algebra CSP [J].

Kaizu, Tomohiro ;

Isobe, Yoshinao ;

Suzuki, Masato .

IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, 2013, E96A (02) :495-504

[50] Automatic web services composition using combining HTN and CSP [J].

Paik, Incheon ;

Maruyama, Daisuke .

2007 CIT: 7TH IEEE INTERNATIONAL CONFERENCE ON COMPUTER AND INFORMATION TECHNOLOGY, PROCEEDINGS, 2007, :206-211

← 1 2 3 4 5 →