Modeling of parallel program synchronization primitives
This article is devoted to the problem of verifying parallel programs that may contain special types of errors associated with the synchronization of parallel executed threads and access to shared memory. Such errors include deadlocks and data races. There is a division of parallel program verificat...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2025-06-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/1938 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1849688230546374656 |
|---|---|
| author | Oleg S. Kryukov Anna G. Voloshko Alexey N. Ivutin |
| author_facet | Oleg S. Kryukov Anna G. Voloshko Alexey N. Ivutin |
| author_sort | Oleg S. Kryukov |
| collection | DOAJ |
| description | This article is devoted to the problem of verifying parallel programs that may contain special types of errors associated with the synchronization of parallel executed threads and access to shared memory. Such errors include deadlocks and data races. There is a division of parallel program verification methods into static and dynamic. The second ones require running the code and allow to check only the current implementation of the program for races, which, if there are a large number of branches, can lead to missing races. Among static methods, analytical methods (for example, based on deductive analysis) and model checking methods are most widely used. However, they are difficult to implement, and model checking still require a significant amount of manual work from the programmer to build such a model. In this regard, it is necessary to use models that can be built automatically. Previously, the authors developed a model based on an extension of Petri nets, which allows automatic creation based on sequential code and its conversion into parallel code. Automatic creation of a model of a parallel program introduces new, previously unused requirements related to the interaction of parallel threads. Thus, this article discusses the features of modeling using extended Petri nets with semantic relations of the main synchronization primitives implemented in most languages and parallel programming technologies for shared memory systems. In the future, these models will be used to search for data races and deadlocks in parallel programs. |
| format | Article |
| id | doaj-art-476b53e183cc4cccb2c78126ff79ed1d |
| institution | DOAJ |
| issn | 1818-1015 2313-5417 |
| language | English |
| publishDate | 2025-06-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj-art-476b53e183cc4cccb2c78126ff79ed1d2025-08-20T03:22:04ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172025-06-0132215017110.18255/1818-1015-2025-2-150-1711433Modeling of parallel program synchronization primitivesOleg S. Kryukov0Anna G. Voloshko1Alexey N. Ivutin2Tula State UiversityTula State UiversityTula State UiversityThis article is devoted to the problem of verifying parallel programs that may contain special types of errors associated with the synchronization of parallel executed threads and access to shared memory. Such errors include deadlocks and data races. There is a division of parallel program verification methods into static and dynamic. The second ones require running the code and allow to check only the current implementation of the program for races, which, if there are a large number of branches, can lead to missing races. Among static methods, analytical methods (for example, based on deductive analysis) and model checking methods are most widely used. However, they are difficult to implement, and model checking still require a significant amount of manual work from the programmer to build such a model. In this regard, it is necessary to use models that can be built automatically. Previously, the authors developed a model based on an extension of Petri nets, which allows automatic creation based on sequential code and its conversion into parallel code. Automatic creation of a model of a parallel program introduces new, previously unused requirements related to the interaction of parallel threads. Thus, this article discusses the features of modeling using extended Petri nets with semantic relations of the main synchronization primitives implemented in most languages and parallel programming technologies for shared memory systems. In the future, these models will be used to search for data races and deadlocks in parallel programs.https://www.mais-journal.ru/jour/article/view/1938verificationparallel programpetri netssynchronization primitives |
| spellingShingle | Oleg S. Kryukov Anna G. Voloshko Alexey N. Ivutin Modeling of parallel program synchronization primitives Моделирование и анализ информационных систем verification parallel program petri nets synchronization primitives |
| title | Modeling of parallel program synchronization primitives |
| title_full | Modeling of parallel program synchronization primitives |
| title_fullStr | Modeling of parallel program synchronization primitives |
| title_full_unstemmed | Modeling of parallel program synchronization primitives |
| title_short | Modeling of parallel program synchronization primitives |
| title_sort | modeling of parallel program synchronization primitives |
| topic | verification parallel program petri nets synchronization primitives |
| url | https://www.mais-journal.ru/jour/article/view/1938 |
| work_keys_str_mv | AT olegskryukov modelingofparallelprogramsynchronizationprimitives AT annagvoloshko modelingofparallelprogramsynchronizationprimitives AT alexeynivutin modelingofparallelprogramsynchronizationprimitives |