Еквівалентність двох систем паралельного виконання
Досліджується метод доведення властивостей паралельних програм, що виконуються багатоекземплярно в режимі почергового покрокового переключення і взаємодіють через спільну пам’ять. У роботі розглянуто дві системи паралельного виконання програм та наведено обґрунтування взаємної виразності двох цих пі...
Saved in:
| Published in: | Проблеми програмування |
|---|---|
| Date: | 2018 |
| Main Authors: | , |
| Format: | Article |
| Language: | Ukrainian |
| Published: |
Інститут програмних систем НАН України
2018
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/144587 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Cite this: | Еквівалентність двох систем паралельного виконання / Т.В. Панченко, Fabunmi Sunmade // Проблеми програмування. — 2018. — № 2-3. — С. 93-98. — Бібліогр.: 7 назв. — укр. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1862714596161224704 |
|---|---|
| author | Панченко, Т.В. Fabunmi Sunmade |
| author_facet | Панченко, Т.В. Fabunmi Sunmade |
| citation_txt | Еквівалентність двох систем паралельного виконання / Т.В. Панченко, Fabunmi Sunmade // Проблеми програмування. — 2018. — № 2-3. — С. 93-98. — Бібліогр.: 7 назв. — укр. |
| collection | DSpace DC |
| container_title | Проблеми програмування |
| description | Досліджується метод доведення властивостей паралельних програм, що виконуються багатоекземплярно в режимі почергового покрокового переключення і взаємодіють через спільну пам’ять. У роботі розглянуто дві системи паралельного виконання програм та наведено обґрунтування взаємної виразності двох цих підходів. Один – з фіксованою, але параметричною, кількістю паралельно виконуваних програм. Другий – реалізує модель породження (start) і приєднання після зупинки (join) паралельних програм (також називається multithreading). Введено відповідні дві базові функції та задано їх семантику. Також наведено семантику інших функцій стосовно паралельного виконання, управління ресурсами та синхронізації доступу. Наведено теорему щодо (функціональної) еквівалентності двох систем та її обґрунтування. Програма в даному випадку розглядається як функція над даними. Стверджується, що для довільної програми в одній з систем паралелізму можна побудувати відповідну їй програму в іншій системі, яка повертає той самий результат (тобто є функціонально еквівалентною). Тільки продуктивні програми розглядаються тут у контексті взаємної виразності, оскільки у протилежному випадку вони "зависають" і не повертають жодного результату, отже є за межами нашого розгляду. Отриманий результат дозволяє звести роботу у більш складній (за будовою) системі з динамічним породженням екземплярів до більш простої (для доведень) системи з параметричною кількістю однакових програм, виконуваних у паралель. Визначено також питання для подальших досліджень у цьому напрямку.
Исследуется метод доказательства свойств параллельных программ, которые выполняются многоэкземплярно в режиме поочередного пошагового переключения и взаимодействуют через общую память. В работе рассмотрены две системы параллельного выполнения программ и приведено обоснование взаимной выразимости этих двух подходов. Один – с фиксированным, но параметрическим, количеством параллельно выполняемых программ. Второй – реализует модель порождения (start) и присоединения после остановки (join) параллельных программ (также называется multithreading). Введено соответствующие две базовые функции и задано их семантику. Также задана семантика других функций касательно параллельного выполнения, управления ресурсами и синхронизации доступа. Приведены теорема об (функциональной) эквивалентности двух систем и ее обоснование. Программа в данном случае рассматривается как функция над данными. Утверждается, что для произвольной программы в одной из систем параллелизма можно построить соответствующую ей программу в другой системе, которая возвращает тот же результат (то есть функционально эквивалентна). Только продуктивные программы рассматриваются здесь в контексте взаимной выразимости, поскольку в противном случае они "зависают" и не возвращают никакого результата, поэтому лежат вне области нашего рассмотрения. Полученный результат позволяет свести работу в более сложной (по строению) системе с динамическим порождением экземпляров к более простой (для доказательств) системе с параметрическим количеством одинаковых программ, выполняемых параллельно. Также указаны вопросы для дальнейших исследований в этом направлении.
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.
|
| first_indexed | 2025-12-07T17:52:15Z |
| format | Article |
| fulltext | |
| id | nasplib_isofts_kiev_ua-123456789-144587 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1727-4907 |
| language | Ukrainian |
| last_indexed | 2025-12-07T17:52:15Z |
| publishDate | 2018 |
| publisher | Інститут програмних систем НАН України |
| record_format | dspace |
| spelling | Панченко, Т.В. Fabunmi Sunmade 2018-12-30T16:56:46Z 2018-12-30T16:56:46Z 2018 Еквівалентність двох систем паралельного виконання / Т.В. Панченко, Fabunmi Sunmade // Проблеми програмування. — 2018. — № 2-3. — С. 93-98. — Бібліогр.: 7 назв. — укр. 1727-4907 https://nasplib.isofts.kiev.ua/handle/123456789/144587 004.415, 681.3 Досліджується метод доведення властивостей паралельних програм, що виконуються багатоекземплярно в режимі почергового покрокового переключення і взаємодіють через спільну пам’ять. У роботі розглянуто дві системи паралельного виконання програм та наведено обґрунтування взаємної виразності двох цих підходів. Один – з фіксованою, але параметричною, кількістю паралельно виконуваних програм. Другий – реалізує модель породження (start) і приєднання після зупинки (join) паралельних програм (також називається multithreading). Введено відповідні дві базові функції та задано їх семантику. Також наведено семантику інших функцій стосовно паралельного виконання, управління ресурсами та синхронізації доступу. Наведено теорему щодо (функціональної) еквівалентності двох систем та її обґрунтування. Програма в даному випадку розглядається як функція над даними. Стверджується, що для довільної програми в одній з систем паралелізму можна побудувати відповідну їй програму в іншій системі, яка повертає той самий результат (тобто є функціонально еквівалентною). Тільки продуктивні програми розглядаються тут у контексті взаємної виразності, оскільки у протилежному випадку вони "зависають" і не повертають жодного результату, отже є за межами нашого розгляду. Отриманий результат дозволяє звести роботу у більш складній (за будовою) системі з динамічним породженням екземплярів до більш простої (для доведень) системи з параметричною кількістю однакових програм, виконуваних у паралель. Визначено також питання для подальших досліджень у цьому напрямку. Исследуется метод доказательства свойств параллельных программ, которые выполняются многоэкземплярно в режиме поочередного пошагового переключения и взаимодействуют через общую память. В работе рассмотрены две системы параллельного выполнения программ и приведено обоснование взаимной выразимости этих двух подходов. Один – с фиксированным, но параметрическим, количеством параллельно выполняемых программ. Второй – реализует модель порождения (start) и присоединения после остановки (join) параллельных программ (также называется multithreading). Введено соответствующие две базовые функции и задано их семантику. Также задана семантика других функций касательно параллельного выполнения, управления ресурсами и синхронизации доступа. Приведены теорема об (функциональной) эквивалентности двух систем и ее обоснование. Программа в данном случае рассматривается как функция над данными. Утверждается, что для произвольной программы в одной из систем параллелизма можно построить соответствующую ей программу в другой системе, которая возвращает тот же результат (то есть функционально эквивалентна). Только продуктивные программы рассматриваются здесь в контексте взаимной выразимости, поскольку в противном случае они "зависают" и не возвращают никакого результата, поэтому лежат вне области нашего рассмотрения. Полученный результат позволяет свести работу в более сложной (по строению) системе с динамическим порождением экземпляров к более простой (для доказательств) системе с параметрическим количеством одинаковых программ, выполняемых параллельно. Также указаны вопросы для дальнейших исследований в этом направлении. 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. uk Інститут програмних систем НАН України Проблеми програмування Паралельне програмування. Розподілені системи і мережі Еквівалентність двох систем паралельного виконання Equivalence of two parallel execution systems Article published earlier |
| spellingShingle | Еквівалентність двох систем паралельного виконання Панченко, Т.В. Fabunmi Sunmade Паралельне програмування. Розподілені системи і мережі |
| title | Еквівалентність двох систем паралельного виконання |
| title_alt | Equivalence of two parallel execution systems |
| title_full | Еквівалентність двох систем паралельного виконання |
| title_fullStr | Еквівалентність двох систем паралельного виконання |
| title_full_unstemmed | Еквівалентність двох систем паралельного виконання |
| title_short | Еквівалентність двох систем паралельного виконання |
| title_sort | еквівалентність двох систем паралельного виконання |
| topic | Паралельне програмування. Розподілені системи і мережі |
| topic_facet | Паралельне програмування. Розподілені системи і мережі |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/144587 |
| work_keys_str_mv | AT pančenkotv ekvívalentnístʹdvohsistemparalelʹnogovikonannâ AT fabunmisunmade ekvívalentnístʹdvohsistemparalelʹnogovikonannâ AT pančenkotv equivalenceoftwoparallelexecutionsystems AT fabunmisunmade equivalenceoftwoparallelexecutionsystems |