DOI: https://doi.org/10.15407/pp2018.02.093

Equivalence of two parallel execution systems

T. V. Panchenko, S. Fabunmi

Abstract


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


Keywords


software correctness; safety property proof; concurrent program; interleaving; IPCL; composition-nominative languages; formal verification

Full Text:

PDF (Ukrainian)

References


PANCHENKO, T. (2008) The Method for Program Properties Proof in Compositional Nominative Languages IPCL [in Ukrainian]. Problems of Programming. 1. P. 3–16.

PANCHENKO, T. (2004) The Methodology for Program Properties Proof in Compositional Languages IPCL [in Ukrainian]. In Proceedings of the International Conference "Theoretical and Applied Aspects of Program Systems Development" (TAAPSD'2004). Kyiv. P. 62–67.

PANCHENKO, T. (2006) Compositional Methods for Software Systems Specification and Verification (PhD Thesis Synopsis) [in Ukrainian]. Kyiv. 17 p.

IVANOV, IE., PANCHENKO, T. and FABUNMI, S. (2017) Parallelism Model with Instances Generation in IPCL [in Ukrainian]. In Proceedings of the International Conference "Theoretical and Applied Aspects of Program Systems Development" (TAAPSD'2017). Kyiv. P. 131–133.

POLISHCHUK, N.V., KARTAVOV, M.O. and PANCHENKO, T.V. (2015) Safety Property Proof using Correctness Proof Methodology in IPCL. In Proceedings of the 5th International Scientific Conference “Theoretical and Applied Aspects of Cybernetics”, Kyiv, Bukrek, P. 37–44.

KARTAVOV, M., PANCHENKO, T. and POLISHCHUK, N. (2015) Properties Proof Method in IPCL Application To Real-World System Correctness Proof. International Journal "Information Models and Analyses", Sofia, Bulgaria, ITHEA, Vol. 4, N 2, P. 142–155.

PANCHENKO, T. (2016) Application of the Method for Concurrent Programs Properties Proof to Real-World Industrial Software Systems. In Proceedings of the 12th International Conference on ICT in Education, Research and Industrial Applications. Integration, Harmonization and Knowledge Transfer (ICTERI 2016), edited by Vadim Ermolayev et al., Kyiv, P.119–128 (CEUR-WS. – Vol. 1614, available online: http://ceur-ws.org/Vol-1614/).




DOI: https://doi.org/10.15407/pp2018.02.093

Refbacks

  • There are currently no refbacks.