Slynko M. Research and development of formalized methods of application design in GPGPU technology

The use of tools of the algorithmic design stage for applications in GPGPU technology was investigated in the thesis and the formalized method of parallel application design for massively parallel GPU-based computing systems was created. A comprehensive high-performance application design and verification method for systems that include GPUs to perform general purpose calculations was created. The proposed method allows using the tools of the algorithmic design phase, namely - algebras of algorithms, transition systems, Petri networks, automaton models and formulas of linear-temporal logic to increase the application performance and guarantee its reliability. The advantages of this method include the ability to model the system under analysis at different levels of abstraction, which allows using both deductive verification and classical testing at a high level of abstraction, and automated methods of verification of lower level logic, such as the model verification. The obtained design method is used to solve the problem of clustering using the GPU computing power and verification of the resulting system. The analysis identified a synchronization error that could not be detected by traditional testing. A regular scheme of Johnson's algorithm was built using the SAA-M mathematical apparatus. The scheme served as the basis for the formation of parallel schemes of the algorithm using GPGPU specifics and CUDA architecture. A parallel CAA-M scheme of Johnson's algorithm is constructed on the basis of a sequential parametric CAA scheme. A method of parallelization of the algorithm for the CUDA software and hardware platform is proposed. The scientific novelty of the obtained results is that for the first time the apparatus of systems of algorithmic algebras and transition systems were used to formalize applications in GPGPU technology; a comprehensive application design and verification method was created, which allows to solve the problem of complexity of engineering design of applications for modern heterogeneous systems; the created method was tested on examples of the implementing solutions for several problems, in particular - clustering problem and all pair shortest path graph problem (Johnson's algorithm). The obtained results have not only theoretical but also practical significance, as they can be used both for designing new and for analyzing existing applications to identify potential failure paths in it.