DOI: https://doi.org/10.20535/SRIT.2308-8893.2020.3.01

Метод семантичної верифікації застосувань у технології GPGPU

Serhii L. Kryvyi, Sergiy D. Pogorilyy, Maksym S. Slynko, Artem A. Kramov

Анотація


Запропоновано метод розроблення та верифікації застосувань для систем з масовим паралелізмом на основі відеоадаптерів від компанії NVIDIA, який дозволяє створювати абстракції різних рівнів за допомогою апарата розмічених транзиційних систем. Композиції таких систем трансформуються в мережі Петрі, які далі аналізуються відповідними засобами. Метод також дає змогу створювати моделі на різних рівнях абстракції, а їх властивості можуть специфікуватися формулами темпоральної логіки. Це дозволяє досліджувати властивості систем з масовим паралелізмом, які майже неможливо аналізувати вручну, оскільки кількість потоків у новітніх архітектурах відеоадаптерів (Pascal, Volta, Amper, Тюрінг), виділених для виконання коду, вимірюється сотнями тисяч або мільйонами.

Ключові слова


CUDA; графічні процесори (GPU); графічні обчислення загального призначення (GPGPU); транзиційна система; мережа Петрі; побудова моделі

Повний текст:

PDF (English)

Посилання


Nvidia Data Center – Nvidia, 2018. [Online]. Available: https://www.nvidia.com/ en-us/data-center/. Accessed on: 2019, March 14.

TOP500 Lists TOP500 Supercomputer Sites, 2018. [Online]. Available: https://www.top500.org/lists. Accessed on: 2019, March 14.

A.V. Anisimov, S.D. Pogorilyy, and D.Yu. Vitel, “About the Issue of Algorithms formalized Design for Parallel Computer Architectures”, Applied and Computational Mathematics, vol. 12, no. 2, pp.140–151, 2013.

A. Arnold, Finite Transition Systems: Semantics of Communicating Systems. Paris, France: Prentice Hall, 1994, 177 p.

T. Murata, “Petri nets: properties, analysis and applications”, in Proc. of the IEEE, 77:541.80, 1989.

M. Ben-Ari, Mathematical Logic for Computer Science. UK: Prentice Hall International Ltd, 1993, 305 p.

E.M. Clarke, Jr., O. Grumberg, and D.A. Peled, Model Checking. USA: MIT Press, 1999.

S.D. Pogorilyy, S.L. Kryvyi, and M.S. Slynko, “Model justification of GPU-based applications”, Control Systems and Computers, vol. 4, pp. 46–56, 2018.

S.L. Kryvyi, Linear Diophantine constraints and their applications. Chernivtsi: Bukrek Publishing House, 2015.

S.L. Kryvyi, S.D. Pogorilyy, and M.S. Slynko, “Transition systems as method of designing applications in GPGPU technology”, in Proc. 11-th international scientific and practical conference on programming UkrPROG’2018.

S.L. Kryvyi et al., “Design of Grid Structures on the Basis of Transition Systems with the Substantiation of the Correctness of Their Operation”, Cybernetics and Systems Analysis, vol. 53, no. 1, pp.105–114, New York, USA: Springer Science + Business Media, January 2017.


Пристатейна бібліографія ГОСТ


1. Nvidia Data Center – Nvidia, 2018. [Online]. Available: https://www.nvidia.com/ en-us/data-center/. Accessed on: 2019, March 14.

2. TOP500 Lists TOP500 Supercomputer Sites, 2018. [Online]. Available: https://www.top500.org/lists. Accessed on: 2019, March 14.

3. A.V. Anisimov, S.D. Pogorilyy, and D.Yu. Vitel, “About the Issue of Algorithms formalized Design for Parallel Computer Architectures”, Applied and Computational Mathematics, vol. 12, no. 2, pp.140–151, 2013.

4. A. Arnold, Finite Transition Systems: Semantics of Communicating Systems. Paris, France: Prentice Hall, 1994, 177 p.

5. T. Murata, “Petri nets: properties, analysis and applications”, in Proc. of the IEEE, 77:541.80, 1989.

6. M. Ben-Ari, Mathematical Logic for Computer Science. UK: Prentice Hall International Ltd, 1993, 305 p.

7. E.M. Clarke, Jr., O. Grumberg, and D.A. Peled, Model Checking. USA: MIT Press, 1999.

8. S.D. Pogorilyy, S.L. Kryvyi, and M.S. Slynko, “Model justification of GPU-based applications”, Control Systems and Computers, vol. 4, pp. 46–56, 2018.

9. S.L. Kryvyi, Linear Diophantine constraints and their applications. Chernivtsi: Bukrek Publishing House, 2015.

10. S.L. Kryvyi, S.D. Pogorilyy, and M.S. Slynko, “Transition systems as method of designing applications in GPGPU technology”, in Proc. 11-th international scientific and practical conference on programming UkrPROG’2018.

11. S.L. Kryvyi et al., “Design of Grid Structures on the Basis of Transition Systems with the Substantiation of the Correctness of Their Operation”, Cybernetics and Systems Analysis, vol. 53, no. 1, pp.105–114, New York, USA: Springer Science + Business Media, January 2017.