ISSN 1818-1015 · EISSN 2313-5417

· Язык: ru

Статья: Моделирование примитивов синхронизации параллельных программ (2025)

Читать

Читать онлайн

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

Ключевые фразы: верификация, ПАРАЛЛЕЛЬНАЯ ПРОГРАММА, СЕТИ ПЕТРИ, примитивы синхронизации

Автор (ы): Крюков Олег Сергеевич, Волошко Анна Геннадьевна, Ивутин Алексей Николаевич

Журнал: МОДЕЛИРОВАНИЕ И АНАЛИЗ ИНФОРМАЦИОННЫХ СИСТЕМ

Предпросмотр статьи

Идентификаторы и классификаторы

SCI: Математика
УДК: 519.876.5. Цифровое имитирование и моделирование систем

Для цитирования:

КРЮКОВ О. С., ВОЛОШКО А. Г., ИВУТИН А. Н. МОДЕЛИРОВАНИЕ ПРИМИТИВОВ СИНХРОНИЗАЦИИ ПАРАЛЛЕЛЬНЫХ ПРОГРАММ // МОДЕЛИРОВАНИЕ И АНАЛИЗ ИНФОРМАЦИОННЫХ СИСТЕМ. 2025. Т. 32, № 2

Текстовый фрагмент статьи

Моя история просмотров (2)

01. Статья: Кусочно-постоянные режимы работы полносвязных сетей и их предельных интегро-дифференциальных систем

02. Книга: Очерки из истории раннего капитализма в Италии

Список литературы

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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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.

Выпуск

Т. 32, № 2 (2025)

Кол-во страниц: 130 страниц

Другие статьи выпуска

Кусочно-постоянные режимы работы полносвязных сетей и их предельных интегро-дифференциальных систем (2025)

Авторы: Глызин Сергей Дмитриевич, Кащенко Сергей Александрович

Рассматриваются полносвязные сети осцилляторов и их предельные системы интегро-дифференциальных уравнений с периодическими краевыми условиями. Предполагается, что связь слабая, то есть мал коэффициент при интегральном члене. В задаче об устойчивости нулевого состояния равновесия выделяются простейшие критические случаи потери устойчивости. В этих ситуациях строятся квазинормальные формы, представляющие собой интегро-дифференциальные уравнения, для которых аналитически определяются несколько континуальных семейств кусочно-постоянных двухступенчатых решений. Исследуется устойчивость этих решений. Показано существование кусочно-постоянных решений, имеющих более одной точки разрыва. Выполнен численный эксперимент, иллюстрирующий аналитические построения.

Сохранить в закладках

Обнаружение прямоугольных импульсных помех на вихретоковых дефектограммах рельсов (2025)

Авторы: Быстров Леонид Юрьевич, Гладков Артемий Николаевич, Кузьмин Егор Владимирович

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

Сохранить в закладках

Точный алгоритм для задачи о минимальном полном остовном дереве в делимом кратном графе (2025)

Авторы: Смирнов Александр Валерьевич

В статье рассматриваются неориентированные кратные графы произвольной натуральной кратности k > 1. Кратный граф содержит ребра трех типов: обычные, кратные и мультиребра. Ребра последних двух типов представляют собой объединение k связанных ребер, которые соединяют 2 или вершину соответственно. Связанные ребра могут использоваться только согласованно. Делимые графы представляют собой специальный класс кратных графов. Их основная особенность состоит в возможности разделить граф на k частей, которые будут согласованы на связанных ребрах и не будут иметь общих ребер. Каждая часть является обычным графом. Кратное дерево представляет собой кратный граф без кратных циклов. Количество ребер может быть разным для кратных деревьев с одинаковым количеством вершин. Также можно рассмотреть остовные деревья в кратном графе. Остовное дерево является полным, если кратный путь, соединяющий любые две выбранные вершины, существует в дереве тогда и только тогда, когда такой путь существует в исходном графе. Задача о минимальном полном остовном дереве в кратном графе NP-трудна даже в случае делимого графа. В данной статье мы получим точный алгоритм для задачи о минимальном полном остовном дереве в делимом кратном графе. Также мы определим подкласс делимых графов, для которых алгоритм будет выполняться за полиномиальное время.

Сохранить в закладках

Алгоритм шаблонизации для динамической задачи упаковки в контейнеры с группами размещения (2025)

Авторы: Бражников Евгений Александрович, Панин Артём Александрович, Ратушный Алексей Владленович

Рассматривается NP-трудная задача динамического распределения виртуальных машин по серверам с группами размещения. Для каждой виртуальной машины известны такие параметры, как необходимое количество ресурсов и временные метки создания и удаления. Каждый сервер представляет собой композицию NUMA-узлов и размещается в некоторой стойке. Рассматриваются большие виртуальные машины, размещаемые на два узла одного сервера, и маленькие, что накладывает дополнительные условия для их размещения. Группы размещения представляют собой объединения подмножеств виртуальных машин с условиями конфликта между подмножествами. Задача состоит в том, чтобы упаковать все виртуальные машины с использованием минимального количества стоек серверов в течение рассматриваемого временного горизонта. Для решения данной задачи предлагается эвристика, основанная на методе генерации столбцов. Анализируется набор статических задач в различные моменты времени, необходимых для формирования общего набора шаблонов, используемых при построении верхних оценок. Результаты вычислительных экспериментов на реальных открытых примерах указывают на незначительные расхождения между нижними и верхними границами.

Сохранить в закладках

Об экстремальных элементах и мощности множества непрерывно дифференцируемых выпуклых продолжений булевой функции (2025)

Авторы: Баротов Достонжон Нумонжонович, Баротов Рузибой Нумонжонович

В данной статье изучается существование максимального и минимального элементов множества непрерывно дифференцируемых выпуклых продолжений на произвольной булевой функции и мощность множества непрерывно дифференцируемых выпуклых продолжений на булевой функции. В результате исследования установлено, что мощность множества непрерывно дифференцируемых выпуклых продолжений на произвольной булевой функции равна континууму. Аргументировано, что для любой булевой функции среди её непрерывно дифференцируемых выпуклых продолжений на нет минимального элемента. Доказано, что для любой булевой функции множество её непрерывно дифференцируемых выпуклых продолжений на имеет максимальный элемент лишь тогда, когда количество существенных переменных данной булевой функции меньше 2.

Сохранить в закладках

Издательство

Издательство: ЯрГУ им. П.Г. Демидова
Регион: Россия, Ярославль
Почтовый адрес: 150003, Ярославль, Советская, 14,
Юр. адрес: 150003, Ярославль, Советская, 14,
ФИО: Иванчин Артем Владимирович (Ректор)
E-mail адрес: rectorat@uniyar.ac.ru
Контактный телефон: +7 (485) 2797702
Сайт: https://www.uniyar.ac.ru/

Все права на тексты и товарные знаки принадлежат их законным владельцам. Подробнее...

Сайт https://scinetwork.ru (далее – сайт) работает по принципу агрегатора – собирает и структурирует информацию из публичных источников в сети Интернет, то есть передает полнотекстовую информацию о товарных знаках в том виде, в котором она содержится в открытом доступе.

Сайт и администрация сайта не используют отображаемые на сайте товарные знаки в коммерческих и рекламных целях, не декларируют своего участия в процессе их государственной регистрации, не заявляют о своих исключительных правах на товарные знаки, а также не гарантируют точность, полноту и достоверность информации.

Все права на товарные знаки принадлежат их законным владельцам!

Сайт носит исключительно информационный характер, и предоставляемые им сведения являются открытыми публичными данными.

Администрация сайта не несет ответственность за какие бы то ни было убытки, возникающие в результате доступа и использования сайта.

Спасибо, понятно.

Сказать «Спасибо»

Вы можете поблагодарить автора за публикацию. Ему (ей) будет приятно.

Наведите камеру на QR-код, чтобы открыть моб. версию страницы.