Математическая модель параллельных программ и основанный на ней подход к верификации MPI-программ
https://doi.org/10.18255/1818-1015-2021-4-394-412
Аннотация
В работе излагается новая математическая модель параллельных программ, на базе которой можно в частности верифицировать параллельные программы, представленные на некотором подмножестве программного интерфейса параллельного программирования MPI. Данная модель основана на понятиях последовательного и распределенного процесса. Параллельная программа моделируется распределенным процессом, в котором последовательные процессы взаимодействуют путем асинхронной передачи и приема сообщений через каналы. Главным преимуществом изложенной модели является возможность моделирования и верификации параллельных программ, порождающих неопределенное число последовательных процессов. Изложенная модель проиллюстрирована применением к верификации MPI программы перемножения матриц.
Об авторе
Андрей Михайлович Миронов
Московский государственный университет им. М. В. Ломоносова
Россия
Россия
Список литературы
1. G. J. Holzmann, Design and Validation of Computer Protocols. Prentice Hall, 1990.
2. 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.
3. 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.
4. A. Blass and Y. Gurevich, “Abstract State Machines Capture Parallel Algorithms,” in ACM Transactions on Computational Logic, 2003, pp. 578-651.
5. 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.
6. 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.
7. 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.
8. G. Gopalakrishnan et al., “Formal analysis of MPI-based parallel programs,” Communications ACM, vol. 54, no. 12, pp. 82-91, 2011.
9. 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.
10. Z. Luo, M. Zheng, and S. F. Siegel, “Verification of MPI programs using CIVL,” in EuroMPI, 2017, pp. 6:1-6:11.
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.
12. 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.
Рецензия
Для цитирования:
Миронов А.М. Математическая модель параллельных программ и основанный на ней подход к верификации MPI-программ. Моделирование и анализ информационных систем. 2021;28(4):394-412. https://doi.org/10.18255/1818-1015-2021-4-394-412
For citation:
Mironov A.M. A Mathematical Model of Parallel Programs and an Approach Based on it to Verification of MPI Programs. Modeling and Analysis of Information Systems. 2021;28(4):394-412. (In Russ.) https://doi.org/10.18255/1818-1015-2021-4-394-412
Просмотров:
510
Послать статью по эл. почте 