Ограничение количества переключений потоков при динамическом анализе многопоточных программ
https://doi.org/10.15514/ISPRAS-2025-37(6)-41
Аннотация
Для обнаружения состояний гонки в многопоточных программах могут использоваться методы динамического анализа. Динамические методы основаны на наблюдении за поведением программы при её реальном выполнении. Так как анализ всех возможных путей выполнения в общем случае неосуществим (из-за комбинаторного взрыва числа возможных чередований потоков), динамические методы могут упускать определённые ошибки, проявляющиеся только при специфических условиях или порядке выполнения потоков. Это ограничение относится, например, к подходу, реализованному в предыдущей версии инструмента RaceHunter, который демонстрирует способность эффективно выявлять состояния гонки, но всё же может пропускать отдельные случаи. Для решения проблемы комбинаторного взрыва может использоваться анализ с ограничением числа переключений потоков (англ. context bounding). Этот метод подразумевает исследование только тех путей выполнения, в которых ограничено число переключений потоков, что позволяет сделать анализ более масштабируемым. Анализ с ограничением числа переключений потоков способен выявлять ошибки, пропускаемые другими методами, при ограничении всего в два принудительных переключения потоков.
В данной работе мы представляем реализацию анализа с ограничением количества переключений потоков в инструменте RaceHunter, который обеспечивает единую платформу для описания различных методов динамического анализа. Оценка показала, что предложенный подход способен выявлять состояния гонки, которые были пропущены другими методами, хотя и ценой значительного увеличения времени анализа. Как и ожидалось, это увеличение времени связано с повторными запусками программы. Тем не менее, реализация представляет собой важную основу для будущей интеграции с другими техниками обнаружения состояний гонки, в частности с подходом, уже реализованным в инструменте RaceHunter.
Об авторах
Вероника Павловна РУДЕНЧИКРоссия
Cтажер-исследователь ИСП РАН. Научные интересы: статический и динамический анализ программ.
Павел Сергеевич АНДРИАНОВ
Россия
Научный сотрудник ИСП РАН, кандидат физико-математических наук. Научные интересы: статическая верификация, параллельные программы.
Вадим Сергеевич МУТИЛИН
Россия
Кандидат физико-математических наук, ведущий научный сотрудник Института системного программирования им. В.П. Иванникова РАН и доцент Московского физико-технического института. Сфера научных интересов: статический и динамический анализ программ.
Список литературы
1. R. H. B. Netzer and B. P. Miller, “What are race conditions? Some issues and formalizations”, LOPLAS, vol. 1, pp. 74–88, 1992.
2. M. Musuvathi and S. Qadeer, “Iterative context bounding for systematic testing of multithreaded programs”, vol. 42, p. 446–455, jun 2007.
3. M. Musuvathi, S. Qadeer, and T. Ball, “Chess: A systematic testing tool for concurrent software”, Tech. Rep. MSR-TR-2007-149, November 2007.
4. E. A. Gerlits, “Racehunter dynamic data race detector”, Programming and Computer Software, vol. 50, pp. 467–481, Dec 2024.
5. L. Lamport, “Time, clocks, and the ordering of events in a distributed system”, Commun. ACM, vol. 21, p. 558–565, jul 1978.
6. S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson, “Eraser: A dynamic data race detector for multi-threaded programs”, SIGOPS Oper. Syst. Rev., vol. 31, pp. 27–37, Oct. 1997.
7. R. O’Callahan and J.-D. Choi, “Hybrid dynamic data race detection”, inProceedings of the Ninth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP ’03, (New York, NY, USA), p. 167–178, Association for Computing Machinery, 2003.
8. K. Serebryany and T. Iskhodzhanov, “Threadsanitizer – data race detection in practice”, in Proceedings of the Workshop on Binary Instrumentation and Applications, (NYC, NY, U.S.A.), pp. 62–71, 2009.
9. Kernel Concurrency Sanitizer (KCSAN) google.github.io”, https://google.github.io/kernel-sanitizers/KCSAN.html. Accessed 05-05-2025.
10. J. Erickson, M. Musuvathi, S. Burckhardt, and K. Olynyk, “Effective data-race detection for the kernel”, pp. 151–162, jan 2010.
11. T. Elmas, S. Qadeer, and S. Tasiran, “Goldilocks: Efficiently computing the happens-before relation using locksets”, pp. 193–208, 01 2006.
12. https://github.com/mc-imperial/sctbench.git. Accessed 05-05-2025.
13. https://gitee.com/openharmony/arkcompiler_runtime_core.git. Accessed 05-05-2025.
Рецензия
Для цитирования:
РУДЕНЧИК В.П., АНДРИАНОВ П.С., МУТИЛИН В.С. Ограничение количества переключений потоков при динамическом анализе многопоточных программ. Труды Института системного программирования РАН. 2025;37(6):133-148. https://doi.org/10.15514/ISPRAS-2025-37(6)-41
For citation:
RUDENCHIK V.P., ANDRIANOV P.S., MUTILIN V.S. Bounding Thread Switches in Dynamic Analysis of Multithreaded Programs. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2025;37(6):133-148. https://doi.org/10.15514/ISPRAS-2025-37(6)-41






