Математическая модель параллельных программ и основанный на ней подход к верификации 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