Control Systems and Computers, N4, 2018, Article 4
DOI: https://doi.org/10.15407/usim.2018.04.046
Upr. sist. maš., 2018, Issue 4 (276), pp. 46-56.
UDC 004.4
Sergiy D. Pogorilyy, Doctor of Technical Sciences, Professor, Head of Computer Engineering Department, E-mail: sdp@univ.net.ua,
ORCID ID – http://orcid.org/0000-0002-6497-5056,
Sergii L. Kryvyi, Doctor of Physical and Mathematical Sciences, Professor, E-mail: sl.krivoi@gmail.com,
ORCID ID – http://orcid.org/0000-0003-4231-0691,
Maksym S. Slynko, PhD student, E-mail: maxim.slinko@gmail.com,
ORCID ID – http://orcid.org/0000-0001-9667-8729,
Taras Shevchenko National University of Kyiv, Glushkov ave., 4g, 03022, Kyiv, Ukraine
Model justification of GPU-based applications
Introduction. Nowadays high performance computing (HPC) trends are shifted from using cluster systems consisting of general-purpose modules to more specialized accelerator components (GPUs, FPGAs etc.). Development of high-level complexity systems with massive parallelism based on GPU accelerators requires evolution of the scientifically based methods of application design and verification.
Goal. The purpose of this article is to present the new method of GPU-based application development based on the model design.
Methods. The method of application design and verification, which allows creating abstractions of different level by using the labeled transition systems apparatus, compositions of which may be converted to Petri nets and analyzed by the relevant means, is proposed. This method allows researching properties of the system, which can’t be analyzed manually, since the number of threads allocated for executing the code is measured by hundreds of thousands (in Pascal/Volta/Turing architectures).
Result. A formalized specification of the analyzed system could be obtained due to the transition system apparatus usage. The model was analyzed for the presense of deadlocks (siphons) and traps and the absence of dead transitions and places. The sets of basis and minimum deadlocks and traps were obtained. Model aliveness was proved due to the fact each deadlock includes at least one of the traps.
Conclusions. The proposed method allows to create models of different abstraction levels, which allows carrying out further analysis by automated means. The possibilities of studying the model characteristics created by the combination of transition systems and Petri Networks apparatuses were presented. The developed approach allows simplifying and reducing the processes of verification and testing of multithreaded applications in computer systems that use video adapters.
Download full text! (On Ukrainian).
Keywords: Transit System, Nvidia CUDA, Petri Networks, Model Design.
- Nvidia Data Center Nvidia. [online] Available at:<https://www.nvidia.com/en-us/data-center/> [Accessed 11 Nov. 2018].
- TOP500 Lists. TOP500 Supercomputer Sites. [online] Available at:<https://www.top500.org/lists Nvidia Data Center Nvidia, https://www.nvidia.com/en-us/data-center/> [Accessed 11 Nov. 2018].
- Arnold, A. 1994. Finite Transition Systems: Semantics of Communicating Systems. Paris: Prentice Hall, 177 p.
- Kryvyi, S.L., Boyko, Y.V., Pogorilyy, S.D., Boretskyi, O.F., Glybovets, M.M., 2017. “Design of Grid Structures on the Basis of Transition Systems with the Substantiation of the Correctness of Their Operation”. Cybernetics and Systems Analysis, 53 (1), pp 105–114.
https://doi.org/10.1007/s10559-017-9911-0 - Kotov, V.E., 1984. Petri nets. Moscow: Nauka, 157 p. (In Russian).
- Murata, T., 1989. Petri nets: properties, analysis and applications. In Proc. of the IEEE, 77, pp. 541-580.
https://doi.org/10.1109/5.24143 - Ben-Ari, M., 1993. Mathematical Logic for Computer Science. Prentice Hall International (UK) Ltd, 305 p.
- Clarke, E.M, Jr., GRUMBERG, O., PELED, D.A, 1999. Model Checking, MIT Press, ISBN 0-262-03270-8, 330 p.
- Kryvyi, S.L., Pogorilyy, D., Slynko, M.S., 2018. “Formalized method of designing applications in GPGPU technology”. Proceedings of the 11-th international scientific and practical conference on programming UkrPROG’2018, T.2, pp.12-20 (In Ukrainian).
- Kryvyi, S.L., 2015. Linear Diophantine constraints and their application. Chernivtsi: “Bukrek” Publishing House, pp. 223-224 (In Ukrainian).
Received 26.11.18
