Equivalence of two parallel execution systems
The method for properties proof for parallel programs running multiple-instance interleaving with shared memory is investigated. Two systems for parallel execution of programs are considered and the justification of the mutual expressiveness of these two approaches are presented in this paper. The f...
Збережено в:
| Дата: | 2018 |
|---|---|
| Автори: | , |
| Формат: | Стаття |
| Мова: | Ukrainian |
| Опубліковано: |
Інститут програмних систем НАН України
2018
|
| Теми: | |
| Онлайн доступ: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/270 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Problems in programming |
| Завантажити файл: |  |
Репозитарії
Problems in programming| id |
pp_isofts_kiev_ua-article-270 |
|---|---|
| record_format |
ojs |
| resource_txt_mv |
ppisoftskievua/df/71a310df99a86248f09b12662ea673df.pdf |
| spelling |
pp_isofts_kiev_ua-article-2702024-04-28T11:37:23Z Equivalence of two parallel execution systems Эквивалентность двух систем параллельного выполнения Еквівалентність двох систем паралельного виконання Panchenko, T. V. Fabunmi, S. software correctness; safety property proof; concurrent program; interleaving; IPCL; composition-nominative languages; formal verification UDC 004.415, 681.3 корректность программного обеспечения; доказательство частичной корректности; параллельная программа; interleaving; IPCL; композиционно-номинативные языки; формальная верификация УДК 004.415, 681.3 коректність програмного забезпечення; IPCL; композиційно-номінативні мови; формальна верифікація УДК 004.415, 681.3 The method for properties proof for parallel programs running multiple-instance interleaving with shared memory is investigated. Two systems for parallel execution of programs are considered and the justification of the mutual expressiveness of these two approaches are presented in this paper. The first one is with a fixed yet parametric number of programs executing in parallel. The second one implements a generation model (start) and joining after the stop (join) of parallel programs (also called multithreading). The corresponding two basic functions are provided, and their semantics are given. Also, the semantics of other functions related to parallel execution, resource management and access synchronization are presented in this paper. The theorem on the (functional) equivalence of these two systems and its justification are presented. The program in this case is considered as a function over the data. It is argued that for an arbitrary program in one of the systems of parallelism it is possible to construct the corresponding program in another system, which returns the same result (that is, functionally equivalent). Only productive programs are considered here in the context of mutual expressiveness, because otherwise they "hang" and do not return any result, thus they are out of our scope. The obtained result allows us to move reasoning from the more complex system (by structure) with a dynamic generation of parallel program instances to the simpler system (for proofs) with a parametric number of identical programs executed in parallel. Questions for further research in this direction are also identified.Problems in programming 2018; 2-3: 093-098 Исследуется метод доказательства свойств параллельных программ, которые выполняются много экземплярно в режиме поочередного пошагового переключения и взаимодействуют через общую память. В работе рассмотрены две системы параллельного выполнения программ и приведено обоснование взаимной выразимости этих двух подходов. Один – с фиксированным, но параметрическим, количеством параллельно выполняемых программ. Второй – реализует модель порождения (start) и присоединения после остановки (join) параллельных программ (также называется multithreading). Введено соответствующие две базовые функции и задано их семантику. Также задана семантика других функций касательно параллельного выполнения, управления ресурсами и синхронизации доступа. Приведены теорема об (функциональной) эквивалентности двух систем и ее обоснование. Программа в данном случае рассматрива ется как функция над данными. Утверждается, что для произвольной программы в одной из систем параллелизма можно построить соответствующую ей программу в другой системе, которая возвращает тот же результат (то есть функционально эквивалентна). Только продуктивные программы рассматриваются здесь в контексте взаимной выразимости, поскольку в противном случае они "зависают" и не возвращают никакого результата, поэтому лежат вне области нашего рассмотрения. Полученный результат позволяет свести работу в более сложной (по строению) системе с динамическим порождением экземпляров к более простой (для доказательств) системе с параметрическим количеством одинаковых программ, выполняемых параллельно. Также указаны вопросы для дальнейших исследований в этом направлении.Problems in programming 2018; 2-3: 093-098 Досліджується метод доведення властивостей паралельних програм, що виконуються багатоекземплярно в режимі почергового покрокового переключення і взаємодіють через спільну пам’ять. У роботі розглянуто дві системи паралельного виконання програм та наведено обґрунтування взаємної виразності двох цих підходів. Один – з фіксованою, але параметричною, кількістю паралельно виконуваних програм. Другий – реалізує модель породження (start) і приєднання після зупинки (join) паралельних програм (також називається multithreading). Введено відповідні дві базові функції та задано їх семантику. Також наведено семантику інших функцій стосовно паралельного виконання, управління ресурсами та синхронізації доступу. Наведено теорему щодо (функціональної) еквівалентності двох систем та її обґрунтування. Програма в даному випадку розглядається як функція над даними. Стверджується, що для довільної програми в одній з систем паралелізму можна побудувати відповідну їй програму в іншій системі, яка повертає той самий результат (тобто є функціонально еквівалент ною). Тільки продуктивні програми розглядаються тут у контексті взаємної виразності, оскільки у протилежному випадку вони "зависають" і не повертають жодного результату, отже є за межами нашого розгляду. Отриманий результат дозволяє звести роботу у більш складній (за будовою) системі з динамічним породженням екземплярів до більш простої (для доведень) системи з параметричною кількістю однакових програм, виконуваних у паралель. Визначено також питання для подальших досліджень у цьому напрямку.Problems in programming 2018; 2-3: 093-098 Інститут програмних систем НАН України 2018-11-05 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/270 10.15407/pp2018.02.093 PROBLEMS IN PROGRAMMING; No 2-3 (2018); 93-98 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2-3 (2018); 93-98 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2-3 (2018); 93-98 1727-4907 10.15407/pp2018.02 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/270/264 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:23Z |
| collection |
OJS |
| language |
Ukrainian |
| topic |
software correctness safety property proof concurrent program interleaving IPCL composition-nominative languages formal verification UDC 004.415 681.3 |
| spellingShingle |
software correctness safety property proof concurrent program interleaving IPCL composition-nominative languages formal verification UDC 004.415 681.3 Panchenko, T. V. Fabunmi, S. Equivalence of two parallel execution systems |
| topic_facet |
software correctness safety property proof concurrent program interleaving IPCL composition-nominative languages formal verification UDC 004.415 681.3 корректность программного обеспечения доказательство частичной корректности параллельная программа interleaving IPCL композиционно-номинативные языки формальная верификация УДК 004.415 681.3 коректність програмного забезпечення IPCL композиційно-номінативні мови формальна верифікація УДК 004.415 681.3 |
| format |
Article |
| author |
Panchenko, T. V. Fabunmi, S. |
| author_facet |
Panchenko, T. V. Fabunmi, S. |
| author_sort |
Panchenko, T. V. |
| title |
Equivalence of two parallel execution systems |
| title_short |
Equivalence of two parallel execution systems |
| title_full |
Equivalence of two parallel execution systems |
| title_fullStr |
Equivalence of two parallel execution systems |
| title_full_unstemmed |
Equivalence of two parallel execution systems |
| title_sort |
equivalence of two parallel execution systems |
| title_alt |
Эквивалентность двух систем параллельного выполнения Еквівалентність двох систем паралельного виконання |
| description |
The method for properties proof for parallel programs running multiple-instance interleaving with shared memory is investigated. Two systems for parallel execution of programs are considered and the justification of the mutual expressiveness of these two approaches are presented in this paper. The first one is with a fixed yet parametric number of programs executing in parallel. The second one implements a generation model (start) and joining after the stop (join) of parallel programs (also called multithreading). The corresponding two basic functions are provided, and their semantics are given. Also, the semantics of other functions related to parallel execution, resource management and access synchronization are presented in this paper. The theorem on the (functional) equivalence of these two systems and its justification are presented. The program in this case is considered as a function over the data. It is argued that for an arbitrary program in one of the systems of parallelism it is possible to construct the corresponding program in another system, which returns the same result (that is, functionally equivalent). Only productive programs are considered here in the context of mutual expressiveness, because otherwise they "hang" and do not return any result, thus they are out of our scope. The obtained result allows us to move reasoning from the more complex system (by structure) with a dynamic generation of parallel program instances to the simpler system (for proofs) with a parametric number of identical programs executed in parallel. Questions for further research in this direction are also identified.Problems in programming 2018; 2-3: 093-098 |
| publisher |
Інститут програмних систем НАН України |
| publishDate |
2018 |
| url |
https://pp.isofts.kiev.ua/index.php/ojs1/article/view/270 |
| work_keys_str_mv |
AT panchenkotv equivalenceoftwoparallelexecutionsystems AT fabunmis equivalenceoftwoparallelexecutionsystems AT panchenkotv ékvivalentnostʹdvuhsistemparallelʹnogovypolneniâ AT fabunmis ékvivalentnostʹdvuhsistemparallelʹnogovypolneniâ AT panchenkotv ekvívalentnístʹdvohsistemparalelʹnogovikonannâ AT fabunmis ekvívalentnístʹdvohsistemparalelʹnogovikonannâ |
| first_indexed |
2024-09-16T04:07:40Z |
| last_indexed |
2024-09-16T04:07:40Z |
| _version_ |
1818568208131555328 |
| fulltext |
Паралельне програмування. Розподілені системи і мережі
© Т.В. Панченко, Sunmade Fabunmi, 2018
ISSN 1727-4907. Проблеми програмування. 2018. № 2–3. Спеціальний випуск 93
УДК 004.415, 681.3
ЕКВІВАЛЕНТНІСТЬ ДВОХ СИСТЕМ
ПАРАЛЕЛЬНОГО ВИКОНАННЯ
Т.В. Панченко, Sunmade Fabunmi
Досліджується метод доведення властивостей паралельних програм, що виконуються багатоекземплярно в режимі почергового
покрокового переключення і взаємодіють через спільну пам’ять. У роботі розглянуто дві системи паралельного виконання
програм та наведено обґрунтування взаємної виразності двох цих підходів. Один – з фіксованою, але параметричною, кількістю
паралельно виконуваних програм. Другий – реалізує модель породження (start) і приєднання після зупинки (join) паралельних
програм (також називається multithreading). Введено відповідні дві базові функції та задано їх семантику. Також наведено
семантику інших функцій стосовно паралельного виконання, управління ресурсами та синхронізації доступу. Наведено теорему
щодо (функціональної) еквівалентності двох систем та її обґрунтування. Програма в даному випадку розглядається як функція
над даними. Стверджується, що для довільної програми в одній з систем паралелізму можна побудувати відповідну їй програму
в іншій системі, яка повертає той самий результат (тобто є функціонально еквівалентною). Тільки продуктивні програми
розглядаються тут у контексті взаємної виразності, оскільки у протилежному випадку вони "зависають" і не повертають
жодного результату, отже є за межами нашого розгляду. Отриманий результат дозволяє звести роботу у більш складній (за
будовою) системі з динамічним породженням екземплярів до більш простої (для доведень) системи з параметричною кількістю
однакових програм, виконуваних у паралель. Визначено також питання для подальших досліджень у цьому напрямку.
Ключові слова: коректність програмного забезпечення, доведення часткової коректності, паралельна програма, interleaving,
IPCL, композиційно-номінативні мови, формальна верифікація.
Исследуется метод доказательства свойств параллельных программ, которые выполняются многоэкземплярно в режиме
поочередного пошагового переключения и взаимодействуют через общую память. В работе рассмотрены две системы
параллельного выполнения программ и приведено обоснование взаимной выразимости этих двух подходов. Один – с
фиксированным, но параметрическим, количеством параллельно выполняемых программ. Второй – реализует модель
порождения (start) и присоединения после остановки (join) параллельных программ (также называется multithreading). Введено
соответствующие две базовые функции и задано их семантику. Также задана семантика других функций касательно
параллельного выполнения, управления ресурсами и синхронизации доступа. Приведены теорема об (функциональной)
эквивалентности двух систем и ее обоснование. Программа в данном случае рассматривается как функция над данными.
Утверждается, что для произвольной программы в одной из систем параллелизма можно построить соответствующую ей
программу в другой системе, которая возвращает тот же результат (то есть функционально эквивалентна). Только
продуктивные программы рассматриваются здесь в контексте взаимной выразимости, поскольку в противном случае они
"зависают" и не возвращают никакого результата, поэтому лежат вне области нашего рассмотрения. Полученный результат
позволяет свести работу в более сложной (по строению) системе с динамическим порождением экземпляров к более простой
(для доказательств) системе с параметрическим количеством одинаковых программ, выполняемых параллельно. Также указаны
вопросы для дальнейших исследований в этом направлении.
Ключевые слова: корректность программного обеспечения, доказательство частичной корректности, параллельная программа,
interleaving, IPCL, композиционно-номинативные языки, формальная верификация.
The method for properties proof for parallel programs running multiple-instance interleaving with shared memory is investigated. Two
systems for parallel execution of programs are considered and the justification of the mutual expressiveness of these two approaches are
presented in this paper. The first one is with a fixed yet parametric number of programs executing in parallel. The second one implements a
generation model (start) and joining after the stop (join) of parallel programs (also called multithreading). The corresponding two basic
functions are provided, and their semantics are given. Also, the semantics of other functions related to parallel execution, resource
management and access synchronization are presented in this paper. The theorem on the (functional) equivalence of these two systems and
its justification are presented. The program in this case is considered as a function over the data. It is argued that for an arbitrary program in
one of the systems of parallelism it is possible to construct the corresponding program in another system, which returns the same result (that
is, functionally equivalent). Only productive programs are considered here in the context of mutual expressiveness, because otherwise they
"hang" and do not return any result, thus they are out of our scope. The obtained result allows us to move reasoning from the more complex
system (by structure) with a dynamic generation of parallel program instances to the simpler system (for proofs) with a parametric number of
identical programs executed in parallel. Questions for further research in this direction are also identified.
Key words: software correctness, safety property proof, concurrent program, interleaving, IPCL, composition -nominative languages,
formal verification.
Вступ. Постановка задачі
У роботах [1–3] та інших, де досліджується метод доведення властивостей програм у композиційних
мовах IPCL з почерговим паралелізмом (shared memory interleaving concurrency, системи зі спільною
пам’яттю та паралелізмом із почерговим переключенням), судження спираються на модель виконання
nА ||
mB || … || kC [1], тобто є певна кількість однотипних підпрограм, запущених паралельно, із
покроковим виконанням (операційна семантика) і поперемінною передачею управління між окремими
підпрограмами. Вказані кількості підпрограм (n, m, …, k ) є параметрами моделі, яка розглядається, і всі
судження проводяться для довільних їх значень одночасно, тобто – незалежно від кількості паралельно
виконуваних екземплярів підпрограм. Крайнім випадком такого виконання підпрограм може бути їх строго
послідовне виконання, одна за одною, але в загальному випадку матиме місце деяка траса комбінованого
покрокового виконання.
Паралельне програмування. Розподілені системи і мережі
94
Разом з тим, у реальних програмах часто застосовується техніка породження-завершення паралельних
підпрограм. Тобто, вводиться деяка специфічна функція start(P), яка породжує екземпляр підпрограми P (додає
+1 екземпляр до таких же, виконуваних паралельно, – зі стартом у точці входу, порожнім початковим даним
(або переданими локальними даними в якості параметра ініціації, якщо передбачено механізмом породження)
та доступом до спільного даного) і повертає код ID породженої підпрограми (ID процесу в операційних
системах, для внутрішнього обліку та можливості подальших звернень до нього), а також функція join(ID), яка
чекає на завершення підпрограми за кодом ID (раніше породженого екземпляру програми P), та після цього
продовжує призупинене (власне) виконання.
Далі наведено обґрунтування взаємної виразності двох підходів до паралельного виконання програм, яке
було сформульоване, зокрема, у [4]. Відповідно, буде розглянуто дві системи паралельного виконання програм.
Одна – з фіксованою, але параметричною, кількістю паралельно виконуваних програм [1–3]. Друга – що
реалізує модель породження (start) – приєднання після зупинки (join) паралельних програм (часто називається
multithreading). У IPCL [1–3] введемо відповідні дві базові функції та задамо їх семантику. Наведемо теорему
щодо еквівалентності двох систем.
Факт еквівалентності є важливим, оскільки дозволить звести роботу в більш складній за побудовою
системі з динамічним породженням екземплярів паралельних підпрограм до більш простої для доведень
системи з параметричною (але довільною, не фіксованою) кількістю однакових програм, виконуваних
паралельно в режимі почергового переключення.
Семантика динамічного породження (start) та приєднання (join) паралельних програм
Уточнимо семантику цих двох нових операцій в транзиційній моделі виконання [1–3].
По-перше, дещо модифікуємо подання самої моделі відносно [1–3] для зручності, дана зміна не впливає
на потужність моделі або виразну силу – лише додає можливість «масштабування» надалі.
Отже, стан будемо подавати у вигляді
𝑆 =
(
((
𝑚11
𝑚12
⋮
𝑚1𝑛1
) ,(
𝑚21
𝑚22
⋮
𝑚2𝑛2
) ,… , (
𝑚𝑘1
𝑚𝑘2
⋮
𝑚𝑘𝑛𝑘
)) ,
(
𝑑,(
𝑑11
𝑑12
⋮
𝑑1𝑛1
) ,(
𝑑21
𝑑22
⋮
𝑑2𝑛2
) ,… ,(
𝑑𝑘1
𝑑𝑘2
⋮
𝑑𝑘𝑛𝑘
)
)
)
,
де
ijm – мітка, в якій перебуває (паралельна) підпрограма номер j, яка є екземпляром деякої iP – для
моделі виконання 𝑃1
𝑛1|| 𝑃2
𝑛2|| … ||𝑃𝑘
𝑛𝑘, тобто 𝑚𝑖𝑗 ∈ 𝑀𝑖 – множина міток iP [1];
ijd – відповідне локальне дане цієї підпрограми – ijP ;
d – глобальне (спільне, загальнодоступне всім підпрограмам) дане,
кожне дане має номінативну структуру – набір пар «ім’я – значення».
В цій моделі кожний крок виконання має вигляд: (𝑚𝑖𝑗 , 𝑑, 𝑑𝑖𝑗) → (𝑚
′
𝑖𝑗 , 𝑑′, 𝑑′𝑖𝑗), тобто програма Pij,
знаходячись у мітці 𝑚𝑖𝑗, після виконання чергової інструкції перейде у мітку 𝑚′𝑖𝑗 та перетворить (можливо,
змінить) глобальне дане 𝑑 на 𝑑′, а локальне 𝑑𝑖𝑗 – на 𝑑′𝑖𝑗 . Таким чином, в стані S за один крок може змінитись
три компоненти.
Множину всіх станів можна задати для певної фіксованої кількості різновидів підпрограм k як
𝑆𝑡𝑎𝑡𝑒𝑠 = ⋃ {𝑠 ∈ ((𝑀1
𝑛1 , 𝑀2
𝑛2 , … ,𝑀𝑘
𝑛𝑘), (𝐷, 𝐷𝑛1 , 𝐷𝑛2 , … , 𝐷𝑛𝑘))}
.
𝑛1,𝑛2,…,𝑛𝑘∈ 𝑁
тобто – як об’єднання множин станів для всіх можливих кількостей екземплярів 𝑃𝑖 , 𝑖 ∈ {1, … , 𝑘}, тобто всіх
комбінацій натуральних степенів множин міток iM та даних D.
Семантика базових функцій та композицій спадкується з [1] без змін, причому кожне перетворення
залишає стан в тій же компоненті об’єднання (стосовно набору 𝑛1, 𝑛2, … , 𝑛𝑘 ∈ 𝑁).
В модифікованій моделі зручно задавати семантику нових двох операцій. Так, розмічена операція
[𝑚𝑏] 𝑖𝑑: = 𝑠𝑡𝑎𝑟𝑡(𝑃𝑥) [𝑚𝑎], виконана у підпрограмі 𝑃𝑖𝑗 , перетворює стан S у наступний (𝑥, 𝑖 ∈ {1, … , 𝑘}, 𝑗 ∈
{1, … , 𝑛𝑖}):
𝑆′ =
(
(
(
𝑚′11
𝑚′12
⋮
𝑚′1𝑛1
) ,… ,(
𝑚′𝑥1
𝑚′𝑥2
⋮
𝑚′𝑥𝑛𝑥+1
) ,… ,(
𝑚′𝑘1
𝑚′𝑘2
⋮
𝑚′𝑘𝑛𝑘
)
)
,
(
𝑑′, (
𝑑′11
𝑑′12
⋮
𝑑′1𝑛1
) ,… ,(
𝑑′𝑥1
𝑑′𝑥2
⋮
𝑑′𝑥𝑛𝑥+1
) ,… ,(
𝑑′𝑘1
𝑑′𝑘2
⋮
𝑑′𝑘𝑛𝑘
)
)
)
,
Паралельне програмування. Розподілені системи і мережі
95
де
𝑚′𝑖𝑗 = 𝑚𝑎, якщо 𝑚𝑖𝑗 = 𝑚𝑏 ,
𝑑′𝑖𝑗 = 𝑑𝑖𝑗∇[𝑖𝑑 ⟼ 𝐼𝑑] і 𝑑′ = 𝑑, якщо id – ім’я в локальному даному dij або ж 𝑑′𝑖𝑗 = 𝑑𝑖𝑗 і 𝑑′ = 𝑑∇[𝑖𝑑 ⟼
𝐼𝑑], якщо id – ім’я в глобальному даному d, Id – значення функції 𝑠𝑡𝑎𝑟𝑡(𝑃𝑥), тобто код щойно породженого
нового процесу 𝑃𝑥𝑛𝑥+1;
𝑚′𝑥𝑛𝑥+1 = 𝑚𝑥[𝑠𝑡𝑎𝑟𝑡] – має значення початкової мітки підпрограми 𝑃𝑥;
𝑑′𝑥𝑛𝑥+1 = ∅ (початкове дане нового екземпляру 𝑃𝑥 – порожнє);
𝑚′𝑦𝑧 = 𝑚𝑦𝑧, 𝑑′𝑦𝑧 = 𝑑𝑦𝑧 для решти компонент стану,
при цьому змінюється розмірність двох векторів у складі стану (стан переходить до іншої компоненти з
об’єднання States) – додається по одній компоненті стану (𝑚′𝑥𝑛𝑥+1) та даного (𝑑′𝑥𝑛𝑥+1) для нового, щойно
створеного та запущеного на виконання, екземпляру 𝑃𝑥.
Семантика розміченої операції приєднання [𝑚𝑏] 𝑗𝑜𝑖𝑛(𝐼𝑑) [𝑚𝑎], виконаної у підпрограмі 𝑃𝑖𝑗 , де Id –
ідентифікатор екземпляру номер q підпрограми 𝑃𝑥 (𝑞 ∈ {1, … , 𝑛𝑥}) – 𝑃𝑥𝑞 , перетворює стан S у наступний
(𝑥, 𝑖 ∈ {1, … , 𝑘}, 𝑗 ∈ {1, … , 𝑛𝑖}):
𝑆′ =
(
(
(
𝑚′11
𝑚′12
⋮
𝑚′1𝑛1
) ,… ,(
𝑚′𝑥1
𝑚′𝑥2
⋮
𝑚′𝑥𝑛𝑥
) ,… ,(
𝑚′𝑘1
𝑚′𝑘2
⋮
𝑚′𝑘𝑛𝑘
)
)
,
(
𝑑′, (
𝑑′11
𝑑′12
⋮
𝑑′1𝑛1
) ,… ,(
𝑑′𝑥1
𝑑′𝑥2
⋮
𝑑′𝑥𝑛𝑥
) ,… ,(
𝑑′𝑘1
𝑑′𝑘2
⋮
𝑑′𝑘𝑛𝑘
)
)
)
,
де
𝑚′𝑖𝑗 = 𝑚𝑎, якщо 𝑚𝑖𝑗 = 𝑚𝑏 та 𝑚𝑥𝑞 = 𝑚𝑥[𝑓𝑖𝑛𝑎𝑙] – фінальна мітка підпрограми 𝑃𝑥 (тобто програма 𝑃𝑥𝑞
завершилась),
𝑚′𝑦𝑧 = 𝑚𝑦𝑧, 𝑑′𝑦𝑧 = 𝑑𝑦𝑧 для всіх решти компонент стану,
інакше – стан не змінюється (якщо наведена щойно умова «𝑃𝑥𝑞 завершилась» не виконується), S' = S – тобто
підпрограма 𝑃𝑖𝑗 не зрушує з місця і буде, фактично, чекати, поки 𝑃𝑥𝑞 завершиться.
Семантика функцій fork, lock, unlock та інших операцій
Також специфікуємо семантику інших важливих та практичних функцій для реального використання
multithreading паралелізму в транзиційній моделі виконання програм IPCL.
Операція fork(), яка створює точну копію поточного процесу (включно з поточним станом пам’яті) та
запускає його на виконання з поточної інструкції, широко застосовується у Unix-подібних операційних
системах для породження паралельних процесів, зокрема у сервісних системах. Функція fork(), як і start(),
породжує новий екземпляр паралельно виконуваної підпрограми, проте запускає її з поточного місця на
поточних даних екземпляра-породжувача. Так, розмічена операція [𝑚𝑏] 𝑖𝑑: = 𝑓𝑜𝑟𝑘() [𝑚𝑎], виконана у
підпрограмі 𝑃𝑖𝑗 , перетворює стан S у наступний (𝑖 ∈ {1, … , 𝑘}, 𝑗 ∈ {1, … , 𝑛𝑖}):
𝑆′ =
(
(
(
𝑚′11
𝑚′12
⋮
𝑚′1𝑛1
) ,… ,(
𝑚′𝑖1
𝑚′𝑖2
⋮
𝑚′𝑖𝑛𝑖+1
) ,… ,(
𝑚′𝑘1
𝑚′𝑘2
⋮
𝑚′𝑘𝑛𝑘
)
)
,
(
𝑑′, (
𝑑′11
𝑑′12
⋮
𝑑′1𝑛1
) ,… ,(
𝑑′𝑖1
𝑑′𝑖2
⋮
𝑑′𝑖𝑛𝑖+1
) ,… ,(
𝑑′𝑘1
𝑑′𝑘2
⋮
𝑑′𝑘𝑛𝑘
)
)
)
,
де
𝑚′𝑖𝑗 = 𝑚𝑎, якщо 𝑚𝑖𝑗 = 𝑚𝑏;
𝑑′𝑖𝑗 = 𝑑𝑖𝑗∇[𝑖𝑑 ⟼ 𝐼𝑑] і 𝑑′ = 𝑑, якщо id – ім’я в локальному даному dij або ж 𝑑′𝑖𝑗 = 𝑑𝑖𝑗 і 𝑑′ = 𝑑∇[𝑖𝑑 ⟼
𝐼𝑑], якщо id – ім’я в глобальному даному d, Id – значення функції 𝑠𝑡𝑎𝑟𝑡(𝑃𝑥), тобто код щойно породженого
нового процесу 𝑃𝑖𝑛𝑖+1;
𝑚′𝑖𝑛𝑖+1 = 𝑚𝑎 – має значення мітки підпрограми 𝑃𝑖 після щойно виконаної функції fork() (як і у 𝑃𝑖𝑗);
𝑑′𝑖𝑛𝑖+1 = 𝑑𝑖𝑗∇[𝑖𝑑 ⟼ 0] і 𝑑′ = 𝑑, якщо id – ім’я в локальному даному dij або ж 𝑑′𝑖𝑛𝑖+1 = 𝑑𝑖𝑗 і 𝑑′ =
𝑑∇[𝑖𝑑 ⟼ 0], якщо id – ім’я в глобальному даному d;
𝑚′𝑦𝑧 = 𝑚𝑦𝑧, 𝑑′𝑦𝑧 = 𝑑𝑦𝑧 для решти компонент стану,
Паралельне програмування. Розподілені системи і мережі
96
при цьому змінюється розмірність двох векторів у складі стану (стан переходить до іншої компоненти з
об’єднання States) – додається по одній компоненті стану (𝑚′𝑖𝑛𝑖+1) та даного (𝑑′𝑖𝑛𝑖+1) для нового, щойно
створеного та запущеного на виконання, екземпляру 𝑃𝑖 .
Функції lock() та unlock() дозволяють виконати (захищені) оператор(и) в ексклюзивному режимі (в
режимі ексклюзивного доступу), коли лише одна з програм – паралельних екземплярів-претендентів може їх
виконувати. Такі операції або їх аналоги є основою для реалізації синхронізації, критичних секцій, моніторів та
взаємовиключного доступу (взаємних блокувань) у операційних системах при управління доступом до
ресурсів.
Розмічена функція [𝑚𝑏] 𝑙𝑜𝑐𝑘(𝑟𝑒𝑠); [𝑚𝑎], виконана у підпрограмі 𝑃𝑖𝑗 , перетворює стан S у наступний
(𝑖 ∈ {1, … , 𝑘}, 𝑗 ∈ {1, … , 𝑛𝑖}):
𝑆′ =
(
(
(
𝑚′11
𝑚′12
⋮
𝑚′1𝑛1
) ,… ,(
𝑚′𝑖1
𝑚′𝑖2
⋮
𝑚′𝑖𝑛𝑖
) ,… ,(
𝑚′𝑘1
𝑚′𝑘2
⋮
𝑚′𝑘𝑛𝑘
)
)
,
(
𝑑′, (
𝑑′11
𝑑′12
⋮
𝑑′1𝑛1
) ,… ,(
𝑑′𝑖1
𝑑′𝑖2
⋮
𝑑′𝑖𝑛𝑖
) ,… ,(
𝑑′𝑘1
𝑑′𝑘2
⋮
𝑑′𝑘𝑛𝑘
)
)
)
,
де
𝑚′𝑖𝑗 = 𝑚𝑎, якщо 𝑚𝑖𝑗 = 𝑚𝑏 та 𝑟𝑒𝑠 ⟹ (𝑑) = 0 (тобто ресурс, асоційований з res, був вільний – значення
змінної з іменем res у глобальному даному дорівнює 0);
𝑑′ = 𝑑∇[𝑟𝑒𝑠 ⟼ 1], тобто ресурс, асоційований з res, тепер «зайнятий», причому важливо гарантувати,
що res – іменує «системну змінну», тобто ніхто інший не може змінювати її значення (ніякі інші функції та
оператори, окрім функцій lock та unlock);
𝑚′𝑦𝑧 = 𝑚𝑦𝑧, 𝑑′𝑦𝑧 = 𝑑𝑦𝑧 для решти компонент стану,
інакше (якщо 𝑟𝑒𝑠 ⟹ (𝑑) ≠ 0, тобто ресурс, асоційований з res, не був вільний) – стан не змінюється, S' = S,
тобто підпрограма 𝑃𝑖𝑗 не зрушує з місця і буде, фактично, чекати, поки відповідний ресурс звільниться (𝑟𝑒𝑠 ⟹
(𝑑) стане рівним 0).
Функцією lock() зазвичай відкривається робота з критичною секцією (критичним ресурсом). У кінці
критичної секції має іти виклик функції unlock(), що вказує на її завершення та звільнення критичного ресурсу.
Так, розмічена функція [𝑚𝑏] 𝑢𝑛𝑙𝑜𝑐𝑘(𝑟𝑒𝑠); [𝑚𝑎], виконана у підпрограмі 𝑃𝑖𝑗 , перетворює стан S у
наступний (𝑖 ∈ {1, … , 𝑘}, 𝑗 ∈ {1, … , 𝑛𝑖}):
𝑆′ =
(
(
(
𝑚′11
𝑚′12
⋮
𝑚′1𝑛1
) ,… ,(
𝑚′𝑖1
𝑚′𝑖2
⋮
𝑚′𝑖𝑛𝑖
) ,… ,(
𝑚′𝑘1
𝑚′𝑘2
⋮
𝑚′𝑘𝑛𝑘
)
)
,
(
𝑑′, (
𝑑′11
𝑑′12
⋮
𝑑′1𝑛1
) ,… ,(
𝑑′𝑖1
𝑑′𝑖2
⋮
𝑑′𝑖𝑛𝑖
) ,… ,(
𝑑′𝑘1
𝑑′𝑘2
⋮
𝑑′𝑘𝑛𝑘
)
)
)
,
де
𝑚′𝑖𝑗 = 𝑚𝑎, якщо 𝑚𝑖𝑗 = 𝑚𝑏;
𝑑′ = 𝑑∇[𝑟𝑒𝑠 ⟼ 0], тобто ресурс, асоційований з res, тепер «вільний», причому важливо гарантувати,
що res – іменує «системну змінну», тобто ніхто інший не може змінювати її значення (ніякі інші функції та
оператори, окрім функцій lock та unlock);
𝑚′𝑦𝑧 = 𝑚𝑦𝑧, 𝑑′𝑦𝑧 = 𝑑𝑦𝑧 для решти компонент стану.
Аналогічно можна задати семантику вбудованих атомарних операцій процесорів test_and_set(a, b),
swap(a, b) роботу з семафорами (зокрема, функції Дейкстри P(semaphore) і V(semaphore), або wait(semaphore) і
signal(semaphore) відповідно) та інших, що є основою атомарного виконання і механізмів синхронізації та
управління доступом в операційних системах – зокрема, enter_critical_section(section_id) та
exit_critical_section(section_id), монітори тощо.
Еквівалентність двох систем
Тепер – про взаємну звідність. Ми розглядаємо лише продуктивні програми, тобто такі, що
завершуються і повертають дане, яке містить результат їх роботи (обчислень). Тобто, розглядаємо паралельні
програми з функціональної точки зору. Програми, що «зациклюються», тобто не завершуються, не являють
собою суттєвого інтересу не тільки в контексті даної роботи, але і в цілому, у більш широкому контексті, адже,
по суті, вони є помилковими (бо не повертають ніякого результату над вхідними даними).
Паралельне програмування. Розподілені системи і мережі
97
Теорема 1. Дві семантичні моделі виконання – IPCL 𝑃1
𝑛1|| 𝑃2
𝑛2|| … ||𝑃𝑘
𝑛𝑘 (з фіксованими степенями
паралельних програм, див. [1]) та модель з динамічним породженням паралельних підпрограм start / join
(специфікована вище) – еквівалентні за обчислювальною потужністю. Тобто, ці дві сукупності програм в
IPCL (розширеному start / join) – взаємно-виразні для довільної «продуктивної» програми (тієї, що
зупиняється).
Обґрунтування. Виразність моделі з фіксованими степенями (𝑃1
𝑛1|| 𝑃2
𝑛2|| … ||𝑃𝑘
𝑛𝑘) у моделі зі start / join
– очевидна – на початку, в «основному потоці», треба породити потрібну кількість екземплярів кожної з
підпрограм 𝑃1…𝑃𝑘 за допомогою start, і одразу ж «приєднати» їх всі, у довільній послідовності, за
допомогою join. В зворотному напрямку – покажемо від супротивного. Припустимо, є деяка програма, яка
задана у розширеному start / join IPCL, яка не має еквівалента (не може бути подана) у моделі з фіксованими
степенями виконання (𝑃1
𝑛1|| 𝑃2
𝑛2|| … ||𝑃𝑘
𝑛𝑘). Тоді можливі два варіанти. Якщо програма у розширеній моделі не
зупиняється («зациклюється», наприклад, нескінченно породжує нові процеси за допомогою start) – то вона
не є продуктивною, отже не підпадає під теорему і не цікавить нас взагалі (саме з причини
непродуктивності). Якщо ж програма зупиняється, то нехай вона це робить за N кроків. Тоді цю поведінку
можна виразити «напряму» у моделі 𝑃1
𝑁|| 𝑃2
𝑁|| … ||𝑃𝑘
𝑁, але така програма у IPCL буде мати і багато інших трас
виконання. Аби написати програму, яка точно відтворюватиме поведінку, потрібно ввести в глобальне дане
змінні (зі значеннями: 0 «не стартувала», 1 «виконується» та 2 «завершилась») за кількістю реально
породжених програм (точніше – модель двовимірного масиву run у номінативних даних з індексами номеру
програми {1,…,k} та номеру екземпляру {1,…,ni}). Тоді:
1) start(.) – збільшує останнє збережене ni на 1 та присвоює run[.][ni] := 1 (тобто дає сигнал «запуску»
відповідному екземпляру паралельної підпрограми);
2) join(.) – переходить до наступної інструкції тільки якщо відповідна підпрограма з кодом Id (значення
аргументу) – завершилась, тобто елемент масиву run, що відповідає її стану, дорівнює 2;
3) самі паралельні підпрограми (всі, окрім «основного потоку», тобто стартової, «точки входу»)
модифікуються таким чином, що на старті (перед кодом самої підпрограми) очікують run[.][.] = 1 (відповідна до
свого номеру екземпляру підпрограми комірка масиву run) у нескінченому циклі
while run[.][.] = 0 do skip;
а при завершенні – встановлюють у ту ж саму комірку run[.][.] = 2 (ознака завершення роботи), на старті ж усі
run[.][.] = 0 (тобто, відповідна підпрограма ще не була запущена).
Ці зміни приводять до точного відтворення роботи (поведінки, можливих трас) програми у розширеній
(start / join) мові IPCL. Так, зокрема, ведеться облік (у т.ч. – кількості) запущених паралельних програм (щоб не
було накладок з нумерацією – ni), вони стартують лише у «дозволені» моменти (run[.][.] = 1) та враховано
специфіку join.
Зауваження. Звісно, розглянуті два класи не є еквівалентними в повному розумінні і не для кожної
програми можна побудувати аналог в іншій системі. Ми розглядаємо лише програми зі скінченими трасами (як
вже було зазначено вище), які завершують своє виконання та повертають деякий результат (результуюче дане
може бути отримане з кінцевого стану ланцюжку переходів – виконання – у транзиційній системі). Так, для
програми
P: id := start(P);
немає аналогу в системі з фіксованими степенями паралельно виконуваних підпрограм, але ж наведена
програма, при цьому, не є продуктивною – її виконання теоретично ніколи не завершується (адже вона постійно
та нескінченно породжує нові екземпляри самої себе), отже вона не повертає дане – результат свого виконання.
Такі програми нас не цікавлять з очевидних причин – їх непродуктивності.
Висновки
В роботі введено модель паралелізму в IPCL з динамічним породженням екземплярів (паралельних)
підпрограм. Для цього визначено семантику нових функцій start та join (породження та приєднання /
очікування завершення / фіналізації) у транзиційній системі з [1–3]. Сформульовано теорему про
еквівалентність (рівнопотужність) двох підходів до побудови програм і, відповідно, двох семантик –
розширеної та базової ([1–3]) транзиційної. Показано, що взаємна виразність можлива у випадках програм, що
завершуються.
Саме обґрунтування не є доведенням у строгому математичному смислі, тож подальші роботи можуть
рафінувати наведені міркування до формального доведення.
Паралельне програмування. Розподілені системи і мережі
98
У цілому, це – важливий результат, адже дозволяє звести роботу у більш складній (за будовою) системі з
динамічним породженням екземплярів до більш простої (для доведень) системи з параметричною кількістю
однакових програм, виконуваних у паралель.
Також треба дослідити, як зміняться доведення [4-7] для моделі виконання з породженням екземплярів
програм у IPCL.
Література
1. Панченко Т.В. Метод доведення властивостей програм в композиційно-номінативних мовах IPCL. Проблеми програмування. 2008.
№ 1. С. 3–16.
2. Панченко Т.В. Методологія доведення властивостей програм в композиційних мовах IPCL. Доповіді Міжнародної конференції
“Теоретичні та прикладні аспекти побудови програмних систем” (TAAPSD’2004). К., 2004. С. 62–67.
3. Панченко Т.В. Композиційні методи специфікації та верифікації програмних систем. Автореферат дисертації на здобуття наук. …
канд. фіз.-мат. наук. К. 2006. 17 с.
4. Іванов Є., Панченко Т.В., Fabunmi Sunmade. Модель паралелізму в IPCL з породженням екземплярів. Праці Міжнар. конф.
“Теоретичні та прикладні аспекти побудови програмних систем” (TAAPSD’2017). Київ. 2017. С. 131–133.
5. Polishchuk N.V., Kartavov M.O. and Panchenko T.V. Safety Property Proof using Correctness Proof Methodology in IPCL. Proceedings of the
5th International Scientific Conference “Theoretical and Applied Aspects of Cybernetics”. Kyiv: Bukrek, 2015. P. 37–44.
6. Kartavov M., Panchenko T., Polishchuk N. Properties Proof Method in IPCL Application To Real-World System Correctness Proof.
International Journal "Information Models and Analyses". Sofia, Bulgaria: ITHEA. 2015. Vol. 4. N 2. P. 142–155.
7. Panchenko T.V. Application of the Method for Concurrent Programs Properties Proof to Real-World Industrial Software Systems. Proceedings
of the 12th International Conference on ICT in Education, Research and Industrial Applications. Integration, Harmonization and Knowledge
Transfer (ICTERI 2016), edited by Vadim Ermolayev et al. Kyiv. 2016. P. 119–128 (CEUR-WS. – Vol. 1614. – ISSN:1613-0073, available
online: http://ceur-ws.org/Vol-1614/).
References
1. PANCHENKO, T. (2008) The Method for Program Properties Proof in Compositional Nominative Languages IPCL [in Ukrainian]. Problems
of Programming. 1. P. 3–16.
2. PANCHENKO, T. (2004) The Methodology for Program Properties Proof in Compositional Languages IPCL [in Ukrainian]. In Proceedings of
the International Conference "Theoretical and Applied Aspects of Program Systems Development" (TAAPSD'2004). Kyiv. P. 62–67.
3. PANCHENKO, T. (2006) Compositional Methods for Software Systems Specification and Verification (PhD Thesis Synopsis) [in Ukrainian].
Kyiv. 17 p.
4. IVANOV, IE., PANCHENKO, T. and FABUNMI, S. (2017) Parallelism Model with Instances Generation in IPCL [in Ukrainian]. In
Proceedings of the International Conference "Theoretical and Applied Aspects of Program Systems Development" (TAAPSD'2017). Kyiv.
P. 131–133.
5. POLISHCHUK, N.V., KARTAVOV, M.O. and PANCHENKO, T.V. (2015) Safety Property Proof using Correctness Proof Methodology in
IPCL. In Proceedings of the 5th International Scientific Conference “Theoretical and Applied Aspects of Cybernetics”, Kyiv, Bukrek, P. 37–44.
6. KARTAVOV, M., PANCHENKO, T. and POLISHCHUK, N. (2015) Properties Proof Method in IPCL Application To Real-World System
Correctness Proof. International Journal "Information Models and Analyses", Sofia, Bulgaria, ITHEA, Vol. 4, N 2, P. 142–155.
7. PANCHENKO, T. (2016) Application of the Method for Concurrent Programs Properties Proof to Real-World Industrial Software Systems. In
Proceedings of the 12th International Conference on ICT in Education, Research and Industrial Applications. Integration, Harmonization and
Knowledge Transfer (ICTERI 2016), edited by Vadim Ermolayev et al., Kyiv, P.119–128 (CEUR-WS. – Vol. 1614, available online:
http://ceur-ws.org/Vol-1614/).
Про авторів:
Тарас Володимирович Панченко,
кандидат фізико-математичних наук, доцент,
доцент кафедри теорії та технології програмування
факультету кібернетики Київського національного університету імені Тараса Шевченка.
Кількість наукових публікацій в українських виданнях – 35.
Кількість наукових публікацій в зарубіжних виданнях – 3.
http://orcid.org/0000-0003-0412-1945,
Sunmade Fabunmi,
аспірант кафедри теорії та технології програмування
факультету комп’ютерних наук та кібернетики
Київського національного університету імені Тараса Шевченка.
Кількість наукових публікацій в українських виданнях – 3.
http://orcid.org/0000-0002-3926-106X.
Місце роботи авторів:
Київський національний університет імені Тараса Шевченка,
03680, Київ, проспект Академіка Глушкова, 4Д.
Тел.: 259 0519.
E-mail: taras.panchenko@gmail.com
|