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

Размещено на http://allbest.ru

1Харківський національний університет імені В. Н. Каразіна

2Харківський національний університет радіоелектроніки)

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

1Мороз О.Ю., 1Толстолузька О.Г., 2Толстолузький Є.Д.



Вступ

Аналіз показує, що у відомих системах проектування паралельних програм (СПИН) широко використовуються методи статичної та динамічної верифікації [1-3].

У СННН основою верифікації є прогін та налагодження паралельних програм на конкретних значеннях числових даних. Відомі також спеціалізовані системи (наприклад, MATHCAD, MAPLE) верифікації з урахуванням одиниць виміру фізичних величин [4-6]. Засоби цих систем залежать від мови програмування та засновані на введенні до вихідного коду додаткових специфікацій фізичних величин та пов'язані з символьною обробкою, що ускладнює їхнє практичне використання, знижує ефективність результатів та обмежує сфери застосування [6].

На сьогодні визнається, що кардинальним вирішенням цієї проблеми має бути створення інтелектуальних технологій автоматичного проєктування мультипаралельних програмних засобів [1-3, 6-8].

Необхідність високої ефективності паралельного програмного забезпечення вимагає суттєвого розширення складу факторів, що враховуються при формальній розробці часопараметризованих мультипаралельних програм [8-14]:

- особливостей алгоритмів задач, що розв'язуються, які описують у вигляді традиційних послідовних програм мовою високого рівня (Сі, С++, Фортран тощо);

- складу методів паралельної обробки даних, який може бути використаний при синтезі часових паралельних програм (суміщення незалежних операцій, конвеєрний метод, кодово-матричний метод, декомпозиційний метод, метод мультипаралельної суміші алгоритмів);

- особливостей архітектури та конфігурацій паралельних процесорів та багатопроцесорних обчислювальних систем, наприклад, клас паралельної обчислювальної системи (SMP, MPP, NUMA), тип процесорів, топології міжпроцесорних комунікацій (повнозв'язна система, загальна шина, кільце, гіперкуб тощо);

- ієрархія пам'яті, можливість та час паралельного доступу до пам'яті різних рівнів; організація міжпроцесорного обміну даними, спосіб синхронізації роботи процесорів та необхідні часові витрати тощо.);

- часових характеристик паралельних процесорів та багатопроцесорних обчислювальних систем: тривалість операцій, тактова частота, надійність, тощо;

- склад конкретної конфігурації паралельної обчислювальної системи (кількість функціональних блоків/процесорів та їх зв'язок тощо);

- системи вимог та обмежень (час вирішення, тактова частота, складність/вартість, надійність/достовірність), які висуваються користувачами до характеристик процесу паралельного вирішення задач;

- одиниць виміру фізичних величин, що надаються даними вихідних послідовних програм.

Формальний та автоматичний характер технологій проєктування часпараметризованих мультипаралельних програм робить винятково актуальною задачу розробки засобів автоматичної верифікації та візуалізації результатів усіх етапів проектування з метою оперативної оцінки людиною коректності та достовірності синтезованих програмно-апаратних об'єктів [15-17].



Виклад основного матеріалу

Домовимося вважати, що поняття конструкція послідовних та паралельних програм визначається як сукупність специфікації даних, специфікації операцій\функцій, специфікації інформаційно-керівних зв'язків, специфікації моментів початку реалізації операцій\функцій та специфікації одиниць виміру фізичних величин.

Для специфікації таких програм, як правило, використовується текстова (алгоритмічною мовою) та графічна (наприклад, мовою UML, Unified Modeling Language) форми подання.

Необхідно відзначити, що UML- діаграми часто використовують при створенні багатопотокових, паралельних та розподілених програм [18, 19]. Це дозволяє скоротити час створення закінченої моделі програми (тобто деякого її спрощеного уявлення).

Основні побічні ефекти такого підходу:

a) засобами UML неможливо поєднати розроблені ракурси докупи, тобто, створити специфікацію, придатну для отримання з неї машинних кодів;

b) зміст моделі, як правило, неформалізовано [19].

На відміну від прийнятого в даний час трактування паралельних програм, часпараметризована мультипаралельна програма визначається як конструкція, яка містить у явному вигляді специфікації наступних категорій інформації (рис. 1):

- множина об'єктів - даних, над якими повинні виконуватися дії (що задаються складом операцій/функцій алгоритмічної мови високого рівня);

- множина дій (операцій/функцій), які мають бути виконані над даними для вирішення задачі;

- множина статичних зв'язків, що задають відносини упорядкованості операцій/функцій за даними та управлінню;

- упорядкованість операцій/функцій у динаміці паралельного обчислювального процесу, що задається множиною моментів часу початку виконання операцій/функцій;

- поділ множини операцій/функцій на часові фрагменти (множинні часові оператори, МЧО), що включають сукупність операцій/функцій, виконання яких починається одночасно в конкретний момент дискретного часу;

- розподіл множини даних на фрагменти даних, що поставлені в однозначну відповідність множинним часовим операторам і використані у відповідні моменти дискретного часу;

- наявність інформації про розбиття множини команд різних фрагментів на підмножини (нитки), що виконуються відповідними модулями/процесорами;

- наявність інформації про одиниці виміру фізичних величин даних.

Рис. 1. Склад категорій інформації специфікованих часопараметризованих мультипаралельних програм.

Принциповими відмінностями ЧПМП від традиційних статичних паралельних програм, що застосовуються у відомих паралельних процесорах (наприклад, з довгим командним рядком (VLIW), з управлінням потоком даних (FLOW) та багатопроцесорних ОС (класів SMP, NUMA, MPP CLUSTER), є:

- явне відображення у конструкціях паралельних/ послідовних програм фактору часу, як визначального параметру паралельних процесів;

- використання при проєктуванні часпараметризованих програм раціонального складу (що відповідає заданим вимогам/обмеженням різних прикладних областей) методів паралельної обробки даних;

- облік у конструкціях часопараметризованих мультипаралельних програм особливостей конкретних архітектур та конфігурацій різних класів паралельних процесорів та обчислювальних систем;

- використання під час виконання паралельних програм принципу «часового управління на кожному такті» на відміну від принципу управління на основі «потоку команд» програми та «потоку даних» програми, прийнятих у відомих паралельних процесорах та обчислювальних систем;

- використання у програмах базових і похідних одиниць виміру (семантики) величин обробки (крім обробки лише числових значень даних, як це має місце у переважній більшості традиційних послідовних та паралельних програмах);

- відображення в явному вигляді в конструкціях часових мультипаралельних програм різних вимог і обмежень, що задаються користувачами (наприклад, забезпечення необхідного часу виконання програми, заданої частоти тактової обробки даних та ін.).

Значне розширення складу категорій інформації, які

специфікуються часопараметризованими мультипаралельними програмами вимогає розробки нових засобів верифікації такого класу паралельних програм.

Постановка задачі семантико-числової верифікації технологій формального синтезу програмних засобів. На даний час основними способами отримання гарантій відповідності системи призначення є тестування і верифікація [20].

Тестування (Testing) визначається як «будь-який вид діяльності, в рамках якої шляхом реального виконання будь- яких завдань (тестових прогонів) перевіряється робота або системи в цілому, або її складової частини». Прийнято розрізняти два види тестування - статичне та динамічне тестування. Статичне тестування визначається як «тестова діяльність, пов'язана з аналізом результатів розробки програмного забезпечення шляхом перевірки програмних кодів, наскрізного контролю та перевірки програми без запуска машиною, тобто «перевірки за столом». Динамічне тестування «складається з прогону програми та порівняння її фактичної поведінки з очікуваною» поведінкою.

Під верифікацією (Verification) деякого об'єкта/системи розуміється «повний набір перевірок, яким піддається система для отримання гарантій її відповідності своєму призначенню». До таких перевірок можуть входити жорсткий набір функціональних тестів, контроль пропускної спроможності, перевірка надійності тощо. Для підвищення конструктивності викладу надалі розумітимемо під верифікацією «повну об'єктивну перевірку відповідності об'єкта певної точно визначеної специфікації». Зазначимо, що, на відміну від верифікації під «підтвердженням правильності» (validation), розуміється «деяка суб'єктивна оцінка ймовірної відповідності призначенню в передбачуваних умовах функціонування» [21]. Під «точно визначеною специфікацією», задоволення якої є критерієм коректності об'єкту проєктування, що верифікується, далі розуміється наступний склад даних:

- клас об'єкту проектування - програмний, апаратний чи апаратно-програмний;

- функціональність - склад завдань, які вирішуються об'єктом проєктування та специфікованих текстами послідовних програм;

- склад вимог і/або обмежень, що пред'являються до об'єкту (наприклад, продуктивність, пропускна здатність, час виконання завдання, тактова частота обробки даних, складність/вартість, надійність/достовірність тощо).

Технологію верифікації визначимо як сукупність формальних методів верифікації та програмних засобів реалізації. Концептуальна модель технології верифікації часопараметризованих мультипаралельних програм представлена на рис. 2.

Рис. 2. Концептуальна модель технології верифікації часопараметризованих мультипаралельних програм.

Розглянемо призначення різних компонентів архітектури технології верифікації ЧПМП програм.

Символ 0 (рис.2) є Базою Даних «Sem» і забезпечує:

- зберігання одиниць вимірювання фізичних величин різних прикладних областей, що використовуються для перевірки семантичної коректності формального синтезу програмних та апаратних засобів паралельних обчислювальних систем;

- склад заданих користувачами одиниць виміру фізичних величин конкретних завдань.

База даних «Soft»» (символ 1, рис.2) містить такі основні дані, що використовуються для верифікації процесів формального синтезу паралельних програмних засобів:

- вихідні тексти послідовних програм завдань, для яких синтезуються часові паралельні програми;

- склад підтримуючих верифікатором типів даних, операторів/функцій мови програмування високого рівня (наприклад, Сі) та процедур обміну повідомленнями;

- бібліотеку тривалості виконання (у процесорних тактах) операторів/функцій/процедур процесорами різних типів (наприклад, суперскалярного типу, VLIW, FLOW).

Синтезатор графів, представлений символом 2 (рис.2), здійснює синтез семантико-числової специфікації графів задач. Результатами роботи синтезатора графів є:

· семантико-числова специфікація (СЧС) вихідного тексту послідовної програми;

· графічна специфікація вихідної послідовної програми.

Символ 3 (рис.2) - Верифікатор графів задач із програмною орієнтацією. Забезпечує компіляційно-семантичну (CSV) та декомпіляційно-семантичну (DSV) верифікацію графів вихідних програм програмно- орієнтованих задач та структур їх семантико-числової специфікації.

Символ 4 (рис.2) - Синтезатор ЧПМП моделей здійснює формальний синтез часових мультипаралельних моделей вихідних послідовних програм, синтезованих з урахуванням характеристик архітектури паралельних процесорів/ОС та заданих вимог/обмежень. Результатом роботи синтезатора ЧПМП моделей є СЧС часпараметризованої архітектурно-орієнтованої моделі вихідної послідовної програми.

Символ 5 (рис.2) - Верифікатор часових паралельних Soft-моделей. Забезпечує компіляційно-семантичну (CSV) та декомпіляційно-семантичну (DSV) верифікацію часових мультипаралельних моделей вихідних послідовних програм, орієнтованих на конкретні класи процесорів/ОС та задані вимоги/обмеження.

Символ 6 (рис.2) - Синтезатор ЧПМП програм, на основі часпараметризованої архітектурно-орієнтованої моделі вихідної послідовної програми, що представлена відповідними семантико-числовими специфікаціями, проєктує ЧПМП програму з урахуванням вимог та обмежень замовника та класу паралельної обчислювальної системи (S).

Символ 7 (рис.2) - Верифікатор структур СЧС часових паралельних програм. Забезпечує компіляційно-семантичну (CSV) та декомпіляційно-семантичну (DSV) верифікацію структур семантико-числової специфікації синтезованих ЧПМП програм.

Символ 8 (рис.2) - Синтезаційний транслятор автоматично синтезує тексти часопараметризованих мультипаралельних програм та часові моделі їх виконання з урахуванням вимог та обмежень, що задаються користувачами.

Символ 9 (рис.2) - Верифікатор текстів часових паралельних програм. Забезпечує декомпіляційно- семантичну верифікацію текстів синтезованих часових мультипаралельних програм (з урахуванням типів та розмірностей даних, складу обчислювальних та керуючих операторів/функцій, засобів обміну даними та операторів часової синхронізації процесів).

Символ 10 (рис.2) - Синтезатор моделей процесів виконання ЧПМП програм забезпечує синтез множини моделей процесів, що задовольняють вимогам та обмеженням замовника.

Символ 11 (рис.2) - Верифікатор моделей процесів виконання паралельних програм. Забезпечує компіляційно-семантичну (CSV) декомпіляційно-семантичну (DSV) верифікацію часових моделей синтезованих текстів мультипаралельних програм.

Символ 12 (рис.2) - Блок оцінки показників ефективності ЧПМП програм здійснює розрахунок показників ефективності паралельних алгоритмів та програм (часу паралельної реалізації програми, прискорення, ефективності) залежно від кількості паралельних процесорних елементів.

Символ 13 (рис.2) - Візуалізатор результатів верифікації. Забезпечує зручну для користувачів наочну форму представлення вихідних результатів технології верифікації ЧПМП програм.

Символ 14 (рис.2) - Оцінювач достовірності верифікації. Забезпечує генерацію операторів - «дефектів» - зовнішніх впливів різних типів, що спотворюють відповідні статичні і тимчасові елементи семантико-числових і графічних специфікацій об'єктів, що верифікуються, і виконує оцінку достовірності як відношення кількості виявлених дефектів до кількості дефектів, фактично введених у паралельну програму.

Проілюструємо результати роботи технології верифікації ЧПМП програм на простому прикладі. На рис. 3 представлена вихідна послідовна програма написана мовою високого рівня (Сі-програма).

Рис. 3. Вихідна послідовна програма (мовою Сі).

До складу вихідних даних входять також фрагмент бази даних одиниць виміру фізичних величин (табл. 1) та перелік даних, що задаються користувачем (табл. 2).



Таблиця 1.

Фрагмент семантичної бази даних «SEM».

KODRAZM	RAZM	KOD RAZM	SEM
2	м	14	рад/с
3	кг	15	м/(с*с)
4	с	16	рад/(с*с)
5	А	17	1/м
6	К	18	кг/(м*м*м)
7	моль	19	м*м*м/кг
8	кд	20	А/(м*м)
9	рад	21	А/м
10	сР	22	моль/(м*м*м)
11	м*м	23	1/с
12	м*м*м	24	м*м/с
13	м/с	25	кд/(м*м)

Таблиця 2.

Структура US_SEM одиниць вимірювання, що задаються користувачем

N OP	REZ	VHOD VIH	KOD SEM
3	a	0	2
4	b	0	2
5	c	0	2
11	s	1	2
12	t	1	11



Таблиця 3.

Базова структура BF операторів вихідної програми

На першому етапі (символ 2 рис. 2) здійснюється автоматичний синтез структур BF і CF (табл. 3 представляє BF) семантико-числової специфікації для вихідної послідовної програми (рис. 3), а також візуалізація отриманого графа (рис.4).



Рис. 4. Граф вихідної послідовної програми.

Базова структура BF (табл. 3) описує номери та склад операторів Pj задачі (масив N), їх типи (масив TYP), число вхідних (масив SJD) та вихідних (масив WJD) зв'язків кожного оператора Pj, ідентифікатори операторів (масив RES), покажчики початку ланцюжків сполучених і зовнішніх операторів (масиви NSJ, NWJ) для кожного оператора послідовної програми. Синтез структур BF і CF СЧС здійснюється відповідно до методики, викладеної в [22]. Виходячи зі структур СЧС BF і CF, здійснюється графічна візуалізація вихідної послідовної програми у вигляді графа (рис. 4). Побудова графа здійснюється за допомогою засобів автоматичної візуалізації паралельних апаратно-програмних об'єктів, описаних у [23 ].

На рис. 5 представлені результати другого етапу технології (символ 3 на рис. 2). програма верифікація автоматичний візуалізація семантичний



Рис. 5. Результати компіляційної верифікації структур семантико-числової специфікації вихідної послідовної програми та її графа (View of test results).

Синтез семантико-числової специфікації BF_SEM послідовної програми (символ 4, рис.2) показано у табл. 4. У таблиці прийнято такі позначення: масив RAZM - одиниці виміру вихідних даних та даних - результатів виконання операцій: «м» - метр, «ні» - відсутність обчисленого значення вихідної змінної, «безрозмір.» - безрозмірна величина, «м* м», «м*м*м» - синтезовані одиниці виміру похідних величин.

Перевірка семантичної коректності структур СЧС BF_SEM, CF_SEM вихідної послідовної програми здійснюється шляхом порівняння розрахованих одиниць вимірювання даних, що відповідають вихідним операторам синтезованої структури BFSEM вихідної програми з одиницями вимірювання вихідних даних, заданими користувачем.



Таблиця 4.

Структура BF_SEM- результат синтезу одиниць виміру операторів вихідної Сі-програми.



Висновки

1. Розроблена технологія семантико-числової верифікації часопараметризованих мультипаралельних програм забезпечує перевірку синтаксичної та часової коректності формального синтезу структур семантико-числової специфікації перерахованих вище об'єктів верифікації в динаміці проєктування цих об'єктів з одночасною перевіркою збігу одиниць вимірювання фізичних величин, отриманих та одиниць вимірювання вхідних та вихідних даних задачі, що задаються користувачами.

2. Вихідними даними та основою для підтримки автоматичного характеру верифікації є формовані на всіх етапах синтезу структури семантико-числової специфікації (послідовних програм задач; часових паралельних моделей задач; часопараметризованих паралельних програм).

3. Формальний характер процесів верифікації часопараметризованих мультипаралельних програм заснований на побудові їх математичних моделей у термінах теорії множин, використанні для специфікації об'єктів статичних і часових структур семантико-числової специфікації та на формальних перетвореннях структур СЧС (і об'єктів, що їх представляють) з використанням бібліотеки операцій алгебри просторово-часової семантико-числової специфікації.



Список використаних джерел

1. Коцовський В. М. Теорія паралельних обчислень : навчальний посібник. Ужгород: ПП «АУТДОР-Шарк», 2021. 188 с.

2. Кузьменко Б.В., Чайковська О.А. Технологія розподілених систем та паралельних обчислень. (конспект лекцій, частина 1. Розподілені об'єктні системи, паралельні обчислювальні системи та паралельні обчислення, паралельне програмування на основі МРІ) Навчальний посібник. К.: Видавничий центр КНУКІМ, 2011. 126. с

3. Мороз О.Ю., Толстолузька О.Г., Савченко Р.В. Аналіз існуючих технологій верифікації паралельних програм. Вісник Харківського національного університету імені В. Н. Каразіна, Серія «Математичне моделювання. Інформаційні технології. Автоматизовані системи управління», 46, 2020. 76-81.

4. Кобильник Т. П. Системи комп'ютерної математики: Maple, Mathematica, Maxima. Дрогобич : Редакційно-видавничий відділ ДДПУ імені Івана Франка, 2008. 316 с.

5. Жалдак М. І., Лапінський В. В., Шут М. І. Комп'ютерно-орієнтовані засоби навчання математики, фізики, інформатики. Інформатика. 2006. №3-4. С. 3-96.

6. Інформаційні технології: Системи комп'ютерної математики [Електронний ресурс] : навч. посіб. для студ. спеціальності «Автоматизація та комп'ютерно-інтегровані технології» / І. В. Кравченко, В. І. Микитенко; КПІ ім. Ігоря Сікорського . Київ : КПІ ім. Ігоря Сікорського, 2018. 243с.

7. Сайт Української команди розподілених обчислень. - Режим доступу: http://distributed.org.ua/.

8. Толстолузька О. Г., Мороз О.Ю., Толстолузький Д.О. Метод компеляційно-семантичної верифікації часопараметризованих мультипаралельних програм. Computer Science and Cybersecurity, ISSNE 4(4), 2016. C. 26-34.

9. Семеренко В. П. Технології паралельних обчислень: навчальний посібник. Вінниця: ВНТУ, 2018. 104 с.

10. Дорошенко А.Ю. Паралельні обчислювальні системи. Методичний посібник і конспект лекцій. Київ: Видавничий дім «КМ Академія», 2013. 46 с.

11. Коцовський В. М. Теорія паралельних обчислень. Частина І: Методичний посібник. Ужгород: Видавництво УжНУ «Говерла», 2019. 51 с.

12. Рольщиков В.Б. Технології розподілених систем та паралельних обчислень. Конспект лекцій. Одеса: ОДЕКУ 2016. 155 с.

13. Youngjoo Woo, Seon Yeong Park, and Euiseong Seo. Virtual battery: A testing tool for power-aware software. Journal of Systems Architecture, 2013. URL: https://doi.org/10.1016/ j.sysarc.2013.06.006.

14. Шликов В. В., Данілова В. А. Високопродуктивні розподілені обчислювальні системи: Практикум [Електронний ресурс]: навч. посіб. для студ. спеціальності 122 «Комп'ютерні науки», спеціалізації «Інформаційні технології в біології та медицині»; КПІ ім. Ігоря Сікорського. Київ: КПІ ім. Ігоря Сікорського, 2018. 108 с.

15. Ясько М. М. Навчальний посібник до вивчення курсів «Паралельна обробка даних» та «Мови обчислень та кластерні системи» [Текст] / М. М. Ясько. Д.: РВВ ДНУ, 2010. 76с.

16. Навчальний посібник з дисципліни Системи візуалізації та розпізнавання образів [навчальний посібник] / Смолій В. В., Савицька Я. А., Місюра М.Д., Шкарупило В. В. // K.: ФОП Ямчинський О.В., 2020. 200 с.

17. Foster, Ian. Designing and Building Parallel Programs [Text] / Ian Foster - AddisonWesley, Inc. Boston, MA, 1995. 381pp.

18. Benjamin Kormann, Dmitry Tikhonov, and Birgit Vogel-Heuser. Automated plc software testing using adapted UML sequence diagrams. IFAC Proceedings Volume. URL: https://doi.org/10.3182/20120523-3-RO-2023.00148.

19. Навчальні ресурси СумДУ. University online learning ecosystem. Підходи до аналізу і проектування інформаційних систем. URL: https://elearning.sumdu.edu.ua/ free_content/lectured:de 1 c9452f2a161439391120eef364dd8ce4d 8e5e/20151203140326/204841/index.html

20. Великий тлумачний словник сучасної української мови: 250 000 / Вячеслав Тимофійович Бусел (уклад. і голов. ред.). К.; Ірпінь : Перун, 2007. 1736 с.

21. Проектування інформаційних систем: Загальні питання теорії проектування ІС (конспект лекцій) [Електронний ресурс]: навч. посіб. для студ. спеціальності 122 «Комп'ютерні науки» / КПІ ім. Ігоря Сікорського; уклад.: О.Є. Коваленко, Л. М. Добровська. Київ : КПІ ім. Ігоря Сікорського, 2020. 192с.

22. Поляков Г. А., Шматков С. И., Толстолужская Е. Г. Толстолужский Д. А. Синтез и анализ параллельных процессов в адаптивных времяпараметризованных вычислительных системах. Х.: ХНУ имени В.Н. Каразина, 2012. 672с.

23. Поляков Г. А., Онищенко В. В. Визуализация статико-динамических объектов автоматического проектирования мультипараллельных цифровых устройств. Системы обработки информации. Х. : ХВУ, 2004. Вып. 7(35) С. 169-177.

Размещено на Allbest.ru

...