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 条

[21] Formalization and Verification of OpenStack Swift Using CSP [J].

Su, Ziqing ;

Lin, Wei ;

Zhu, Huibiao .

2024 IEEE 48TH ANNUAL COMPUTERS, SOFTWARE, AND APPLICATIONS CONFERENCE, COMPSAC 2024, 2024, :51-60

[22] Using CSP to detect errors in the TMN protocol [J].

Lowe, G ;

Roscoe, B .

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1997, 23 (10) :659-669

[23] Verifying anonymity in voting systems using CSP [J].

Moran, Murat ;

Heather, James ;

Schneider, Steve .

FORMAL ASPECTS OF COMPUTING, 2014, 26 (01) :63-98

[24] Modeling and Verifying the Ariadne Protocol Using CSP [J].

Wu, Xi ;

Liu, Si ;

Zhu, Huibiao ;

Zhao, Yongxin ;

Chen, Lei .

2012 IEEE 19TH INTERNATIONAL CONFERENCE AND WORKSHOPS ON ENGINEERING OF COMPUTER BASED SYSTEMS (ECBS), 2012, :24-32

[25] Formalization and Verification of REST on HTTP Using CSP [J].

Yuan, Ting ;

Tang, Yiting ;

Wu, Xi ;

Zhang, Yue ;

Zhu, Huibiao ;

Guo, Jian ;

Qin, Weijun .

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2014, 309 :75-93

[26] Routing of Vehicles Using CSP Case Study [J].

Ratke, Claudio ;

Hoffmann, Helcio ;

Nehring, Hannelore .

2015 9TH INTERNATIONAL CONFERENCE ON COMPLEX, INTELLIGENT, AND SOFTWARE INTENSIVE SYSTEMS CISIS 2015, 2015, :250-253

[27] Specifying authentication using signal events in CSP [J].

Shaikh, Sirai A. ;

Bush, Vicky J. ;

Schneider, Steve A. .

COMPUTERS & SECURITY, 2009, 28 (05) :310-324

[28] Assertional Reasoning about Data Races in Relaxed Memory Models [J].

Sanders, Beverly A. ;

Kim, KyungHee .

PPOPP'08: PROCEEDINGS OF THE 2008 ACM SIGPLAN SYMPOSIUM ON PRINCIPLES AND PRACTICE OF PARALLEL PROGRAMMING, 2008, :267-268

[29] Toward Verifying Cooperatively Scheduled Runtimes Using CSP [J].

Pedersen, Jan Baekgaard ;

Chalmers, Kevin .

FORMAL ASPECTS OF COMPUTING, 2023, 35 (04)

[30] Formalization and Verification of the OpenFlow Bundle Mechanism Using CSP [J].

Wang, Huiwen ;

Zhu, Huibiao ;

Xiao, Lili ;

Fei, Yuan .

INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING, 2018, 28 (11-12) :1657-1677

← 1 2 3 4 5 →