maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2025-2-150-171mais-1938Research ArticleTheory of ComputingМоделирование примитивов синхронизации параллельных программModeling of parallel program synchronization primitiveshttps://orcid.org/0000-0003-3155-6266КрюковОлег СергеевичKryukovOleg S.ol_kryukov97@mail.ruhttps://orcid.org/0000-0002-4304-2513ВолошкоАнна ГеннадьевнаVoloshkoAnna G.atroshina@mail.ruhttps://orcid.org/0000-0003-2970-2148ИвутинАлексей НиколаевичIvutinAlexey N.alexey.ivutin@gmail.comТульский государственный университетРоссияTula State UiversityRussian Federation202528062025322150171Copyright © Крюков О.С., Волошко А.Г., Ивутин А.Н., 20252025Крюков О.С., Волошко А.Г., Ивутин А.Н.Kryukov O.S., Voloshko A.G., Ivutin A.N.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1938

Данная статья посвящена проблеме верификации параллельных программ, которые могут содержать особые виды ошибок, связанных с синхронизацией параллельно исполняемых потоков и доступом к общей памяти. К таким ошибкам относятся тупики и гонки данных. Существует разделение методов верификации параллельных программ на статические и динамические. Последние требуют запуска кода и позволяют проверить на гонки лишь текущую реализацию программы, что при наличии большого числа ветвлений может привести к пропуску гонок. Среди статических методов наибольшее применение нашли аналитические методы (например, на основе дедуктивного анализа) и методы проверки моделей. Однако они сложны в реализации, а последние по-прежнему требуют от программиста значительного объёма ручной работы для построения модели. В этой связи необходимо использование моделей, которые могут быть построены автоматически. Ранее авторами была разработана модель на основе расширения сетей Петри, позволяющая автоматическое построение на основе последовательного кода и преобразование её в параллельный код. Автоматическое построение модели параллельной программы вводит новые, ранее не использовавшиеся требования, связанные со взаимодействием параллельных потоков. Таким образом, в данной статье рассматриваются особенности моделирования с использованием расширенных сетей Петри с семантическими связями основных примитивов синхронизации, реализуемых в большинстве языков и технологий параллельного программирования для систем с общей памятью. В дальнейшем на основе этих моделей будет проводится поиск гонок данных и тупиков для параллельных программ.

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.

верификацияпараллельная программасети Петрипримитивы синхронизацииverificationparallel programPetri netssynchronization primitivesReferencesK. N. Zainidinov and Z. A. Karshiev, “Features of Parallel Execution of Data Mining Algorithms,” Automatics and Software Enginery, vol. 31, no. 1, pp. 83–91, 2020.K. N. Zainidinov and Z. A. Karshiev, “Features of Parallel Execution of Data Mining Algorithms,” Automatics and Software Enginery, vol. 31, no. 1, pp. 83–91, 2020.C. Atilgan, B. T. Tezel, and E. Nasiboglu, “Efficient implementation and parallelization of fuzzy density based clustering,” Information Sciences, vol. 575, pp. 454–467, 2021, doi: 10.1016/j.ins.2021.06.044.C. Atilgan, B. T. Tezel, and E. Nasiboglu, “Efficient implementation and parallelization of fuzzy density based clustering,” Information Sciences, vol. 575, pp. 454–467, 2021, doi: 10.1016/j.ins.2021.06.044.A. Krizhevsky, “One weird trick for parallelizing convolutional neural networks.” 2014.A. Krizhevsky, “One weird trick for parallelizing convolutional neural networks.” 2014.B. Blum and G. Gibson, “Stateless model checking with data-race preemption points,” in Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2016, pp. 477–493, doi: 10.1145/2983990.2984036.B. Blum and G. Gibson, “Stateless model checking with data-race preemption points,” in Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2016, pp. 477–493, doi: 10.1145/2983990.2984036.A. N. Ivutin, A. G. Voloshko, and V. N. Izotov, “Approach to Data Race Detection Based on Petri Nets with Additional Semantic Relations,” in Proceedings of the 2020 ELEKTRO, 2020, pp. 1–5, doi: 10.1109/ELEKTRO49696.2020.9130252.A. N. Ivutin, A. G. Voloshko, and V. N. Izotov, “Approach to Data Race Detection Based on Petri Nets with Additional Semantic Relations,” in Proceedings of the 2020 ELEKTRO, 2020, pp. 1–5, doi: 10.1109/ELEKTRO49696.2020.9130252.A. N. Ivutin, A. G. Troshina, and D. O. Yesikov, “Parallelization of algorithms with use the semantic Petri-Markov nets,” Vestnik of Ryazan State Radio Engineering University, vol. 58, no. 4, pp. 49–56, 2016, doi: 10.21667/1995-4565-2016-58-4-49-56.A. N. Ivutin, A. G. Troshina, and D. O. Yesikov, “Parallelization of algorithms with use the semantic Petri-Markov nets,” Vestnik of Ryazan State Radio Engineering University, vol. 58, no. 4, pp. 49–56, 2016, doi: 10.21667/1995-4565-2016-58-4-49-56.A. V. Soloviev and D. A. Sedov, “Algorithms of detecting errors in parallel programs for distributed memory systems,” in Proceedings of the Instittute for Systems Analysis Russian Academy of Sciences (ISA RAS), 2013, vol. 63, no. 4, pp. 9–15.A. V. Soloviev and D. A. Sedov, “Algorithms of detecting errors in parallel programs for distributed memory systems,” in Proceedings of the Instittute for Systems Analysis Russian Academy of Sciences (ISA RAS), 2013, vol. 63, no. 4, pp. 9–15.S. Abbaspour Asadollah, D. Sundmark, S. Eldh, and H. Hansson, “Concurrency bugs in open source software: a case study,” Journal of Internet Services and Applications, vol. 8, no. 1, pp. 4–19, 2017, doi: 10.1186/s13174-017-0055-2.S. Abbaspour Asadollah, D. Sundmark, S. Eldh, and H. Hansson, “Concurrency bugs in open source software: a case study,” Journal of Internet Services and Applications, vol. 8, no. 1, pp. 4–19, 2017, doi: 10.1186/s13174-017-0055-2.I. Tamas, I. Salomie, and M. Antal, “Atomic invariants verification and deadlock detection at compile-time,” in Proceedings of the IEEE 14th International Conference on Intelligent Computer Communication and Processing (ICCP), 2018, pp. 435–441.I. Tamas, I. Salomie, and M. Antal, “Atomic invariants verification and deadlock detection at compile-time,” in Proceedings of the IEEE 14th International Conference on Intelligent Computer Communication and Processing (ICCP), 2018, pp. 435–441.Y. Cai, C. Ye, Q. Shi, and C. Zhang, “Peahen: fast and precise static deadlock detection via context reduction,” in Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2022, pp. 784–796, doi: 10.1145/3540250.3549110.Y. Cai, C. Ye, Q. Shi, and C. Zhang, “Peahen: fast and precise static deadlock detection via context reduction,” in Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2022, pp. 784–796, doi: 10.1145/3540250.3549110.M. Ronsse and K. De Bosschere, “RecPlay: a fully integrated practical record/replay system,” ACM Transactions on Computer Systems, vol. 17, no. 2, pp. 133–152, 1999, doi: 10.1145/312203.312214.M. Ronsse and K. De Bosschere, “RecPlay: a fully integrated practical record/replay system,” ACM Transactions on Computer Systems, vol. 17, no. 2, pp. 133–152, 1999, doi: 10.1145/312203.312214.C. Flanagan and S. N. Freund, “FastTrack: efficient and precise dynamic race detection,” in Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2009, pp. 121–133, doi: 10.1145/1542476.1542490.C. Flanagan and S. N. Freund, “FastTrack: efficient and precise dynamic race detection,” in Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2009, pp. 121–133, doi: 10.1145/1542476.1542490.E. Pozniansky and A. Schuster, “Efficient on-the-fly data race detection in multithreaded C++ programs,” in Proceedings of the Ninth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2003, pp. 179–190, doi: 10.1145/781498.781529.E. Pozniansky and A. Schuster, “Efficient on-the-fly data race detection in multithreaded C++ programs,” in Proceedings of the Ninth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2003, pp. 179–190, doi: 10.1145/781498.781529.K. Serebryany and T. Iskhodzhanov, “ThreadSanitizer: data race detection in practice,” in Proceedings of the Workshop on Binary Instrumentation and Applications, 2009, pp. 62–71, doi: 10.1145/1791194.1791203.K. Serebryany and T. Iskhodzhanov, “ThreadSanitizer: data race detection in practice,” in Proceedings of the Workshop on Binary Instrumentation and Applications, 2009, pp. 62–71, doi: 10.1145/1791194.1791203.S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson, “Eraser: a dynamic data race detector for multithreaded programs,” ACM Transactions on Computer Systems, vol. 15, no. 4, pp. 391–411, 1997, doi: 10.1145/265924.265927.S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson, “Eraser: a dynamic data race detector for multithreaded programs,” ACM Transactions on Computer Systems, vol. 15, no. 4, pp. 391–411, 1997, doi: 10.1145/265924.265927.X. Xie and J. Xue, “Acculock: Accurate and efficient detection of data races,” in Proceedings of the International Symposium on Code Generation and Optimization, 2011, pp. 201–212, doi: 10.1109/CGO.2011.5764688.X. Xie and J. Xue, “Acculock: Accurate and efficient detection of data races,” in Proceedings of the International Symposium on Code Generation and Optimization, 2011, pp. 201–212, doi: 10.1109/CGO.2011.5764688.M. Yu and D.-H. Bae, “SimpleLock+: Fast and Accurate Hybrid Data Race Detection,” The Computer Journal, vol. 59, no. 6, pp. 793–809, 2016, doi: 10.1093/comjnl/bxu119.M. Yu and D.-H. Bae, “SimpleLock+: Fast and Accurate Hybrid Data Race Detection,” The Computer Journal, vol. 59, no. 6, pp. 793–809, 2016, doi: 10.1093/comjnl/bxu119.A. I. Legalov, V. S. Vasilyev, I. V. Matkovskii, and M. S. Ushakova, “Support tools for creation and transformation of functional-dataflow parallel programs,” Proceedings of the Institute for System Programming of the RAS, vol. 29, no. 5, pp. 165–184, 2017, doi: 10.15514/ISPRAS-2017-29(5)-10.A. I. Legalov, V. S. Vasilyev, I. V. Matkovskii, and M. S. Ushakova, “Support tools for creation and transformation of functional-dataflow parallel programs,” Proceedings of the Institute for System Programming of the RAS, vol. 29, no. 5, pp. 165–184, 2017, doi: 10.15514/ISPRAS-2017-29(5)-10.V. A. Tikhomirov, S. G. Timofeev, and E. A. Moshkova, “Modified model checking verification method,” Bulletin of Russian Academy of Natural Sciences, no. 3, pp. 118–121, 2018.V. A. Tikhomirov, S. G. Timofeev, and E. A. Moshkova, “Modified model checking verification method,” Bulletin of Russian Academy of Natural Sciences, no. 3, pp. 118–121, 2018.E. M. Clarke, T. A. Henzinger, H. Veith, R. Bloem, and others, Handbook of Model Checking, vol. 10. Springer Cham, 2018.E. M. Clarke, T. A. Henzinger, H. Veith, R. Bloem, and others, Handbook of Model Checking, vol. 10. Springer Cham, 2018.J. Barnat et al., “Parallel model checking algorithms for linear-time temporal logic,” in Handbook of Parallel Constraint Reasoning, Springer, 2018, pp. 457–507.J. Barnat et al., “Parallel model checking algorithms for linear-time temporal logic,” in Handbook of Parallel Constraint Reasoning, Springer, 2018, pp. 457–507.H. Boucheneb, G. Gardey, and O. H. Roux, “TCTL Model Checking of Time Petri Nets,” Journal of Logic and Computation, vol. 19, no. 6, pp. 1509–1540, 2009, doi: 10.1093/logcom/exp036.H. Boucheneb, G. Gardey, and O. H. Roux, “TCTL Model Checking of Time Petri Nets,” Journal of Logic and Computation, vol. 19, no. 6, pp. 1509–1540, 2009, doi: 10.1093/logcom/exp036.K. M. Kavi, A. Moshtaghi, and D.-jyi Chen, “Modeling Multithreaded Applications Using Petri Nets,” International Journal of Parallel Programming, vol. 30, pp. 353–371, 2002, doi: 10.1023/A:1019917329895.K. M. Kavi, A. Moshtaghi, and D.-jyi Chen, “Modeling Multithreaded Applications Using Petri Nets,” International Journal of Parallel Programming, vol. 30, pp. 353–371, 2002, doi: 10.1023/A:1019917329895.G. Liu, M. Zhou, and C. Jiang, “Petri Net Models and Collaborativeness for Parallel Processes with Resource Sharing and Message Passing,” ACM Transactions on Embedded Computing Systems, vol. 16, no. 4, pp. 1–20, 2017, doi: 10.1145/2810001.G. Liu, M. Zhou, and C. Jiang, “Petri Net Models and Collaborativeness for Parallel Processes with Resource Sharing and Message Passing,” ACM Transactions on Embedded Computing Systems, vol. 16, no. 4, pp. 1–20, 2017, doi: 10.1145/2810001.S. Bandyopadhyay, D. Sarkar, and C. Mandal, “Equivalence checking of Petri net models of programs using static and dynamic cut-points,” Acta Informatica, vol. 56, pp. 321–383, 2019, doi: 10.1007/s00236-018-0320-2.S. Bandyopadhyay, D. Sarkar, and C. Mandal, “Equivalence checking of Petri net models of programs using static and dynamic cut-points,” Acta Informatica, vol. 56, pp. 321–383, 2019, doi: 10.1007/s00236-018-0320-2.A. Albaghajati and M. Ahmed, “CPN.Net: An Automated Colored Petri Nets Model Extraction From .Net Based Source Code,” in Proceedings of the 1st International Conference on Artificial Intelligence and Data Analytics (CAIDA), 2021, pp. 245–250, doi: 10.1109/CAIDA51941.2021.9425201.A. Albaghajati and M. Ahmed, “CPN.Net: An Automated Colored Petri Nets Model Extraction From .Net Based Source Code,” in Proceedings of the 1st International Conference on Artificial Intelligence and Data Analytics (CAIDA), 2021, pp. 245–250, doi: 10.1109/CAIDA51941.2021.9425201.M. Westergaard, “Verifying Parallel Algorithms and Programs Using Coloured Petri Nets,” in Transactions on Petri Nets and Other Models of Concurrency VI, Springer Berlin Heidelberg, 2012, pp. 146–168.M. Westergaard, “Verifying Parallel Algorithms and Programs Using Coloured Petri Nets,” in Transactions on Petri Nets and Other Models of Concurrency VI, Springer Berlin Heidelberg, 2012, pp. 146–168.O. S. Kryukov, A. G. Voloshko, and A. N. Ivutin, “Automation of the formation of the maximum parallelism in the process,” Izvestiya Tul'skogo gosudarstvennogo universiteta. Tekhnicheskiye nauki, vol. 10, pp. 230–237, 2022.O. S. Kryukov, A. G. Voloshko, and A. N. Ivutin, “Automation of the formation of the maximum parallelism in the process,” Izvestiya Tul'skogo gosudarstvennogo universiteta. Tekhnicheskiye nauki, vol. 10, pp. 230–237, 2022.I. Lomazova, Nested Petri nets: Modeling and analysis of distributedsystems with object structure. Moscow: Scientific World, 2003.I. Lomazova, Nested Petri nets: Modeling and analysis of distributedsystems with object structure. Moscow: Scientific World, 2003.P. de C. Gomes, D. Gurov, M. Huisman, and C. Artho, “Specification and verification of synchronization with condition variables,” Science of Computer Programming, vol. 163, pp. 174–189, 2018, doi: 10.1016/j.scico.2018.05.001.P. de C. Gomes, D. Gurov, M. Huisman, and C. Artho, “Specification and verification of synchronization with condition variables,” Science of Computer Programming, vol. 163, pp. 174–189, 2018, doi: 10.1016/j.scico.2018.05.001.O. S. Kryukov, A. G. Voloshko, and A. N. Ivutin, “Method for automatically building a parallel program model in Go language,” Izvestiya Tul'skogo gosudarstvennogo universiteta. Tekhnicheskiye nauki, vol. 2, pp. 420–433, 2025.O. S. Kryukov, A. G. Voloshko, and A. N. Ivutin, “Method for automatically building a parallel program model in Go language,” Izvestiya Tul'skogo gosudarstvennogo universiteta. Tekhnicheskiye nauki, vol. 2, pp. 420–433, 2025.

The authors declare that there are no conflicts of interest present.