Метод семантичної верифікації застосувань у технології GPGPU
An application development and verification method for massively parallel systems using NVIDIA GPUs is proposed. The method allows creating models at different levels of abstraction using the apparatus of marked transition systems. The compositions (product) of such systems are transformed into a Pe...
Saved in:
| Date: | 2020 |
|---|---|
| Main Authors: | , , , |
| Format: | Article |
| Language: | English |
| Published: |
The National Technical University of Ukraine "Igor Sikorsky Kyiv Polytechnic Institute"
2020
|
| Subjects: | |
| Online Access: | http://journal.iasa.kpi.ua/article/view/213203 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | System research and information technologies |
Institution
System research and information technologies| _version_ | 1856543503983575040 |
|---|---|
| author | Kryvyi, Serhii L. Pogorilyy, Sergiy D. Slynko, Maksym S. Kramov, Artem A. |
| author_facet | Kryvyi, Serhii L. Pogorilyy, Sergiy D. Slynko, Maksym S. Kramov, Artem A. |
| author_sort | Kryvyi, Serhii L. |
| baseUrl_str | |
| collection | OJS |
| datestamp_date | 2021-01-19T12:18:25Z |
| description | An application development and verification method for massively parallel systems using NVIDIA GPUs is proposed. The method allows creating models at different levels of abstraction using the apparatus of marked transition systems. The compositions (product) of such systems are transformed into a Petri net, which are then analyzed by appropriate means. The proposed method allows specifying model properties by temporal logic formulas. This allows studying the properties of massively parallel systems which is almost impossible to analyze manually, since the number of execution threads in the latest NVIDIA video adapter architectures (Pascal, Volta, Turing, Ampere) is measured in hundreds of thousands or millions. |
| first_indexed | 2025-07-17T10:26:48Z |
| format | Article |
| id | journaliasakpiua-article-213203 |
| institution | System research and information technologies |
| language | English |
| last_indexed | 2025-07-17T10:26:48Z |
| publishDate | 2020 |
| publisher | The National Technical University of Ukraine "Igor Sikorsky Kyiv Polytechnic Institute" |
| record_format | ojs |
| spelling | journaliasakpiua-article-2132032021-01-19T12:18:25Z Method of semantic application verification in GPGPU technology Метод семантической верификации приложений в технологии GPGPU Метод семантичної верифікації застосувань у технології GPGPU Kryvyi, Serhii L. Pogorilyy, Sergiy D. Slynko, Maksym S. Kramov, Artem A. CUDA graphical processing units (GPU) General Purpose Graphics Computing (GPGPU) transition system Petri net model design CUDA графічні процесори (GPU) графічні обчислення загального призначення (GPGPU) транзиційна система мережа Петрі побудова моделі CUDA графические процессоры (GPU) графические вычисления общего назначения (GPGPU) транзиционная система сеть Петри построение модели An application development and verification method for massively parallel systems using NVIDIA GPUs is proposed. The method allows creating models at different levels of abstraction using the apparatus of marked transition systems. The compositions (product) of such systems are transformed into a Petri net, which are then analyzed by appropriate means. The proposed method allows specifying model properties by temporal logic formulas. This allows studying the properties of massively parallel systems which is almost impossible to analyze manually, since the number of execution threads in the latest NVIDIA video adapter architectures (Pascal, Volta, Turing, Ampere) is measured in hundreds of thousands or millions. Предложен метод разработки и верификации приложений для систем с массовым параллелизмом на основе видеоадаптеров от компании NVIDIA, который позволяет создавать абстракции различных уровней с помощью аппарата размеченных транзиционных систем. Композиции таких систем трансформируются в сети Петри, которые далее анализируются соответствующими средствами. Метод позволяет создавать модели на различных уровнях абстракции, а их свойства могут специфицироваться формулами темпоральной логики. Это позволяет исследовать свойства систем с массовым параллелизмом, которые практически невозможно анализировать вручную, так как количество потоков в новейших архитектурах видеоадаптеров (Pascal, Volta, Amper, Тьюринг), выделенных для выполнения кода, измеряется сотнями тысяч или миллионами. Запропоновано метод розроблення та верифікації застосувань для систем з масовим паралелізмом на основі відеоадаптерів від компанії NVIDIA, який дозволяє створювати абстракції різних рівнів за допомогою апарата розмічених транзиційних систем. Композиції таких систем трансформуються в мережі Петрі, які далі аналізуються відповідними засобами. Метод також дає змогу створювати моделі на різних рівнях абстракції, а їх властивості можуть специфікуватися формулами темпоральної логіки. Це дозволяє досліджувати властивості систем з масовим паралелізмом, які майже неможливо аналізувати вручну, оскільки кількість потоків у новітніх архітектурах відеоадаптерів (Pascal, Volta, Amper, Тюрінг), виділених для виконання коду, вимірюється сотнями тисяч або мільйонами. The National Technical University of Ukraine "Igor Sikorsky Kyiv Polytechnic Institute" 2020-12-07 Article Article application/pdf http://journal.iasa.kpi.ua/article/view/213203 10.20535/SRIT.2308-8893.2020.3.01 System research and information technologies; No. 3 (2020); 7-22 Системные исследования и информационные технологии; № 3 (2020); 7-22 Системні дослідження та інформаційні технології; № 3 (2020); 7-22 2308-8893 1681-6048 en http://journal.iasa.kpi.ua/article/view/213203/223554 Copyright (c) 2021 System research and information technologies |
| spellingShingle | CUDA графічні процесори (GPU) графічні обчислення загального призначення (GPGPU) транзиційна система мережа Петрі побудова моделі Kryvyi, Serhii L. Pogorilyy, Sergiy D. Slynko, Maksym S. Kramov, Artem A. Метод семантичної верифікації застосувань у технології GPGPU |
| title | Метод семантичної верифікації застосувань у технології GPGPU |
| title_alt | Method of semantic application verification in GPGPU technology Метод семантической верификации приложений в технологии GPGPU |
| title_full | Метод семантичної верифікації застосувань у технології GPGPU |
| title_fullStr | Метод семантичної верифікації застосувань у технології GPGPU |
| title_full_unstemmed | Метод семантичної верифікації застосувань у технології GPGPU |
| title_short | Метод семантичної верифікації застосувань у технології GPGPU |
| title_sort | метод семантичної верифікації застосувань у технології gpgpu |
| topic | CUDA графічні процесори (GPU) графічні обчислення загального призначення (GPGPU) транзиційна система мережа Петрі побудова моделі |
| topic_facet | CUDA graphical processing units (GPU) General Purpose Graphics Computing (GPGPU) transition system Petri net model design CUDA графічні процесори (GPU) графічні обчислення загального призначення (GPGPU) транзиційна система мережа Петрі побудова моделі CUDA графические процессоры (GPU) графические вычисления общего назначения (GPGPU) транзиционная система сеть Петри построение модели |
| url | http://journal.iasa.kpi.ua/article/view/213203 |
| work_keys_str_mv | AT kryvyiserhiil methodofsemanticapplicationverificationingpgputechnology AT pogorilyysergiyd methodofsemanticapplicationverificationingpgputechnology AT slynkomaksyms methodofsemanticapplicationverificationingpgputechnology AT kramovartema methodofsemanticapplicationverificationingpgputechnology AT kryvyiserhiil metodsemantičeskojverifikaciipriloženijvtehnologiigpgpu AT pogorilyysergiyd metodsemantičeskojverifikaciipriloženijvtehnologiigpgpu AT slynkomaksyms metodsemantičeskojverifikaciipriloženijvtehnologiigpgpu AT kramovartema metodsemantičeskojverifikaciipriloženijvtehnologiigpgpu AT kryvyiserhiil metodsemantičnoíverifíkacíízastosuvanʹutehnologíígpgpu AT pogorilyysergiyd metodsemantičnoíverifíkacíízastosuvanʹutehnologíígpgpu AT slynkomaksyms metodsemantičnoíverifíkacíízastosuvanʹutehnologíígpgpu AT kramovartema metodsemantičnoíverifíkacíízastosuvanʹutehnologíígpgpu |