Моделирование примитивов синхронизации параллельных программ

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

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.