@inproceedings{2dbf7dec036b485d87dbcd13a5535a6c,
title = "Precise analysis of value-dependent synchronization in priority scheduled programs",
abstract = "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.",
author = "Schwarz, {Martin D.} and Helmut Seidl and Vesal Vojdani and Kalmer Apinis",
year = "2014",
doi = "10.1007/978-3-642-54013-4_2",
language = "English",
isbn = "9783642540127",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "21--38",
booktitle = "Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, Proceedings",
note = "15th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2014 ; Conference date: 20-01-2014 Through 21-01-2014",
}