Analysis of correct synchronization of operating system components
https://doi.org/10.15514/ISPRAS-2019-31(5)-16
Abstract
Most of the software model checker tools do not scale well on complicated software. Our goal was to develop a tool, which provides an adjustable balance between precise and slow software model checkers and fast and imprecise static analyzers. The key idea of the approach is an abstraction over the precise thread interaction and analysis for each thread in a separate way, but together with a specific environment, which models effects of other threads. The environment contains a description of potential actions over the shared data and synchronization primitives, and conditions for its application. Adjusting the precision of the environment, one can achieve a required balance between speed and precision of the complete analysis. A formal description of the suggested approach was performed within a Configurable Program Analysis theory. It allows formulating assumptions and proving the soundness of the approach under the assumptions. For efficient data race detection we use a specific memory model, which allows to distinguish memory domains into the disjoint set of regions, which correspond to a data types. An implementation of the suggested approach into the CPAchecker framework allows reusing an existed approaches with minimal changes. Implementation of additional techniques according to the extended theory allows to increase the precision of the analysis. Results of the evaluation allow confirming scalability and practical usability of the approach.
About the Author
Pavel Sergeevich Andrianov
Ivannikov Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Junior researcher
Russian Federation
Junior researcher
References
1. Parosh Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. Optimal dynamic partial order reduction. SIGPLAN Notices, vol. 49, issue 1, 2014, pp. 373–384.
2. Patrice Godefroid. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer-Verlag, Berlin, Heidelberg, 1996, 143 p.
3. Gérard Basler, Michele Mazzucchi, Thomas Wahl, and Daniel Kroening. Symbolic counter abstraction for concurrent software. Lecture Notes in Computer Science, vol. 5643, 2009, pp. 64–78.
4. Dirk Beyer. Automatic verification of C and Java Programs: SV-COMP. Lecture Notes in Computer Science, vol. 11429, 2019, pp. 133–155.
5. Dirk Beyer, Thomas A. Henzinger, and Grégory Théoduloz. Configurable software verification: concretizing the convergence of model checking and program analysis. Lecture Notes in Computer Science, vol. 4590, 2007, pp. 504–518
6. D. Beyer, T.A. Henzinger, and G. Theoduloz. Program analysis with dynamic precision adjustment. In Proc. of the 23rd IEEE/ACM International Conference on Automated Software Engineering, 2008, pp. 29–38.
7. Cormac Flanagan and Shaz Qadeer. Thread-modular model checking. Lecture Notes in Computer Science, vol. 2648, 2003, pp. 213–224.
8. Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Shaz Qadeer. Thread-Modular Abstraction Lecture Notes in Computer Science, vol. 2725, 2003, pp, 262–274.
9. Byron Cook, Daniel Kroening, and Natasha Sharygina. Verification of Boolean programs with unbounded thread creation. Theoretical Computer Science, vol. 388, issue 1-3, 2007, pp. 227–242.
10. Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. Threader: A constraint-based verifier for multi-threaded programs. Lecture Notes in Computer Science, vol. 6806, 2011, pp. 412–417.
11. E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. Lecture Notes in Computer Science, vol. 1855, 2000, pp. 154–169.
12. Susanne Graf and Hassen Saidi. Construction of abstract state graphs with PVS. Lecture Notes in Computer Science, vol. 1254, 1997, pp. 72–83.
13. Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro, and Thomas Anderson. Eraser: A dynamic data race detector for multi-threaded programs. ACM SIGOPS Operating Systems Review, vol. 31, issue 5, 1997, pp. 27–37.
14. Richard Bornat. Proving pointer programs in Hoare logic. Lecture Notes in Computer Science, vol. 1837, 2000, pp. 102–126.
15. R M Burstall. Some techniques for proving correctness of programs which alter data structures. Machine Intelligence, vol. 7, 1972, pp. 23–50.
16. Pavel Andrianov, Karlheinz Friedberger, Mikhail Mandrykin, Vadim Mutilin, and Anton Volkov. CPA-BAM-BnB: Block-abstraction memoization and region-based memory models for predicate abstractions. Lecture Notes in Computer Science, vol. 10206, 2017, pp. 355–359.
17. Evgeny Novikov and Ilja Zakharov. Towards automated static verification of GNU C programs. Lecture Notes in Computer Science, vol. 10742, 2018, pp. 402–416.
18. Evgeny Novikov and Ilja Zakharov. Verification of operating system monolithic kernels without extensions. Lecture Notes in Computer Science, vol. 11247, 2018, pp. 230–248.
19. Dirk Beyer and Karlheinz Friedberger. In Proc. of the 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, 2016, pp. 61–71.
20. Dirk Beyer and Stefan Löwe. Explicit-state software model checking based on CEGAR and interpolation. Lecture Notes in Computer Science, vol. 7793, 2013, pp. 146–162.
21. D. Beyer, M.E. Keremoglu, and P. Wendler. Predicate abstraction with adjustable-block encoding. In Proc. of 10th International Conference on Formal Methods in Computer-Aided Design, 2010, pp. 189–197.
22. Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. Symbolic model checking without bdds. Lecture Notes in Computer Science, vol. 1579, 1999, pp. 193–207
23. Dirk Beyer, Stefan Löwe, and Philipp Wendler. Reliable benchmarking: requirements and solutions. International Journal on Software Tools for Technology Transfer, vol. 21, issue 1, 2019, pp. 1–29.
24. Shaz Qadeer and Jakob Rehof. Context-bounded model checking of concurrent software. Lecture Notes in Computer Science, vol. 3440, 2005, pp. 93–107.
25. Lucas Cordeiro, Jeremy Morse, Denis Nicole, and Bernd Fischer. Context-bounded model checking with esbmc 1.17. Lecture Notes in Computer Science, vol. 7214, 2012, pp. 534–537.
26. Ariel Cohen and Kedar S. Namjoshi. Local proofs for global safety properties. Formal Methods in System Design, vol. 34, issue 2, 2009, pp. 104–125.
27. Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Race checking by context inference. In Proc. of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation, 2004, pp. 1–13.
28. Alexander Malkis, Andreas Podelski, and Andrey Rybalchenko. Thread-modular verification is cartesian abstract interpretation. Lecture Notes in Computer Science, vol. 4281, 2006, pp. 183–197.
29. Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. Predicate abstraction and refinement for verifying multi-threaded programs. ACM SIGPLAN Notices, vol. 46, issue 1m 2011, pp. 331–344.
30. Akash Lal and Thomas Reps. Reducing concurrent analysis under a context bound tosequential analysis. Formal Methods in System Design, vol. 35, issue 1, 2009, pp. 73–97.
31. Salvatore La Torre, P. Madhusudan, and Gennaro Parlato. Reducing context-bounded concurrent reachability to sequential reachability. Lecture Notes in Computer Science, vol. 5643, 2009, pp. 477–492.
32. Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. MU-CSeq: Sequentialization of C programs by shared memory unwindings. Lecture Notes in Computer Science, vol. 8413, 2014, pp. 402–404.
33. Pantazis Deligiannis, Alastair F. Donaldson, and Zvonimir Rakamaric. Fast and precise symbolic analysis of concurrency bugs in device drivers (t). In Proc. of the 2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2015, pp. 166–177.
34. Akash Lal, Shaz Qadeer, and Shuvendu K. Lahiri. A solver for reachability modulo theories. Lecture Notes in Computer Science, vol. 7358, 2012, pp. 427–443.
35. Jan Wen Voung, Ranjit Jhala, and Sorin Lerner. RELAY: Static race detection on millions of lines of code. In Proceedings of the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering, 2007, pp. 205–214.
36. Polyvios Pratikakis, Jeffrey S. Foster, and Michael Hicks. LOCKSMITH: Context-sensitive correlation analysis for race detection. In Proc. of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2006, pp. 320–331.
37. Peng Di and Yulei Sui. Accelerating dynamic data race detection using static thread interference analysis. In Proc. of the 7th International Workshop on Programming Models and Applications for Multicores and Manycores, 2016, pp. 30–39.
38. Daniel Kroening, Lihao Liang, Tom Melham, Peter Schrammel, and Michael Tautschnig. Effective verification of low-level software with nested interrupts. In the Europe Conference & Exhibition on Design, Automation & Test, 2015, pp. 229–234.
39. Suvam Mukherjee, Arun Kumar, and Deepak D’Souza. Detecting all high-level dataraces in an RTOS kernel. Lecture Notes in Computer Science, vol. 10145, 2017, pp. 405–423.
40. Nikita Chopra, Rekha Pai, and Deepak D’Souza. Data races and static analysis for interrupt-driven kernels. Lecture Notes in Computer Science, vol. 11423, 2019, pp. 697–723.
41. Jia-Ju Bai, Julia Lawall, Qiu-Liang Chen, and Shi-Min Hu. Effective static analysis of concurrency use-after-free bugs in Linux device drivers. In the USENIX Annual Technical Conference, 2019, pp. 255–268.
42. Dirk Beyer, Marie-Christine Jakobs, Thomas Lemberger, and Heike Wehrheim. Reducer-based construction of conditional verifiers. In Proceedings of the 40th International Conference on Software Engineering, 2018, pp. 1182–1193.
Review
For citations:
Andrianov P.S. Analysis of correct synchronization of operating system components. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2019;31(5):203-232. (In Russ.) https://doi.org/10.15514/ISPRAS-2019-31(5)-16
Email this article 