Фабунмі Сунмаде Кунле Формальні моделі клієнт-серверних систем в ком­позиційних мовах паралельного програмування

Краткое описание

Фабунмі Сунмаде Кунле, тимчасово не працює: «Формальні моделі клієнт-серверних систем в ком­позиційних мовах паралельного програмування» (01.05.03 - математичне та програмне забезпечення обчислювальних машин і систем). Спецрада Д 26.001.09 у Київському національному університеті імені Тараса Шевченка

Київський національний університет імені Тараса Шевченка
Міністерство освіти і науки України
Київський національний університет імені Тараса Шевченка
Міністерство освіти і науки України
Кваліфікаційна наукова
праця на правах рукопису
Фабунмі Сунмаде Кунле
УДК 004.415,681.3
ДИСЕРТАЦІЯ
ФОРМАЛЬНІ МОДЕЛІ КЛІЄНТ-СЕРВЕРНИХ СИСТЕМ В
КОМПОЗИЦІЙНИХ МОВАХ ПАРАЛЕЛЬНОГО ПРОГРАМУВАННЯ
01.05.03 – Математичне та програмне забезпечення
обчислювальних машин і систем
Подається на здобуття наукового ступеня кандидата фізико-математичних наук
Дисертація містить результати власних досліджень. Використання ідей,
результатів і текстів інших авторів мають посилання на відповідне джерело
_______________________________(підпис, ініціали та прізвище здобувача)
Науковий керівник Буй Дмитро Борисович,
доктор фіз.-мат. наук, професор
Київ – 2019

ЗМІСТ
ВСТУП ................................................................................................................... 15
РОЗДІЛ 1 РОЗВИТОК ОСНОВНИХ ПОНЯТЬ ПРОГРАМУВАННЯ ............ 21
1.1 Проста мова програмування SIPL та її формалізація .......................... 22
1.1.1 Синтаксис мови SIPL.................................................................... 23
1.1.2 Семантика мови SIPL. .................................................................. 26
1.1.3 Програмні алгебри........................................................................ 31
1.1.4 Побудова семантичного терму.................................................... 34
1.1.5 Підалгебри програмної алгебри .................................................. 37
1.2 Основні принципи композиційно-номінативного підходу ................. 42
1.3. Формалізація програмних понять......................................................... 47
1.4 Програмні системи .................................................................................. 50
1.4.1 Рівні конкретизації даних ............................................................ 52
1.4.2. Рівні конкретизації функцій та композицій.............................. 55
1.4.3 Рівні конкретизації дескрипцій ................................................... 56
Висновки до розділу 1................................................................................... 57
РОЗДІЛ 2. ПАРАЛЕЛІЗМ В ПРОГРАМУВАННІ............................................. 58
2.1 Різновиди паралелізму ............................................................................ 59
2.2 Паралелізм шляхом обміну повідомленнями та паралелізм через
спільну пам’ять.................................................................................... 62
2.3 Підходи до паралелізму через спільну пам’ять в режимі почергового
виконання............................................................................................. 65
2.4 Методи суджень про паралельні програми та їх класифікація .......... 69
Висновки до розділу 2................................................................................... 75
РОЗДІЛ 3 ДОВЕДЕННЯ ВЛАСТИВОСТЕЙ ПРОГРАМ В КОМПОЗИЦІЙНО
- НОМІНАТИВНИХ МОВАХ IPCL.................................................................... 76
3.1 Актуальність використання паралелізму зі спільною пам’яттю........ 76
3.2 Мова IPCL. Синтаксис ............................................................................ 79
3.3. Композиційна семантика мов класу IPCL ........................................... 80
3.4. Два види властивостей програм IPCL.................................................. 86
3.5 Методика доведення властивостей програм IPCL............................... 88
14
3.5.1. Побудова моделі. Транзиційна система .................................... 89
3.5.2 Розстановка міток та визначення функції Step.......................... 92
3.5.3 Спрощена модель за відсутності локальних даних................... 95
3.6 Доведення властивостей програм IPCL ................................................ 98
3.6.1 Рівнопотужність двох типів властивостей в IPCL .................... 98
3.6.2 Схема доведення властивостей в IPCL..................................... 103
3.6.3 Приклад застосування методу доведення властивостей в IPCL
..................................................................................................... 104
3.7 Висновки щодо методу доведення властивостей в IPCL.................. 106
Висновки до розліду 3................................................................................. 110
РОЗДІЛ 4. MULTITHREADING МОДЕЛІ КОМПОЗИЦІЙНОЇ МОВИ IPCL
............................................................................................................................... 113
4.1 Системи паралельного виконання програм в IPCL ........................... 114
4.2 Модель динамічного стану транзиційної моделі із породженням та
приєднанням паралельних програм ................................................ 116
4.2.1 Модифікований стан транзиційної моделі IPCL..................... 117
4.2.2 Семантика операцій start та join................................................ 119
4.2.3 Семантика функцій fork, lock, unlock в транзиційній моделі IPCL
..................................................................................................... 121
4.3 Семантика операцій test_and_set та swap в транзиційній моделі
виконання програм IPCL.................................................................. 125
4.4 Еквівалентність двох систем паралельного виконання програм...... 131
Висновки до розділу 4................................................................................. 134
ВИСНОВКИ......................................................................................................... 136
СПИСОК ВИКОРИСТАНИХ ДЖЕРЕЛ........................................................... 140

Список литературы

ВИСНОВКИ
В дисертаційній роботі проведено ретельний порівняльний аналіз
існуючих формальних методів, застосовних до проблеми, а також
запропоновано більш адекватну модель паралельного виконання із
породженням екземплярів програм. Проведено дослідження запропонованого
розширення та надано його характеристику.
Головний результат дисертаційної роботи – розробка композиційних
моделей, розширення мови специфікації та методів верифікації програмних
систем, що розв’язують практично важливі задачі специфікації клієнтсерверних систем та верифікації часткової коректності даного класу
програмного забезпечення у галузі програмного забезпечення
обчислювальних машин і систем (або ж – комп’ютерних наук). Розроблені
моделі та розширення методів мають суттєве значення для підвищення якості
та надійності програмних систем.
В результаті проведеної роботи вирішено такі наукові задачі:
1. Побудовано та досліджено нове розширення композиційних мов
специфікацій, що дає можливість адекватно моделювати клієнтсерверні системи з динамічним породженням програм.
2. Проведено аналіз двох підходів до породження нових програм у
паралельному середовищі, сконструйовано їх моделі у
композиційному підході. Показано переваги обох підходів.
3. Шляхом уточнення механізму породження паралельних програм
створено нову композиційно-номінативну модель та обґрунтовано
адекватність серверному середовищу класичних клієнт-серверних
систем. Це дає можливість не тільки більш точно відображати
поведінку клієнт-серверних систем, а й підвищує виразність мови для
моделювання поведінки таких паралельних систем.
137
4. Визначено та досліджено клас композиційно-номінативних мов з
композиціями породження та приєднання паралельних програм під
час виконання, а також визначено базові функції в рамках цих мов,
що дозволило розширити засоби подання паралельної взаємодії
програм.
5. Для побудованої моделі доведено, за яких умов вона буде
рівнопотужною з класом паралельних композиційних інтерлівінгових
мов (IPCL), що дозволяє спростити судження над програмами у таких
випадках.
6. Адаптовано метод верифікації властивостей для класу серверних
програм на введених композиційних мовах, що дозволяє ефективно
проводити доведення властивостей у новому класі мов.
7. Для обґрунтування ефективності запропонованого методу його
апробовано на актуальних клієнт-серверних системах для їх
верифікації.
У дисертаційній роботі запропоновано розширення композиційнономінативних паралельних мов (Interleaving Parallel Composition Languages,
IPCL) та моделі виконання (включаючи модель стану програми), які є більш
адекватним поданням для паралельних систем з динамічним породженням
програм (що є найбільш поширеним у програмуванні). На підставі уточнення
механізму породження паралельних програм побудовано нову композиційнономінативну модель та обґрунтовано адекватність серверному середовищу
класичних клієнт-серверних систем. Побудовано та досліджено клас
композиційно-номінативних мов з композиціями породження та приєднання
паралельних програм під час виконання, а також подано ряд базових функцій
у цих мовах (атомарні та інші). Для побудованої моделі показано, за яких умов
вона буде рівнопотужною з класом мов IPCL. Адаптовано метод верифікації
138
властивостей у класі серверних програм на введених композиційних мовах.
Сформульовано та доведено теорему, яка визначає умови, при яких введене
розширення моделі еквівалентне існуючій моделі багатоекземплярного
виконання у IPCL.
Таким чином, наукова новизна полягає у наступному:
• побудовано та досліджено нове розширення композиційних мов
специфікацій, що дає можливість адекватно моделювати клієнтсерверні системи з динамічним породженням програм;
• проведено аналіз підходів до породження нових програм у
паралельному середовищі, побудовано їх моделі у композиційному
підході;
• на підставі уточнення механізму породження паралельних програм
побудовано нову композиційно-номінативну модель та
обґрунтовано її адекватність серверному середовищу класичних
клієнт-серверних систем, а також – прагматичну повноту цієї моделі;
• побудовано та досліджено клас композиційно-номінативних мов з
композиціями породження та приєднання паралельних програм під
час виконання, а також подано ряд базових функцій у цих мовах
(атомарні та інші);
• для побудованої моделі показано, за яких умов вона буде
рівнопотужною з класом мов IPCL;
• адаптовано метод верифікації властивостей у класі серверних
програм на введених композиційних мовах.
Дослідження має як теоретичне, так і практичне значення одержаних
результатів. Результати роботи можуть використовуватись для специфікації та
139
верифікації паралельних систем з динамічним породженням екземплярів
програм, що взаємодіють через спільну пам’ять.
Отримані результати впроваджено у навчальний процес за освітньою
програмою «Інформатика» спеціальності 122 «Комп’ютерні науки» на
факультеті комп’ютерних наук та кібернетики Київського національного
університету імені Тараса Шевченка.
Також запропоновані методи застосовано для доведення властивостей
реальних клієнт-серверних програмних систем [179].