Equivalence of two parallel execution systems

• Veröffentlicht in: PROBLEMS IN PROGRAMMING
• Datum: 2018
• Heft: 2-3
• Сторінки: 93-98
• ISSN: 1727-4907
• Автори та афіліації: T.V. Panchenko — Kiev Taras Shevchenko National University; S. Fabunmi — Kiev Taras Shevchenko National University
• Ключові слова: паралельна програма, синхронізація паралельних програм, доведення часткової коректності, коректність програмного забезпечення, програмна синхронізація, розподілені системи та паралельне програмування, ipcl, паралельні обчислення, паралельні алгоритми, паралелізація
• Hauptverfasser: Panchenko, T.V., Fabunmi, S.
• Format: Artikel
• Sprache: Ukrainisch
• Veröffentlicht: PROBLEMS IN PROGRAMMING 2018
• Schlagworte: software correctness; safety property proof; concurrent program; interleaving; IPCL; composition-nominative languages; formal verification; UDC 004.415; 681.3
• Online Zugang: https://pp.isofts.kiev.ua/index.php/ojs1/article/view/270
• Назва журналу: Problems in programming

The method for properties proof for parallel programs running multiple-instance interleaving with shared memory is investigated. Two systems for parallel execution of programs are considered and the justification of the mutual expressiveness of these two approaches are presented in this paper. The first one is with a fixed yet parametric number of programs executing in parallel. The second one implements a generation model (start) and joining after the stop (join) of parallel programs (also called multithreading). The corresponding two basic functions are provided, and their semantics are given. Also, the semantics of other functions related to parallel execution, resource management and access synchronization are presented in this paper. The theorem on the (functional) equivalence of these two systems and its justification are presented. The program in this case is considered as a function over the data. It is argued that for an arbitrary program in one of the systems of parallelism it is possible to construct the corresponding program in another system, which returns the same result (that is, functionally equivalent). Only productive programs are considered here in the context of mutual expressiveness, because otherwise they "hang" and do not return any result, thus they are out of our scope. The obtained result allows us to move reasoning from the more complex system (by structure) with a dynamic generation of parallel program instances to the simpler system (for proofs) with a parametric number of identical programs executed in parallel. Questions for further research in this direction are also identified.Problems in programming 2018; 2-3: 093-098