Modeling of parallel program synchronization primitives
https://doi.org/10.18255/1818-1015-2025-2-150-171
Abstract
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.
About the Authors
Oleg S. Kryukov
Tula State Uiversity
Russian Federation
Russian Federation
Anna G. Voloshko
Tula State Uiversity
Russian Federation
Russian Federation
Alexey N. Ivutin
Tula State Uiversity
Russian Federation
Russian Federation
References
1. 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.
2. 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.
3. A. Krizhevsky, “One weird trick for parallelizing convolutional neural networks.” 2014.
4. 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.
5. 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.
6. 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.
7. 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.
8. 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.
9. 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.
10. 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.
11. 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.
12. 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.
13. 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.
14. 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.
15. 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.
16. 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.
17. 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.
18. 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.
19. 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.
20. E. M. Clarke, T. A. Henzinger, H. Veith, R. Bloem, and others, Handbook of Model Checking, vol. 10. Springer Cham, 2018.
21. J. Barnat et al., “Parallel model checking algorithms for linear-time temporal logic,” in Handbook of Parallel Constraint Reasoning, Springer, 2018, pp. 457–507.
22. 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.
23. 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.
24. 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.
25. 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.
26. 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.
27. 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.
28. 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.
29. I. Lomazova, Nested Petri nets: Modeling and analysis of distributedsystems with object structure. Moscow: Scientific World, 2003.
30. 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.
31. 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.
Review
For citations:
Kryukov O.S., Voloshko A.G., Ivutin A.N. Modeling of parallel program synchronization primitives. Modeling and Analysis of Information Systems. 2025;32(2):150-171. (In Russ.) https://doi.org/10.18255/1818-1015-2025-2-150-171
Views:
37
Email this article 