Слинько М. С. Дослідження і створення формалізованих методів проектування застосувань в технології GPGPU

В роботі досліджено використання інструментальних засобів алгоритмічного етапу проектування для застосунків в технології GPGPU та сформовано формалізовану методику створення паралельних застосувань для програмних систем із відеоадаптерами. На основі проведених досліджень створено комплексний метод проектування та верифікації високопродуктивних застосувань для програмних систем, які включають відеоадаптери для виконання обчислень загального призначення, який дозволяє використати інструментальні засоби алгоритмічного етапу проектування, а саме – алгебри алгоритмів, транзиційні системи, мережеві, автоматні моделі та формули лінійно-темпоральної логіки для підвищення продуктивності паралельних застосувань а також забезпечення їх надійності. До переваг цього методу відносяться можливість моделювання системи, що розглядається, на різних рівнях абстракції, що дозволяє задіяти як дедуктивну верифікацію або класичне тестування на високому рівні абстракції, так і автоматизовані методи верифікації більш низкорівневої логіки, такі, як перевірка моделі. Отриманий метод застосовано для вирішення задачі кластеризації з використанням обчислювальних потужностей графічних адаптерів та верифікації отриманої системи. В ході дослідження було виявлено помилку синхронізації, яку неможливо було б виявити за допомогою традиційного тестування. Побудовано регулярну схему алгоритму Джонсона з використанням математичного апарату САА-М, яка є основною для формування паралельних схем алгоритму з використанням відеоадаптерів та архітектури обчислень CUDA. На основі послідовної параметричної САА-схеми побудовано паралельну САА-М-схему алгоритму Джонсона. Запропоновано метод розпаралелювання алгоритму Джонсона для програмно-апаратної платформи CUDA. Наукова новизна отриманих результатів полягає в тому, що вперше використано апарати систем алгоритмічних алгебр та транзиційних систем для формалізації застосувань в технології GPGPU; створено комплексний метод проектування та верифікації таких застосувань, який дозволяє вирішити проблему складності інженерного проектування застосувань для сучасних гетерогенних систем; апробовано створений метод на прикладах вирішення кількох задач, зокрема задачі кластеризації та задачі пошуку шляхів у графі (алгоритму Джонсона). Отримані результати мають не лише теоретичне, але і практичне значення, оскільки можуть бути використані як для проектування нових, так і для дослідження існуючих застосувань та виявлення в них помилок.