Geodesic
A mathematical model of parallel programs and an approach based on it to verification of MPI programs
Modelirovanie i analiz informacionnyh sistem, Tome 28 (2021) no. 4, pp. 394-412.

Voir la notice de l'article provenant de la source Math-Net.Ru

The paper presents a new mathematical model of parallel programs, on the basis of which it is possible, in particular, to verify parallel programs presented on a certain subset of the parallel programming interface MPI. This model is based on the concepts of a sequential and distributed process. A parallel program is modeled as a distributed process in which sequential processes communicate by asynchronously sending and receiving messages over channels. The main advantage of the described model is the ability to simulate and verify parallel programs that generate an indefinite number of sequential processes. The proposed model is illustrated by the application of verification of the matrix multiplication MPI program.
Keywords: parallel programs, MPI, distributed processes, verification. 
@article{MAIS_2021_28_4_a5,
     author = {A. M. Mironov},
     title = {A mathematical model of parallel programs and an approach based on it to verification of {MPI} programs},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {394--412},
     publisher = {mathdoc},
     volume = {28},
     number = {4},
     year = {2021},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2021_28_4_a5/}
}
TY  - JOUR
AU  - A. M. Mironov
TI  - A mathematical model of parallel programs and an approach based on it to verification of MPI programs
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2021
SP  - 394
EP  - 412
VL  - 28
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2021_28_4_a5/
LA  - ru
ID  - MAIS_2021_28_4_a5
ER  - 
%0 Journal Article
%A A. M. Mironov
%T A mathematical model of parallel programs and an approach based on it to verification of MPI programs
%J Modelirovanie i analiz informacionnyh sistem
%D 2021
%P 394-412
%V 28
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2021_28_4_a5/
%G ru
%F MAIS_2021_28_4_a5
A. M. Mironov. A mathematical model of parallel programs and an approach based on it to verification of MPI programs. Modelirovanie i analiz informacionnyh sistem, Tome 28 (2021) no. 4, pp. 394-412. http://geodesic.mathdoc.fr/item/MAIS_2021_28_4_a5/

[1] G. J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, 1990

[2] H. A. Lopez, E. R. Marques, F. Martins, N. Ng, C. Santos, V. T. Vasconcelos, N. Yoshida, “Protocol-based verification of message-passing parallel programs”, Proceedings of the 2015 ACM sigplan international conference on object-oriented programming, systems, languages, and applications, OOPSLA 2015, 2015, 280–298 | DOI

[3] I. Grudenic, N. Bogunovic, “Modeling and verification of MPI based distributed software”, Recent advances in parallel virtual machine and message passing interface, EuroPVM/MPI 2006, LNCS, 4192, Springer, 2006, 123–132

[4] A. Blass, Y. Gurevich, “Abstract state machines capture parallel algorithms”, ACM transactions on computational logic, 2003, 578–651 | DOI | Zbl

[5] S. F. Siegel, “Model checking nonblocking MPI programs”, International workshop on verification, model checking, and abstract interpretation, VMCAI, LNCS, 4349, Springer, 2007, 44–58 | Zbl

[6] S. F. Siegel, A. Mironova, G. S. Avrunin, L. A. Clarke, “Combining”, ACM Transactions on Software Engineering and Methodology, 17:2 (2008), 1–34 | DOI

[7] S. Vakkalanka, G. Gopalakrishnan, R. M. Kirby, “Dynamic verification of MPI programs with reductions in presence of split operations and relaxed orderings”, International Conference on Computer Aided Verification CAV 2008, LNCS, 5123, Springer, 2008, 66–79 | Zbl

[8] G. Gopalakrishnan, R. M. Kirby, S. Siegel, R. Thakur, W. Gropp, E. Lusk, B. R. De Supinski, M. Schulz, G. Bronevetsky, “Formal analysis of MPI-based parallel programs”, Communications, 54:12 (2011), 82–91

[9] V. Forejt, S. Joshi, D. Kroening, G. Narayanaswamy, S. Sharma, “Precise predictive analysis for discovering communication deadlocks in MPI programs”, ACM Transactions on Programming Languages and Systems, 39:4 (2017), 1–27 | DOI

[10] Z. Luo, M. Zheng, S. F. Siegel, “Verification of MPI programs using CIVL”, EuroMPI, 2017, 6:1–6:11

[11] W. Hong, Z. Chen, H. Yu, J. Wang, “Evaluation”, Science China information sciences, 62 (2019)

[12] H. Yu, Z. Chen, X. Fu, J. Wang, Z. Su, J. Sun, C. Huang, W. Dong, “Symbolic verification of message passing interface programs”, Proceedings of the ACM/IEEE 42nd international conference on software engineering, ICSE'20, 2020, 1248–1260