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 条
[31]   Constructing and verifying a robust Mix Net using CSP [J].
Efstathios Stathakidis ;
David M. Williams ;
James Heather .
Software & Systems Modeling, 2016, 15 :1063-1089
[32]   Formalization and Verification of Kafka Messaging Mechanism Using CSP [J].
Xu, Junya ;
Yin, Jiaqi ;
Zhu, Huibiao ;
Xiao, Lili .
COMPUTER SCIENCE AND INFORMATION SYSTEMS, 2023, 20 (01) :277-306
[33]   Investigating a file transfer protocol using CSP and B [J].
Evans N. ;
Treharne H. .
Software & Systems Modeling, 2005, 4 (3) :258-276
[34]   Constructing and verifying a robust Mix Net using CSP [J].
Stathakidis, Efstathios ;
Williams, David M. ;
Heather, James .
SOFTWARE AND SYSTEMS MODELING, 2016, 15 (04) :1063-1089
[35]   USING CSP AND SYSTEM DYNAMICS AS PROCESS ENGINEERING TOOLS [J].
GREENWOOD, RM .
LECTURE NOTES IN COMPUTER SCIENCE, 1992, 635 :138-145
[36]   Formalization and Verification of Group Communication CoAP Using CSP [J].
Chen, Sini ;
Li, Ran ;
Zhu, Huibiao .
PARALLEL AND DISTRIBUTED COMPUTING, APPLICATIONS AND TECHNOLOGIES, PDCAT 2021, 2022, 13148 :616-628
[37]   Test-Driven Repair of Data Races in Structured Parallel Programs [J].
Surendran, Rishi ;
Raman, Raghavan ;
Chaudhuri, Swarat ;
Mellor-Crummey, John ;
Sarkar, Vivek .
ACM SIGPLAN NOTICES, 2014, 49 (06) :15-25
[38]   Detecting Data Races in OpenMP with Deep Learning and Large Language Models [J].
Alsofyani, May ;
Wang, Liqiang .
53RD INTERNATIONAL CONFERENCE ON PARALLEL PROCESSING, ICPP 2024, 2024, :96-103
[39]   Understanding and identifying latent data races cross-thread interleaving [J].
Zheng, Long ;
Liao, Xiaofei ;
Wu, Song ;
Fan, Xuepeng ;
Jin, Hai .
FRONTIERS OF COMPUTER SCIENCE, 2015, 9 (04) :524-539
[40]   Understanding and identifying latent data races cross-thread interleaving [J].
Long Zheng ;
Xiaofei Liao ;
Song Wu ;
Xuepeng Fan ;
Hai Jin .
Frontiers of Computer Science, 2015, 9 :524-539
12345