Adjustable method with predicate abstraction for detection of race conditions in operating systems
https://doi.org/10.15514/ISPRAS-2016-28(6)-5
Abstract
The paper presents a configurable method of static data race detection that is trying to keep a balance between resource consumption and a number of false alarms. The method is based on well known Lockset approach. It uses simplified memory model to be fast enough. At the same time it includes advanced techniques aimed to achieve acceptable false alarms rate. The key techniques are thread analysis and predicate abstraction based refinement. The method was implemented in CPALockator tool built on top of CPAchecker framework. The tool was evaluated on Linux kernel modules and it has detected several actual data races, which were approved by developers and were fixed in upstream Linux kernel.
About the Authors
P. S. Andrianov
Institute for System Programming of the RAS
Russian Federation
Russian Federation
V. S. Mutilin
Institute for System Programming of the RAS
Russian Federation
Russian Federation
A. V. Khoroshilov
1Institute for System Programming of the RAS; Lomonosov Moscow State University; Moscow Institute of Physics and Technology (State University); National Research University Higher School of Economics (HSE)
Russian Federation
Russian Federation
References
1. Mutilin V.S., Novikov E.M., Khoroshilov A.V. Analysis of typical faults in Linux operating system drivers. Trudy ISP RAN / Proc. ISP RAS, vol. 22, 2012, pp. 349–374 (in Russian). DOI: 10.15514/ISPRAS-2012-22-19
2. Nancy Levenson, Safeware: System Safety and Computers, 1995
3. Nachum Dershowitz, Software horror stories, http://www.cs.tau.ac.il/~nachumd/pub.html
4. Cordeiro, L., Fischer, B.: Verifying Multi-Threaded Software using SMT-based Context-Bounded Model Checking. In: ICSE, pp. 331–340 (2011)
5. E. Clarke, D. Kroening, N. Sharygina, K. Yorav. SATABS: SAT-based predicate abstraction for ANSI-C. Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05), pp. 570-574, 2005.
6. A. Gupta, C. Popeea, A. Rybalchenko. Predicate abstraction and refinement for verifying multi-threaded programs In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2011), pp. 331-344, 2011.
7. A. Gupta, C. Popeea, A. Rybalchenko. Threader: a constraint-based verifier for multi-threaded programs In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV 2011), LNCS, vol. 6806, pp. 412-417, 2011.
8. Stefan Savage, Michael Burrows, Greg Nelson, Patric Sobalvarro, Thomas Anderson Eraser: A Dynamic Data Race Detector for Multithreaded Programs ACM Transactions on Computer Systems, Vol. 15, No. 4, November 1997, Pages 391–411.
9. Dirk Beyer, Thomas A. Henzinger, and Gregory Theoduloz, Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis, ACM Transactions on Computer Systems, Vol. 15, No. 4, November 1997, Pages 391–411.
10. Andrianov P.S., Mutilin V.S., Khoroshilov A.V. Lightweight Static Analysis for Data Race Detection in Operating System Kernels. Trudy ISP RAN / Proc. ISP RAS, vol. 27, 2015, pp. 87-116 (in Russian). DOI: 10.15514/ISPRAS-2015-27(5)-6
11. Dirk Beyer , M. Erkan Keremoglu , Philipp Wendler, Predicate abstraction with adjustable-block encoding, Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design, October 20-23, 2010, Lugano, Switzerland
12. Mandrykin M.U., Mutilin V.S., Khoroshilov A.V. Introduction to CEGAR — Counter-Example Guided Abstraction Refinement. Trudy ISP RAN / Proc. ISP RAS, vol. 24, 2013, pp. 219-292 (in Russian). DOI: 10.15514/ISPRAS-2013-24-12
13. Shostak R., Deciding Combinations of Theories, Journal of the ACM, 1-12, 1984
14. Beyer Dirk, Zuerey Damien, Majumdar Rupak., Csisat: Interpolation for la+euf, CAV, 304-308, 2008
15. Bruttomesso Roberto, Cimatti Alessandro, Franzen Anders, Griggio Alberto, Sebastiani Roberto., The mathsat 4 smt solver, CAV, 299-303, 2008
16. Alexey Khoroshilov, Mikhail Mandrykin, Vadim Mutilin, Eugene Novikov, Alexander Petrenko, Ilya Zakharov. Configurable toolset for static verification of operating systems kernel modules. Programming and Computer Software, vol. 41, № 1, 2015, pp. 49-64. DOI: 10.1134/S0361768815010065
17. Alexey Khoroshilov, Mikhail Mandrykin, Vadim Mutilin, Eugene Novikov, Pavel Shved. Using Linux Device Drivers for Static Verification Tools Benchmarking. Programming and Computer Software, vol. 38, № 5, 2012, pages 245-256. DOI: 10.1134/S0361768812050039
18. Alexey Khoroshilov,Vadim Mutilin, Ilya Zakharov. Pattern-based environment modeling for static verification of Linux kernel modules. Programming and Computer Software, vol. 41, № 3, 2015, pages 183-195. DOI: 10.1134/S036176881503007X
Review
For citations:
Andrianov P.S., Mutilin V.S., Khoroshilov A.V. Adjustable method with predicate abstraction for detection of race conditions in operating systems. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2016;28(6):65-86. (In Russ.) https://doi.org/10.15514/ISPRAS-2016-28(6)-5
Email this article 