Sistemnì Doslìdženâ ta Informacìjnì Tehnologìï (Dec 2020)

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

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

DOI
https://doi.org/10.20535/SRIT.2308-8893.2020.3.01
Journal volume & issue
no. 3

Abstract

Read online

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

Keywords