Symbolic Execution of MPI Programs

被引:6
|
作者
Fu, Xianjin [1 ,2 ]
Chen, Zhenbang [2 ]
Yu, Hengbiao [1 ,2 ]
Huang, Chun [2 ]
Dong, Wei [2 ]
Wang, Ji [1 ,2 ]
机构
[1] Natl Univ Def Technol, State Key Lab High Performance Comp, Changsha, Hunan, Peoples R China
[2] Natl Univ Def Technol, Coll Comp, Changsha, Hunan, Peoples R China
关键词
D O I
10.1109/ICSE.2015.259
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
MPI is widely used in high performance computing. In this extended abstract, we report our current status of analyzing MPI programs. Our method can provide coverage of both input and non-determinism for MPI programs with mixed blocking and non-blocking operations. In addition, to improve the scalability further, a deadlock-oriented guiding method for symbolic execution is proposed. We have implemented our methods, and the preliminary experimental results are promising.
引用
收藏
页码:809 / 810
页数:2
相关论文
共 50 条
  • [1] MPISE: Symbolic Execution of MPI Programs
    Fu, Xianjin
    Chen, Zhenbang
    Zhang, Yufeng
    Huang, Chun
    Dong, Wei
    Wang, Ji
    [J]. 2015 IEEE 16TH INTERNATIONAL SYMPOSIUM ON HIGH ASSURANCE SYSTEMS ENGINEERING (HASE), 2015, : 181 - 188
  • [2] Static Analysis and Symbolic Execution for Deadlock Detection in MPI Programs
    Douglas, Craig C.
    Krishnamoorthy, Krishanthan
    [J]. COMPUTATIONAL SCIENCE - ICCS 2018, PT II, 2018, 10861 : 783 - 796
  • [3] Combining Symbolic Execution and Model Checking to Verify MPI Programs
    Yu, Hengbiao
    [J]. PROCEEDINGS 2018 IEEE/ACM 40TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING - COMPANION (ICSE-COMPANION, 2018, : 527 - 529
  • [4] Symbolic Execution of MPI Programs with One-Sided Communications
    Hu, Nenghui
    Bian, Zheng
    Shuai, Ziqi
    Chen, Zhenbang
    Zhang, Yufeng
    [J]. PROCEEDINGS OF THE 2023 30TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE, APSEC 2023, 2023, : 657 - 658
  • [5] MPI-SV: A Symbolic Verifier for MPI Programs
    Chen, Zhenbang
    Yu, Hengbiao
    Fu, Xianjin
    Wang, Ji
    [J]. 2020 ACM/IEEE 42ND INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING: COMPANION PROCEEDINGS (ICSE-COMPANION 2020), 2020, : 93 - 96
  • [6] Symbolic Execution for Randomized Programs
    Susag, Zachary
    Lahiri, Sumit
    Hsu, Justin
    Roy, Subhajit
    [J]. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2022, 6 (OOPSLA):
  • [7] Symbolic execution of programs with strings
    Redelinghuys, Gideon
    Visser, Willem
    Geldenhuys, Jaco
    [J]. PROCEEDINGS OF THE SOUTH AFRICAN INSTITUTE FOR COMPUTER SCIENTISTS AND INFORMATION TECHNOLOGISTS CONFERENCE, 2012, : 139 - 148
  • [8] On Symbolic Execution of Decompiled Programs
    Korencik, Lukas
    Rockai, Petr
    Lauko, Henrich
    Barnat, Jiri
    [J]. 2020 IEEE 20TH INTERNATIONAL CONFERENCE ON SOFTWARE QUALITY, RELIABILITY, AND SECURITY (QRS 2020), 2020, : 265 - 272
  • [9] Dynamic Symbolic Verification of MPI Programs
    Khanna, Dhriti
    Sharma, Subodh
    Rodriguez, Cesar
    Purandare, Rahul
    [J]. FORMAL METHODS, 2018, 10951 : 466 - 484
  • [10] TESTING MIXAL PROGRAMS BY SYMBOLIC EXECUTION
    ERMAKOV, GV
    [J]. PROGRAMMING AND COMPUTER SOFTWARE, 1988, 14 (01) : 1 - 6