RUS  ENG
Full version
JOURNALS // Proceedings of the Institute for System Programming of the RAS // Archive

Proceedings of ISP RAS, 2025 Volume 37, Issue 6(3), Pages 133–148 (Mi tisp1095)

Bounding thread switches in dynamic analysis of multithreaded programs

V. P. Rudenchika, P. S. Andrianova, V. S. Mutilinab

a Ivannikov Institute for System Programming of the RAS
b Moscow Institute of Physics and Technology (National Research University)

Abstract: For detecting race conditions in multithreaded programs, dynamic analysis methods can be used. Dynamic methods are based on observing program behavior on real program executions. Since analyzing all possible execution paths is generally infeasible (due to the combinatorial explosion of possible thread interleavings), dynamic methods can overlook certain bugs that manifest only within the specific conditions or thread interleavings. This limitation applies, for instance, to the approach implemented in the previous version of RaceHunter tool, which demonstrates the ability to effectively detect race conditions, but may still miss certain cases. To address the combinatorial explosion problem, context bounding analysis can be used. Context bounding is a dynamic analysis technique that limits the number of thread switches in each explored execution path, enabling more scalable exploration. This method is able to detect bugs missed by other techniques with the bound of only two preemptive thread switches. In this work, we present an implementation of context bounding within the RaceHunter tool, which provides a unified framework for describing various dynamic analysis techniques. The evaluation shows that the proposed approach is able to detect race conditions that other methods missed, though at the cost of significantly increased analysis time. As expected, this increase in analysis time is caused by repeated executions. Still, the implementation is an important foundation for future integration with other race detection techniques, specifically with the approach already implemented in the RaceHunter tool.

Keywords: verification, dynamic analysis, context bounding

Language: English

DOI: 10.15514/ISPRAS-2025-37(6)-41



© Steklov Math. Inst. of RAS, 2026