Transition systems as method of designing applications in GPGPU technology

The method of researching systems with high-performance computing support, based on the transition systems apparatus (discrete computational model), is proposed. Two variants of synchronous product limitations of transition systems that model tha Nvidia CUDA approach are proposed. transition systems...

Повний опис

Збережено в:
Бібліографічні деталі
Дата:2018
Автори: Kryvyi, S.L., Pogorilyy, S.D., Slynko, M.C.
Формат: Стаття
Мова:Ukrainian
Опубліковано: Інститут програмних систем НАН України 2018
Теми:
Онлайн доступ:https://pp.isofts.kiev.ua/index.php/ojs1/article/view/258
Теги: Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:Problems in programming
Завантажити файл: Pdf

Репозитарії

Problems in programming
id pp_isofts_kiev_ua-article-258
record_format ojs
resource_txt_mv ppisoftskievua/78/2ccd7f2252723bb19ec9771f077f8078.pdf
spelling pp_isofts_kiev_ua-article-2582024-04-28T11:37:22Z Transition systems as method of designing applications in GPGPU technology Формализованный метод проектирования приложений в технологии GPGPU Формалізований метод проектування застосувань в технології GPGPU Kryvyi, S.L. Pogorilyy, S.D. Slynko, M.C. Nvidia CUDA; GPGPU; SAA; Petri net; transition system UDC 004.4 Nvidia CUDA; GPGPU; САА; сети Петри; транзиционная система УДК 004.4 Nvidia CUDA; GPGPU; САА; мережі Петрі; транзиційна система УДК 004.4 The method of researching systems with high-performance computing support, based on the transition systems apparatus (discrete computational model), is proposed. Two variants of synchronous product limitations of transition systems that model tha Nvidia CUDA approach are proposed. transition systems that represent two types of instructions, process of the warp instruction execution, and the process of warp scheduling were described. GPGPU application execution model was formalized and its correctness was proved. Two variants of the relevant Petri net which allowed automatic or semi-automatic detection of design errors were obtained.Problems in programming 2018; 2-3: 012-020 Предложен метод исследования характеристик систем, использующих высокопроизводительные вычисления, основанный на аппарате транзиционных систем (дискретной модели вычислений). Предложено два варианта ограничений синхронного произведения транзиционных систем, моделирующих подход, использованный в архитектуре Nvidia CUDA. Описаны транзиционные системы, представляющие два типа инструкций, процесс выполнения инструкции варпа и работу планировщика варпа. Выполнена формализация модели выполнения GPGPU-приложения. Получено спецификацию вышеуказанного подхода и строго доказана его корректность. Спецификацию сведено к двум вариантам сетей Петри, которые позволяют выявлять ошибки проектирования в автоматическом или полуавтоматическом режиме.Problems in programming 2018; 2-3: 012-020 Запропоновано метод дослідження характеристик систем, що використовують високопродуктивні обчислення, який ґрунтується на апараті транзиційних систем (дискретної моделі обчислень). Запропоновано два варіанти обмежень синхронного добутку цих транзиційних систем, що моделюють підхід, використаний в архітектурі Nvidia CUDA. Описано транзиційні системи, що представляють два типи інструкцій, процес виконання інструкції варпом та роботу планувальника варпу. Виконано формалізацію моделі виконання GPGPU-застосування. Отримано специфікацію вищевказаного підходу та строго доведено його коректність. Специфікацію зведено до двох варіантів мереж Петрі, які дозволяють виявляти помилки проектування в автоматичному або напівавтоматичному режимі.Problems in programming 2018; 2-3: 012-020 Інститут програмних систем НАН України 2018-11-05 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/258 10.15407/pp2018.02.012 PROBLEMS IN PROGRAMMING; No 2-3 (2018); 12-20 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2-3 (2018); 12-20 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2-3 (2018); 12-20 1727-4907 10.15407/pp2018.02 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/258/252 Copyright (c) 2018 PROBLEMS OF PROGRAMMING
institution Problems in programming
baseUrl_str https://pp.isofts.kiev.ua/index.php/ojs1/oai
datestamp_date 2024-04-28T11:37:22Z
collection OJS
language Ukrainian
topic Nvidia CUDA
GPGPU
SAA
Petri net
transition system
UDC 004.4
spellingShingle Nvidia CUDA
GPGPU
SAA
Petri net
transition system
UDC 004.4
Kryvyi, S.L.
Pogorilyy, S.D.
Slynko, M.C.
Transition systems as method of designing applications in GPGPU technology
topic_facet Nvidia CUDA
GPGPU
SAA
Petri net
transition system
UDC 004.4
Nvidia CUDA
GPGPU
САА
сети Петри
транзиционная система
УДК 004.4
Nvidia CUDA
GPGPU
САА
мережі Петрі
транзиційна система
УДК 004.4
format Article
author Kryvyi, S.L.
Pogorilyy, S.D.
Slynko, M.C.
author_facet Kryvyi, S.L.
Pogorilyy, S.D.
Slynko, M.C.
author_sort Kryvyi, S.L.
title Transition systems as method of designing applications in GPGPU technology
title_short Transition systems as method of designing applications in GPGPU technology
title_full Transition systems as method of designing applications in GPGPU technology
title_fullStr Transition systems as method of designing applications in GPGPU technology
title_full_unstemmed Transition systems as method of designing applications in GPGPU technology
title_sort transition systems as method of designing applications in gpgpu technology
title_alt Формализованный метод проектирования приложений в технологии GPGPU
Формалізований метод проектування застосувань в технології GPGPU
description The method of researching systems with high-performance computing support, based on the transition systems apparatus (discrete computational model), is proposed. Two variants of synchronous product limitations of transition systems that model tha Nvidia CUDA approach are proposed. transition systems that represent two types of instructions, process of the warp instruction execution, and the process of warp scheduling were described. GPGPU application execution model was formalized and its correctness was proved. Two variants of the relevant Petri net which allowed automatic or semi-automatic detection of design errors were obtained.Problems in programming 2018; 2-3: 012-020
publisher Інститут програмних систем НАН України
publishDate 2018
url https://pp.isofts.kiev.ua/index.php/ojs1/article/view/258
work_keys_str_mv AT kryvyisl transitionsystemsasmethodofdesigningapplicationsingpgputechnology
AT pogorilyysd transitionsystemsasmethodofdesigningapplicationsingpgputechnology
AT slynkomc transitionsystemsasmethodofdesigningapplicationsingpgputechnology
AT kryvyisl formalizovannyjmetodproektirovaniâpriloženijvtehnologiigpgpu
AT pogorilyysd formalizovannyjmetodproektirovaniâpriloženijvtehnologiigpgpu
AT slynkomc formalizovannyjmetodproektirovaniâpriloženijvtehnologiigpgpu
AT kryvyisl formalízovanijmetodproektuvannâzastosuvanʹvtehnologíígpgpu
AT pogorilyysd formalízovanijmetodproektuvannâzastosuvanʹvtehnologíígpgpu
AT slynkomc formalízovanijmetodproektuvannâzastosuvanʹvtehnologíígpgpu
first_indexed 2024-09-16T04:07:39Z
last_indexed 2024-09-16T04:07:39Z
_version_ 1818568201106096128
fulltext Теоретичні та методологічні основи програмування © С.Л. Кривий, С.Д. Погорілий, М.С. Слинько, 2018 12 ISSN 1727-4907. Проблеми програмування. 2018. № 2–3. Спеціальний випуск УДК 004.4 ФОРМАЛІЗОВАНИЙ МЕТОД ПРОЕКТУВАННЯ ЗАСТОСУВАНЬ В ТЕХНОЛОГІЇ GPGPU С.Л. Кривий, С.Д. Погорілий, М.С. Слинько Запропоновано метод дослідження характеристик систем, що використовують високопродуктивні обчислення, який ґрунтується на апараті транзиційних систем (дискретної моделі обчислень). Запропоновано два варіанти обмежень синхронного добутку цих транзиційних систем, що моделюють підхід, використаний в архітектурі Nvidia CUDA. Описано транзиційні системи, що представляють два типи інструкцій, процес виконання інструкції варпом та роботу планувальника варпу. Виконано формалізацію моделі виконання GPGPU-застосування. Отримано специфікацію вищевказаного підходу та строго доведено його коректність. Специфікацію зведено до двох варіантів мереж Петрі, які дозволяють виявляти помилки проектування в автоматичному або напівавтоматичному режимі. Ключові слова: Nvidia CUDA, GPGPU, САА, мережі Петрі, транзиційна система. Предложен метод исследования характеристик систем, использующих высокопроизводительные вычисления, основанный на аппарате транзиционных систем (дискретной модели вычислений). Предложено два варианта ограничений синхронного произведения транзиционных систем, моделирующих подход, использованный в архитектуре Nvidia CUDA. Описаны транзиционные системы, представляющие два типа инструкций, процесс выполнения инструкции варпа и работу планировщика варпа. Выполнена формализация модели выполнения GPGPU-приложения. Получено спецификацию вышеуказанного подхода и строго доказана его корректность. Спецификацию сведено к двум вариантам сетей Петри, которые позволяют выявлять ошибки проектирования в автоматическом или полуавтоматическом режиме. Ключевые слова: Nvidia CUDA, GPGPU, САА, сети Петри, транзиционная система. The method of researching systems with high-performance computing support, based on the transition systems apparatus (discrete computational model), is proposed. Two variants of synchronous product limitations of transition systems that model tha Nvidia CUDA approach are proposed. transition systems that represent two types of instructions, process of the warp instruction execution, and the process of warp scheduling were described. GPGPU application execution model was formalized and its correctness was proved. Two variants of the relevant Petri net which allowed automatic or semi-automatic detection of design errors were obtained. Key words: Nvidia CUDA, GPGPU, SAA, Petri net, transition system. Вступ Майбутнє високопродуктивних обчислень (та так званих «exascale» обчислень) лежить в галузі систем з масовим паралелізмом [1]. В свою чергу, використання таких систем унеможливлює інженерне проектування і вимагає наявності формалізованого математичного апарату і методів представлення алгоритму. В роботі основний акцент ставиться на алгоритмічному етапі проектування. Алгоритмічний етап проектування є початковим та найменш технологічно забезпеченим. Але він впливає на подальший процес розробки та визначає її успіх в цілому. Ефективним методом алгоритмічного проектування і дослідження паралельних алгоритмів є використання алгебр алгоритмів, які дозволяють сформувати формули (схеми) алгоритмів, що залежать від різних параметрів, якими можуть виступати програмно-апаратні платформи, парадигми паралельного програмування тощо. Зокрема, В.М. Глушковим було запропоновано математичний апарат систем алгоритмічних (мікропрограмних) алгебр (САА) [2]. Приклад представлення GPGPU застосувань у апараті САА наведено у [3, 4]. Однак, хоч САА і дозволяють осягнути структуру застосування і проводити еквівалентні перетворення схеми застосування без прив’язки до апаратної архітектури, в них відсутня можливість темпорального моделювання та глибокого аналізу. Саме тому в роботі пропонується використання апарату транзиційних систем, що дозволяють створювати різнорівневі абстракції, та можуть бути зведені до мереж Петрі (МП), котрі підтримують темпоральне моделювання. На початку статті описуються особливості розробки застосувань в технології GPGPU, що є критичними для дослідження їх властивостей та моделювання. Далі описується метод проектування застосувань, що базується на використанні апарату транзиційних систем та їх синхронного добутку. Потім проводиться аналіз властивостей МП, що моделює гетерогенну систему в цілому. В процесі проектування систем визначення синхронного добутку виконується на етапі проектування, а використання МП, як специфікації, є засобом перевірки правильності прийнятих проектних рішень. Метод застосовується для обґрунтування властивостей процесу виконання застосувань на архітектурі Nvidia CUDA. При проектуванні, за наявності вихідного коду конкретного застосування можливо використати наведену модель для аналітичного обґрунтування його коректності, в тому числі, за допомогою автоматизованих засобів, таких як CPN Tools. Архітектури сучасних GPU від NVIDIA Інтенсивний розвиток графічних процесорів (GPU), призвів до створення пристроїв, які, окрім управління графічним дисплеєм, також дозволяють виконувати алгоритми неграфічних задач. CUDA (Computed Теоретичні та методологічні основи програмування 13 Unified Device Architecture) – це архітектура паралельних обчислень, розроблена компанією NVIDIA для спрощення програмування GPGPU за рахунок використання високорівневих API. Застосування, що працює в гетерогенному середовищі, обладнаному GPU, може бути розділене на наступні частини:  «хост» – блоки інструкцій, що виконуються на центральному процесорі;  функції-«ядра» – блоки інструкцій, що виконуються на GPU. Хост-блоки визначають контекст виконання функцій-ядер, займаються передачею даних між оперативною пам’яттю комп’ютера та пам’яттю GPU. Функції-ядра мають доступ до великої (до 655360 на відеоадаптерах архітектури Pascal) кількості потоків. За таксономією Флінна, принцип роботи CUDA пристроїв є близьким до принципу SIMD (Singe Instruction – Multiple Data), з деякими уточненнями: кожен потік не лише виконує одну й ту ж саму інструкцію над своєю підмножиною даних, але й може мати власний шлях виконання в залежності від заданих умов. Розробники CUDA називають такий підхід SIMT (Single Instruction, Multiple Thread), тобто одна інструкція виконується одночасно багатьма потоками, при чому поведінка кожного окремого потоку нічим не обмежується. У такий спосіб, основною програмною обчислювальною одиницею є потік. Всі GPU потоки структуровані у блоки однакового розміру, котрі, в свою чергу, групуються у сітку [5]. Блок потоків – це набір одночасно виконуваних потоків (насправді, не усі потоки виконуються одночасно, як буде показано нижче). Взаємодія між потоками в блоці досягається за рахунок механізму бар’єрної синхронізації. Також потоки в межах блоку мають доступ до спільної пам’яті. Розмір блоку залежить від апаратної платформи (на сучасних архітектурах, зокрема, Kepler, підтримуються блоки розмірами до 1024 потоків). Кожен блок має ідентифікатор, унікальний в межах сітки, а кожен поток – ідентифікатор, унікальний в межах блоку. Сітка – це масив блоків, що виконують одну і ту саму функцію-ядро. Кількість блоків у сітці визначається розмірністю даних та апаратною платформою. Обмін даними між блоками зазвичай відбувається з використанням глобальної пам’яті. Апаратна платформа GPU від Nvidia складається з набору потокових мультипроцесорів (streaming multiprocessor, SM). Блоки потоків розподіляються між SM таким чином, що всі потоки в межах блоку виконуються на одному мультипроцесорі, і в той же час, одному SM може бути поставлено у відповідність більше, ніж 1 блок. В свою чергу, мультипроцесор розділяє блок на групи по 32 потоки. Ця операція виконується для кожного блоку окремо, а утворені групи називаються варпами (warp). Як згадано вище, кожен SM працює за принципом SIMT, тобто всі потоки в межах варпу в один момент часу виконують одну і ту саму інструкцію. Таким чином, фізично паралельно виконуються лише потоки в межах одного варпу. Будь-яке розгалуження в інструкціях (умовні оператори тощо) призводить до того, що кожен шлях виконання буде обчислюватися окремо і послідовно. Кожен SM працює з багатьма варпами. SM має вбудований планувальник варпу та диспетчер інструкцій (в архітектурі Pascal їх може бути до 4-х). Планувальник обирає варп, інструкція якого може бути виконана, і передає контроль над обчислювальними ядрами його потокам. Якщо варп з будь-яких причин переходить в стан очікування (синхронізація, очікування доступу до пам’яті тощо), планувальник обирає для виконання інший варп, забезпечуючи постійне навантаження ядер SM. Враховуючи багаторівневість обчислювальної архітектури та велику кількість обчислювальних одиниць (потоків, блоків), дослідження і виправлення помилок проектування в ручному режимі є неможливим. Доцільно застосувати математичну модель загального типу, таку, як транзиційну систему, та використати апарат мереж Петрі для виявлення помилок в автоматичному або напівавтоматичному режимі. Транзиційні системи та мережі Петрі Як показано в [6], транзиційна система (ТС) – це система ),,,,( 0sTSA  , де  S – скінченна або нескінченна множина станів;  Т – скінченна або нескінченна множина переходів;  , – два відображення із Т в S, що ставлять у відповідність кожному переходу t два стани )(),( tt  , які називають відповідно початком і кінцем переходу t;  0s – початковий стан ТС. Нехай nAA ,...,1 – транзиційні системи, де ),,,,( ' 0sTSA iiiii  , ni ,...,1 . Обмеженням синхронізації називається підмножина Т множини )},...,{(\}){(...}){( 1   nTT , де  - тотожний перехід, який означає відсутність будь-якої дії в ТС. Елементи із Т називаються глобальними переходами. Якщо Tttt n  ),...,( 1 і it , то говорять, що ТС iA бере участь у переході t . Теоретичні та методологічні основи програмування 14 Кортеж ),,...,( 1 TAAA n називається добутком ТС nAA ,...,1 , які називаються компонентами A . Інтуїтивно глобальний перехід ),...,( 1 nttt  моделює можливі переходи в nAA ,...,1 . Якщо перехід it , то ТС iA не приймає участі у глобальному переході t . Мережа Петрі (МП) ),,,( 0MFTP зображує добуток ),,...,( 1 TAAA n ТС ),,,,( ' 0sTSA iiiii  , де  ji AA при ,ji  nji ,...,2,1,  , якщо nSSSP  ...21 , TT  , )}(&|),{()}(&|),{( iiiiii tststtsttsF   для деякого },...,,2,1{ ni , де it означає і-ту компоненту Tt , ),...,,( 0 2 0 1 00 nsssM  . Семантика добутку ТС і семантика МП, яка його зображує, узгоджуються в тому сенсі, що послідовність глобальних переходів ktt ,...,1 являє собою глобальну історію добутку ТС тоді і тільки тоді, коли вона є допустимою послідовністю спрацювань переходів в МП. Розробка моделі виконання CUDA-застосування З точки зору моделювання архітектури обчислень, виконання GPGPU-застосування можна представити у вигляді взаємодії таких систем:  ТС 1: моделює абстрактну інструкцію;  ТС 2: моделює варп, що містить набір інструкцій та послідовно їх виконує;  ТС 3: моделює виконання блоку на потоковому мультипроцесорі. Розглянемо функціональні можливості цих транзиційних систем. ТС 1. Залежно від мети моделювання, доцільно змінювати акцент в представленні інструкції у вигляді транзиційної системи. В роботі представлено 2 моделі:  ТС 1А: представляє собою узагальнену інформаційну інструкцію (рис. 1). Варто використовувати у випадках, коли потрібен прогноз ефективності застосування за рівнем використання певного ресурсу (наприклад, часу);  ТС 1Б: представляє собою детальну абстракцію обчислювальної інструкції. Варто використовувати у випадках, коли потрібен детальний аналіз «вузького місця» застосування. ТС 1А. Час виконання різних типів інструкцій може відрізнятися на кілька порядків (наприклад, арифметична інструкція в архітектурі Kepler виконується за 4 обчислювальні такти, а інструкція доступу до глобальної пам’яті може займати від 400 тактів). Абстрактна інформаційна інструкція моделюється простою транзиційною системою ) , }, , , , , ,{ }, , , , , ,({ 0654321543210 bppppppbbbbbb = BA  . Рис. 1. Представлення інформаційної інструкції у вигляді ТС Інтерпретація місць та переходів в даній ТС така: 0b – фіксація старту виконання; 1p – підготовка до виконання арифметичної операції; 1b – фіксація старту виконання арифметичної операції; 2p – виконання операції; 2b – арифметичну операцію виконано; 3p – перехід у стан завершення інструкції; 4p – формування запиту до пам’яті; 3b – фіксація старту запиту до пам’яті; Теоретичні та методологічні основи програмування 15 5p – процес отримання даних; 4b – фіксація отримання даних; 6p – перехід у стан завершення інструкції; 5b – інструкцію завершено. В цій моделі враховуються 2 типи інструкцій – арифметична та інструкція доступу до пам’яті. Втім, час доступу до різних видів пам’яті GPU відрізняється на порядки, тому в реальній моделі може бути доцільним виділення додаткових типів інструкцій, та, відповідно, додаткових місць та переходів за вищевказаним зразком. Також варто зазначити, що кожна реальна інструкція належить лише до одного з типів. З метою спрощення узагальненої моделі, вважаємо, що тип інструкції визначається випадковим чином. ТС 1Б. Обчислювальна інструкція (рис. 2) з акцентом на внутрішню будову моделюється наступною транзиційною системою ) , }, , , , , ,{ }, , , , , ,({ 0654321543210 bppppppbbbbbb = BB  . Рис. 2. Представлення обчислювальної інструкції у вигляді ТС Інтерпретація місць та переходів в даній ТС така: 0b – фіксація старту виконання; 1p – формування запиту операндів з пам’яті; 1b – фіксація старту запиту операндів з пам’яті; 2p – завантаження операндів; 2b – фіксація отримання операндів; 3p – перехід у стан завершення інструкції; 3b – інструкцію завершено; 4p – підготовка до виконання обчислень; 4b – фіксація старту виконання обчислень; 5p – процес виконання обчислень; 5b – обчислення завершено. 6p – перехід у стан завершення інструкції. ТС 2. Кожен варп містить набір інструкцій, що мають бути виконаними всіма його потоками. За моделлю SIMT інструкції надходять послідовно, а кожна з них виконується одночасно всіма потоками варпу (рис. 3). Такий протокол моделюється транзиційною системою ) , }, , , ,{ }, , , ,({ 043213210 arrrraaaaA =  . Рис. 3. ТС виконання інструкції варпом Інтерпретація місць та переходів в даній ТС така: 0a – фіксація стану деактивації варпа. Варп готовий до виконання наступної інструкції; Теоретичні та методологічні основи програмування 16 1r – активація варпа планувальником (даний варп отримує доступ до ресурсів SM для виконання однієї інструкції); 1a – фіксація стану активного варпу; 2 r – підготовка до виконання інструкції; 2a – фіксація стану варпу в процесі виконання інструкції («зайнятого» варпу); 3 r – отримання підтвердження про виконання інструкції; 3a – інструкцію виконано; 4 r – деактивація варпу (після переходу варп знову стає доступним для вибору планувальником). ТС 3. Як вказано вище, ТС 3 представляє собою виконання блоку на SM. Основною структурною одиницею в даному процесі за означенням відіграє планувальник варпу (рис. 4). Основні дії на цьому етапі включать вибір варпу та інструкції і забезпечення ексклюзивного доступу до обчислювальних ресурсів на час виконання кожної пари варп-інструкція. Ця пара дій має ітеративно виконуватися, поки всі інструкції не буде виконано на всіх варпах блоку. Такий процес моделюється транзиційною системою }, , , ,({ 3210 cccc=C ) , }, , , ,{ 04321 cqqqq  . Рис. 4. Представлення роботи планувальника варпу у вигляді ТС Інтерпретація місць та переходів в даній ТС наступна: 0c – фіксація старту планування; 1q – вибір варпу та інструкції; 1c – обрано пару варп-інструкція; 2q – початок виконання обраної інструкції для обраного варпу; 2c – фіксація стану очікування виконання інструкції; 3q – отримання підтвердження про виконання інструкції; 3c – фіксація виконання пари варп-інструкція; 4q – перехід до наступної ітерації. За наявністю сформованих транзиційних систем можна побудувати модель виконання застосування в архітектурі CUDA у вигляді синхронного добутку ТС 1А, 2, 3 з глобальними переходами: ),,(),,,(),,,(),,,(),,,{( 2243332221111 qrpqrppqrpqrT  )},,(),,,(),,,(),,,( 443365 qrqrpp  . (1) За множиною обмежень синхронного добутку 1T будуємо мережу Петрі, що моделює сумісну роботу всіх підсистем [6] (рис. 5). Після побудови мережі Петрі, виникає задача перевірки коректності отриманої моделі. В рамках статті перевіримо живучість такої системи. Характеристика «живучості» означає, що в отриманій моделі всі переходи будуть приймати участь у процесі її функціонування [6]. Якщо певні переходи в МП ніколи не спрацьовують, це означає, що проект системи побудовано неправильно, або ж він є надлишковим. Дослідимо МП на живучість у такий спосіб: перевіримо, чи досяжна кінцева розмітка з початкової, і чи всі переходи в цьому процесі спрацьовують. Початкова розмітка має вигляд: ),1,0,0,0,0,0,0,1,1(0 M тобто існує 1 планувальник варпу (токен в місці № 1), 1 інструкція для виконання (токен в місці № 2) та відсутня інструкція в процесі (токен в місці № 9). Кінцева розмітка має вигляд: ),1,0,0,0,0,0,0,0,1(kM Теоретичні та методологічні основи програмування 17 Рис. 4 МП, що представляє синхронний добуток ТС з множиною переходів 1T тобто всі інструкції виконано, активних варпів немає, планування не відбувається. Знайдемо розв’язки рівняння стану вигляду: ,0)( 0 0   MMxA MMxA k k (2) де A – матриця інцидентності МП. Для нашої МП рівняння стану має вигляд (табл. 1). Таблиця 1 t1 t2 t3 t4 t5 t6 t7 t8 t9 -(Mk – M0) S1 -1 0 0 0 0 0 0 0 1 0 S2 -1 0 0 0 0 0 0 0 0 1 S3 1 -1 0 0 -1 0 0 0 0 0 S4 0 1 -1 0 0 0 0 0 0 0 S5 0 0 1 -1 0 0 0 0 0 0 S6 0 0 0 0 1 -1 0 0 0 0 S7 0 0 0 0 0 1 -1 0 0 0 S8 0 0 0 1 0 0 1 -1 0 0 S9 -1 0 0 0 0 0 0 1 0 0 Застосовуючи алгоритм TSS [7] для вирішення рівняння стану з вищевказаною матрицею, отримуємо наступні вирішення рівняння стану з вищевказаною матрицею (табл. 2). Таблиця 2 t1 t2 t3 t4 t5 t6 t7 t8 t9 1 1 1 1 0 0 0 1 1 1 0 0 0 1 1 1 1 1 Теоретичні та методологічні основи програмування 18 Як видно з множини розв’язків, всі переходи в МП з вищевказаними початковою і кінцевою розмітками живі (значення, що відповідає кожному переходу, хоча б у одному з розв’язків є позитивним), крім того, в один момент часу виконуються переходи, що відповідають лише одному з можливих типів інструкцій. Недоліком МП на рис. 5 є неможливість покриття її позитивними інваріантами через наявність місця S2, яке представляє собою набір інструкцій для виконання, і тому живучість мережі в цілому (а не для конкретних пар початкової та кінцевої розміток) визначити неможливо. Крім того, важливо довести коректність взаємодії ТС 2 та ТС 3 незалежно від форми представлення інструкції. Для аналізу обох питань побудуємо іншу множину обмежень синхронного добутку ТС 1, 2, 3 (рис. 6), але цього разу як представлення інструкції використаємо ТС 1Б: ),,,(),,,(),,,(),,,(),,,{( 432221112  pppqrpqrT  )},,(),,,(),,,(),,,( 443365 qrqrpp  . (3) Рис. 6. МП, що представляє синхронний добуток ТС з множиною переходів 2T Перевіримо живучість МП на рис. 6. В цій мережі можливо знайти інваріанти переходів, незалежно від початкової і кінцевої розмітки. Для цього знайдемо розв’язки рівняння стану 0 xA . Матриця інцидентності має вигляд (табл. 3). Таблиця 3 t1 t2 t3 t4 t5 t6 t7 t8 t9 S1 -1 0 0 0 0 0 0 0 1 S2 -1 0 0 0 0 0 0 0 1 S3 1 -1 0 0 0 0 0 0 0 S4 0 1 -1 0 0 0 0 0 0 S5 0 0 1 -1 0 0 0 0 0 S6 0 0 0 1 -1 0 0 0 0 S7 0 0 0 0 1 -1 0 0 0 S8 0 0 0 0 0 1 -1 0 0 S9 0 0 0 0 0 0 1 -1 0 S10 0 0 0 0 0 0 0 1 -1 Теоретичні та методологічні основи програмування 19 Застосовуючи алгоритм TSS, отримуємо єдиний розв’язок рівняння стану: Таблиця 4 t1 t2 t3 t4 t5 t6 t7 t8 t9 1 1 1 1 1 1 1 1 1 Це означає, що всі переходи покриваються позитивними інваріантами, і мережа завжди буде живою. Висновки Основним результатом статті є узагальнена модель обчислень в архітектурі Nvidia CUDA, що базується на апараті транзиційних систем та мереж Петрі. Створення гетерогенних застосувань з використанням новітніх архітектур відеоадаптерів порушує нагальну проблему їх верифікації, при чому, концептуальні помилки бажано знаходити ще на етапі проектування., що досягається запропонованим підходом. В роботі пропонується використання математичного апарату транзиційних систем для отримання формалізованих специфікацій систем, що проектуються. Такі специфікації є апаратно-незалежними та інтуїтивно зрозумілими. Крім того, до переваг сформованої моделі належить можливість її трансформування до мережі Петрі, і подальшої верифікації автоматизованими засобами, такими як CPN Tools. Отримано узагальнену модель виконання застосування з використанням Nvidia CUDA, що надало можливість строго довести коректність підходу, що використовується у вищевказаній архітектурі. В роботі проведено дослідження двох властивостей системи – досяжності та структурної живучості. Однак поєднання апарату ТС та МП дозволяє також аналізувати контрольованість, структурну обмеженість, несуперечність тощо; дозволяє проводити аналіз циклів, пасток, дедлоків, інваріантів, тобто проводити максимальний набір досліджень для забезпечення надійного функціонування застосування. Література 1. Погорілий С.Д., Вітель Д.Ю., Верещинський О.А. Новітні архітектури відеоадаптерів. Технологія GPGPU. Частина 1. Реєстрація, зберігання і оброб. даних. 2012. Т. 14, № 4. 2. Pogorilyy S.D. & Shkulipa I. Yu. (2009) A Conception for Creating a System of Parametric Design of Parallel Algorithms and their Software Implementations. Cybernetics and System Analysis, Volume 45, Issue 6 (November 2009). P. 952–958. Springer Science and Business Media Inc. ISSN:1060-0396. 3. Pogorilyy S.D., Slynko M.S. (2016) Research and development of Johnson’s algorithm parallel schemes in GPGPU technology. In 10-th international scientific programming conference UKRPROG’2016. Kyiv. P. 105–112. 4. Pogorilyy S.D., Slynko M.S. & Rustamov Y.I. (2017) A formalized method of Johnson’s algorithm parallelization suitable for use in GPGPU technology. TWMS Journal of Pure and Applied Mathematics, V. 8, N.1. 2017. P. 12–21. 5. Погорелый С.Д., Бойко Ю.В., Трибрат М.И., Грязнов Д.Б. Анализ методов повышения производительности компьютеров с использованием графических процессоров и программно-аппаратной платформы CUDA. Математичні машини і системи. 2010. № 1. С. 40–54. 6. Бойко Ю.В., Кривий С.Л., Погорілий С.Д. та ін. Методи та новітні підходи до проектування, управління і застосування високопродуктивних ІТ-інфраструктур. – К.: ВПЦ «Київський університет». 2016. 447 с. 7. Кривий С.Л. Лінійні діофантові обмеження та їх застосування. Букрек: Чернівці. 2015. 224 с. References 1. POGORILYY S.D., VITEL D. Yu. & VERESCHINSKY O.A. (2012) Modern video adapter architectures. GPGPU technology. Part 1. Data registration, storage and processing. 14 (4). 2. POGORILYY S.D. & SHKULIPA I. Yu. (2009) A Conception for Creating a System of Parametric Design of Parallel Algorithms and their Software Implementations. Cybernetics and System Analysis, Volume 45, Issue 6 (November 2009) pages: 952 - 958. Springer Science and Business Media Inc. ISSN:1060-0396. 3. POGORILYY S.D., SLYNKO M.S. (2016) Research and development of Johnson’s algorithm parallel schemes in GPGPU technology. In 10- th international scientific programming conference UKRPROG’2016. Kyiv, pp. 105-112. 4. POGORILYY S.D., SLYNKO M.S. & RUSTAMOV Y.I. (2017) A formalized method of Johnson’s algorithm parallelization suitable for use in GPGPU technology. TWMS Journal of Pure and Applied Mathematics, V.8, N.1, 2017, pp. 12-21. 5. POGORILYY S.D., BOYKO Yu.V., TRYBRAT M.I., GRYAZNOV D.B. (2010) Analysis of the computer performance improvement methods using graphic processors and CUDA platform. Mathematical Machines and Systems, N.1, pp. 40-54. 6. BOYKO Yu.V., KRYVYI S.L., POGORILYY S.D. et al. (2016). Methods and latest approaches to the design, management and application of high-performance IT infrastructures. Publishing and printing center “Kyiv University”. 7. KRYVYI S.L. (2015). Linear Diophantine limits and their application. Chernivtsi: “Bukrek” Publishing House. Теоретичні та методологічні основи програмування 20 Про авторів: Кривий Сергій Лук’янович, доктор фізико-математичних наук, професор факультету комп’ютерних наук та кібернетики Київського національного університету імені Тараса Шевченка. Індекс Хірша (Google Scholar) – 17. Індекс Хірша (Scopus) – 4. Кількість наукових публікацій в українських виданнях – 150, Кількість наукових публікацій в зарубіжних виданнях – 60. http://orcid.org/0000-0003-4231-0691, Погорілий Сергій Дем’янович, доктор технічних наук, професор, завідувач кафедри комп’ютерної інженерії факультету радіофізики, електроніки та комп’ютерних систем Київського національного університету імені Тараса Шевченка. Індекс Хірша (Google Scholar) – 6. Індекс Хірша (Scopus) – 2. Кількість наукових публікацій в українських виданнях – 200. Кількість наукових публікацій в зарубіжних виданнях – 45. http://orcid.org/0000-0002-6497-5056, Слинько Максим Сергійович, аспірант 2-го року навчання факультету радіофізики, електроніки та комп’ютерних систем Київського національного університету імені Тараса Шевченка. Кількість наукових публікацій в українських виданнях – 2. Кількість наукових публікацій в зарубіжних виданнях – 1. http://orcid.org/0000-0001-9667-8729. Місце роботи авторів: Київський національний університет імені Тараса Шевченка, 03022, Київ, проспект Академіка Глушкова, 4г. Тел.: (044) 526 0522, E-mail: sdp@univ.net.ua, maxim.slinko@gmail.com mailto:sdp@univ.net.ua mailto:maxim.slinko@gmail.com