maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2021-4-394-412mais-1567Research ArticleTheory of ComputingМатематическая модель параллельных программ и основанный на ней подход к верификации MPI-программA Mathematical Model of Parallel Programs and an Approach Based on it to Verification of MPI Programshttps://orcid.org/0000-0002-9132-7804МироновАндрей МихайловичMironovAndrew M.amironov66@gmail.comМосковский государственный университет им. М. В. ЛомоносоваРоссияLomonosov Moscow State UniversityRussian Federation202118122021284394412Copyright © Миронов А.М., 20212021Миронов А.М.Mironov A.M.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1567

В работе излагается новая математическая модель параллельных программ, на базе которой можно в частности верифицировать параллельные программы, представленные на некотором подмножестве программного интерфейса параллельного программирования MPI. Данная модель основана на понятиях последовательного и распределенного процесса. Параллельная программа моделируется распределенным процессом, в котором последовательные процессы взаимодействуют путем асинхронной передачи и приема сообщений через каналы. Главным преимуществом изложенной модели является возможность моделирования и верификации параллельных программ, порождающих неопределенное число последовательных процессов. Изложенная модель проиллюстрирована применением к верификации MPI программы перемножения матриц.

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.

параллельные программыMPIраспределенные процессыверификацияparallel programsMPIdistributed processesverificationReferencesG. J. Holzmann, Design and Validation of Computer Protocols. Prentice Hall, 1990.G. J. Holzmann, Design and Validation of Computer Protocols. Prentice Hall, 1990.H. A. Lopez et al., “Protocol-based verification of message-passing parallel programs,” in Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications - OOPSLA 2015, 2015, pp. 280-298.H. A. Lopez et al., “Protocol-based verification of message-passing parallel programs,” in Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications - OOPSLA 2015, 2015, pp. 280-298.I. Grudenic and N. Bogunovic, “Modeling and Verification of MPI Based Distributed Software,” in Recent Advances in Parallel Virtual Machine and Message Passing Interface. EuroPVM/MPI 2006, vol. 4192, Springer, 2006, pp. 123-132.I. Grudenic and N. Bogunovic, “Modeling and Verification of MPI Based Distributed Software,” in Recent Advances in Parallel Virtual Machine and Message Passing Interface. EuroPVM/MPI 2006, vol. 4192, Springer, 2006, pp. 123-132.A. Blass and Y. Gurevich, “Abstract State Machines Capture Parallel Algorithms,” in ACM Transactions on Computational Logic, 2003, pp. 578-651.A. Blass and Y. Gurevich, “Abstract State Machines Capture Parallel Algorithms,” in ACM Transactions on Computational Logic, 2003, pp. 578-651.S. F. Siegel, “Model Checking Nonblocking MPI Programs,” in International Workshop on Verification, Model Checking, and Abstract Interpretation, VMCAI, vol. 4349, Springer, 2007, pp. 44-58.S. F. Siegel, “Model Checking Nonblocking MPI Programs,” in International Workshop on Verification, Model Checking, and Abstract Interpretation, VMCAI, vol. 4349, Springer, 2007, pp. 44-58.S. F. Siegel, A. Mironova, G. S. Avrunin, and L. A. Clarke, “Combining symbolic execution with model checking to verify parallel numerical programs,” ACM Transactions on Software Engineering and Methodology, vol. 17, no. 2, pp. 1-34, 2008.S. F. Siegel, A. Mironova, G. S. Avrunin, and L. A. Clarke, “Combining symbolic execution with model checking to verify parallel numerical programs,” ACM Transactions on Software Engineering and Methodology, vol. 17, no. 2, pp. 1-34, 2008.S. Vakkalanka, G. Gopalakrishnan, and R. M. Kirby, “Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings,” in International Conference on Computer Aided Verification CAV 2008, vol. 5123, Springer, 2008, pp. 66-79.S. Vakkalanka, G. Gopalakrishnan, and R. M. Kirby, “Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings,” in International Conference on Computer Aided Verification CAV 2008, vol. 5123, Springer, 2008, pp. 66-79.G. Gopalakrishnan et al., “Formal analysis of MPI-based parallel programs,” Communications ACM, vol. 54, no. 12, pp. 82-91, 2011.G. Gopalakrishnan et al., “Formal analysis of MPI-based parallel programs,” Communications ACM, vol. 54, no. 12, pp. 82-91, 2011.V. Forejt, S. Joshi, D. Kroening, G. Narayanaswamy, and S. Sharma, “Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs,” ACM Transactions on Programming Languages and Systems, vol. 39, no. 4, pp. 1-27, 2017.V. Forejt, S. Joshi, D. Kroening, G. Narayanaswamy, and S. Sharma, “Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs,” ACM Transactions on Programming Languages and Systems, vol. 39, no. 4, pp. 1-27, 2017.Z. Luo, M. Zheng, and S. F. Siegel, “Verification of MPI programs using CIVL,” in EuroMPI, 2017, pp. 6:1-6:11.Z. Luo, M. Zheng, and S. F. Siegel, “Verification of MPI programs using CIVL,” in EuroMPI, 2017, pp. 6:1-6:11.W. Hong, Z. Chen, H. Yu, and J. Wang, “Evaluation of model checkers by verifying message passing programs,” in Science China Information Sciences, vol. 62, 2019.W. Hong, Z. Chen, H. Yu, and J. Wang, “Evaluation of model checkers by verifying message passing programs,” in Science China Information Sciences, vol. 62, 2019.H. Yu et al., “Symbolic Verification of Message Passing Interface Programs,” in Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering, ICSE '20, 2020, pp. 1248-1260.H. Yu et al., “Symbolic Verification of Message Passing Interface Programs,” in Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering, ICSE '20, 2020, pp. 1248-1260.

The authors declare that there are no conflicts of interest present.