Martin D. Schwarz, Helmut Seidl, Vesal Vojdani and Kalmer Apinis. Precise Analysis of Value-Dependent Synchronization in Priority Scheduled Programs. Verification, Model Checking, and Abstract Interpretation, volume 8318 of Lecture Notes in Computer Science, pages 21-38, 2014. Springer Berlin Heidelberg.
Although priority scheduling in concurrent programs provides a clean way of synchronization, developers still additionally rely on hand-crafted schemes based on integer variables to protect critical sections. We identify a set of sufficient conditions for variables to serve this purpose. We provide efficient methods to verify these conditions, which enable us to construct an enhanced analysis of mutual exclusion in interrupt-driven concurrent programs. All our algorithms are build upon off-the-shelf inter-procedural analyses alone. We have implemented this approach for the analysis of automotive controllers, and demonstrate that it results in a major improvement in the precision of data race detection compared to purely priority-based techniques.