intCV: Automatically Inferring Correlated Variables in Interrrupt-Driven Program

Interrupt-driven programs are extensively employed in safety-critical areas such as aerospace, autonomous driving, and medical equipment. Nevertheless, the uncertainty of interrupt preemption may result in concurrent bugs. Among these concurrent bugs, atomicity violations are critical and challenging to detect. Existing methods mostly concentrate on predicting or detecting single-variable atomicity violations but fail to address the more intricate multi-variable atomicity violations. In real-world programs, many variables are inherently correlated and must be accessed together with their correlated peers consistently. To significantly improve the ability of techniques in inferring correlated variables, this paper conducts an empirical study on real-world software to understand the manifestation characteristics of variable correlations. Building upon this foundation, an automated method called intCV, based on the XGBoost model, is introduced to effectively infer correlated variables within interrupt-driven programs. Once we accurately identify the correlated variables requiring atomic execution, existing detection techniques can be utilized to identify violations of multi-variable atomicity. Experimental results on real-world aerospace embedded software demonstrate the practicality and effectiveness of our method.