Theory of computing

A mathematical model of parallel programs and an approach based on it to verification of MPI programs

A. M. Mironov

Lomonosov Moscow State University, 1 Leninskie Gory, Moscow 119991, Russia

Abstract: 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.

UDC: 519.681.2

MSC: 68Q60

Received: 15.11.2021
Revised: 01.12.2021
Accepted: 08.12.2021

DOI: 10.18255/1818-1015-2021-4-394-412