×

Analysis of correct synchronization of operating system components. (English) Zbl 1467.68032

Summary: 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.

MSC:

68N25 Theory of operating systems
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Abdulla, P.; Aronis, S.; Jonsson, B.; Sagonas, K., Optimal dynamic partial order reduction, SIGPLAN Not., 49, 373-384 (2014) · Zbl 1284.68377
[2] Godefroid, P., Partial-Order Methods for the Verification of Concurrent Systems: an Approach to the State-Explosion Problem (1996), Berlin, Heidelberg: Springer-Verlag, Berlin, Heidelberg · Zbl 1293.68005
[3] Basler, G., Mazzucchi, M., Wahl, T., and Kroening, D., Symbolic counter abstraction for concurrent software, in Proc. 21st Int. Conf. on Computer Aided Verification, CAV’09, Berlin, Heidelberg: Springer-Verlag, 2009, pp. 64-78. · Zbl 1242.68055
[4] Beyer, D., Automatic verification of C and Java programs: SV-COMP 2019, in Tools and Algorithms for the Construction and Analysis of Systems, Beyer, D. Huisman, M. Kordon, F. and Steffen, B., Eds., Cham: Springer Int. Publ., 2019, pp. 133-155.
[5] Beyer, D., Henzinger, T.A., and Theoduloz, G., Program analysis with dynamic precision adjustment, in Proc. 23rd IEEE/ACM Int. Conf. on Automated Software Engineering, ASE 2008, L’Aquila, Sept. 2008, pp. 29-38.
[6] Flanagan C. and Qadeer, S., Thread-modular model checking, in Proc. 10th Int. Conf. on Model Checking Software, SPIN’03, Berlin, Heidelberg: Springer-Verlag, 2003, pp. 213-224. · Zbl 1023.68529
[7] Henzinger, T. A.; Jhala, R.; Majumdar, R.; Qadeer, S., Thread-Modular Abstraction Refinement (2003), Berlin, Heidelberg: Springer, Berlin, Heidelberg
[8] Cook, B.; Kroening, D.; Sharygina, N., Verification of boolean programs with unbounded thread creation, Theor. Comput. Sci., 388, 227-242 (2007) · Zbl 1143.68043
[9] Gupta, A., Popeea, C., and Rybalchenko, A., Threader, a constraint-based verifier for multi-threaded programs, in Proc. 23rd Int. Conf. on Computer Aided Verification, CAV’11, Berlin, Heidelberg: Springer-Verlag, 2011, pp. 412-417.
[10] Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., and Veith, H., Counter example-guided abstraction refinement, Proc. CAV 2000: Computer Aided Verification, Chicago, 2000, pp. 154-169. · Zbl 0974.68517
[11] Graf, S.; Saidi, H., Computer Aided Verification (1997), Berlin, Heidelberg: Springer, Berlin, Heidelberg
[12] Savage, S.; Burrows, M.; Nelson, G.; Sobalvarro, P.; Anderson, T., Eraser: a dynamic data race detector for multi-threaded programs, SIGOPS Oper. Syst. Rev., 31, 27-37 (1997)
[13] Bornat, R., Proving pointer programs in Hoare logic, in Proc. 5th Int. Conf. on Mathematics of Program Construction, MPC’00, London: Springer-Verlag, 2000, pp. 102-126. · Zbl 0963.68036
[14] Burstall, R. M., Machine Intelligence 7 (1972), New York: American Elsevier, New York
[15] Andrianov, P.; Friedberger, K.; Mandrykin, M.; Mutilin, V.; Volkov, A., Tools and Algorithms for the Construction and Analysis of Systems (2017), Berlin, Heidelberg: Springer, Berlin, Heidelberg
[16] Novikov, E.; Zakharov, I., Perspectives of System Informatics (2018), Cham: Springer Int. Publ., Cham
[17] Novikov, E.; Zakharov, I., Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice (2018), Cham: Springer Int. Publ., Cham
[18] Beyer, D. and Friedberger, K., A light-weight approach for verifying multithreaded programs with CPAchecker, in Proc. 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2016) Telč, Czechia, Oct. 21-23,2016, Bouda, J., Holík, L., Kofroñ, J., Strejček, J., and Rambousek, A., Eds., 2016, pp. 61-71.
[19] Beyer, D. and Löwe, S., Explicit-state software model checking based on CEGAR and interpolation, in Proc. 16th Int. Conf. on Fundamental Approaches to Software Engineering (FASE 2013, Rome, Italy, March 20-22,2013), Heidelberg: Springer-Verlag, 2013, pp. 146-162.
[20] Beyer, D., Keremoglu, M.E., and Wendler, P., Predicate abstraction with adjustableblock encoding, Proc. Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, 2010.
[21] Biere, A., Cimatti, A., Clarke, E.M., and Zhu, Y., Symbolic model checking without bdds, in Proc. 5th Int. Conf. on Tools and Algorithms for Construction and Analysis of Systems, TACAS’99, London: Springer-Verlag, 1999, pp. 193-207.
[22] Beyer, D., Henzinger, T.A., and Théoduloz, G., Configurable software verification: concretizing the convergence of model checking and program analysis, in Proc. CAV, Berlin, Heidelberg: Springer-Verlag, 2007, pp. 504-518. · Zbl 1135.68466
[23] Beyer, D.; Löwe, S.; Wendler, P., Reliable benchmarking: requirements and solutions, Int. J. Software Tools Technol. Transfer, 21, 1-29 (2019)
[24] Qadeer, S.; Rehof, J., Tools and Algorithms for the Construction and Analysis of Systems (2005), Berlin, Heidelberg: Springer, Berlin, Heidelberg · Zbl 1087.68598
[25] Cordeiro, L., Morse, J., Nicole, D., and Fischer, B., Context-bounded model checking with esbmc 1.17, in Proc. 18th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’12, Berlin, Heidelberg: Springer-Verlag, 2012, pp. 534-537.
[26] Cohen, A.; Namjoshi, K. S., Local proofs for global safety properties, Formal Methods Syst. Des., 34, 104-125 (2009) · Zbl 1176.68118
[27] Henzinger, T.A., Jhala, R., and Majumdar, R., Race checking by context inference, in Proc. ACM SIGPLAN 2004 Conf. on Programming Language Design and Implementation, PLDI’04, New York: ACM, 2004, pp. 1-13.
[28] Malkis, A.; Podelski, A.; Rybalchenko, A., Proc. Theoretical Aspects of Computing - ICTAC 2006 (2006), Berlin, Heidelberg: Springer, Berlin, Heidelberg
[29] Gupta, A.; Popeea, C.; Rybalchenko, A., Predicate abstraction and refinement for verifying multi-threaded programs, SIGPLAN Not., 46, 331-344 (2011) · Zbl 1284.68427
[30] Lal, A.; Reps, T., Reducing concurrent analysis under a context bound tosequential analysis, Formal Methods Syst. Des., 35, 73-97 (2009) · Zbl 1186.68298
[31] La Torre, S.; Madhusudan, P.; Parlato, G., Computer Aided Verification (2009), Berlin, Heidelberg: Springer, Berlin, Heidelberg
[32] Tomasco, E.; Inverso, O.; Fischer, B.; La Torre, S.; Parlato, G., Tools and Algorithms for the Construction and Analysis of Systems (2014), Berlin, Heidelberg: Springer, Berlin, Heidelberg
[33] Deligiannis, P., Donaldson, A.F., and Rakamaric, Z., Fast and precise symbolic analysis of concurrency bugs in device drivers (t), in Proc. 30th IEEE/ACM Int. Conf. on Automated Software Engineering, ASE’15, Washington: IEEE Computer Soc., 2015, pp. 166-177.
[34] Lal, A., Qadeer, S., and Lahiri, S.K., A solver for reachability modulo theories, in Proc. 24th Int. Conf. on Computer Aided Verification, CAV’12, Berlin, Heidelberg: Springer-Verlag, 2012, pp. 427-443.
[35] Voung, J.W., Jhala, R., and Lerner, S., RELAY: static race detection on millions of lines of code, in Proc. 6th Joint Meeting of the European Software Engineering Conf. and the ACM SIGSOFT Symp. on the Foundations of Software Engineering, ESEC-FSE’07, New York: ACM, 2007, pp. 205-214.
[36] Pratikakis, P., Foster, J.S., and Hicks, M., LOCKSMITH: context sensitive correlation analysis for race detection, in Proc. 27th ACM SIGPLAN Conf. on Programming Language Design and Implementation, PLDI’06, New York: ACM, 2006, pp. 320-331.
[37] Di, P. and Sui, Y., Accelerating dynamic data race detection using static thread interference analysis, in Proc. 7th Int. Workshop on Programming Models and Applications for Multicores and Manycores, PMAM’16, New York: ACM, 2016, pp. 30-39.
[38] Kroening, D., Liang, L., Melham, T., Schrammel, P., and Tautschnig, M., Effective verification of low-level software with nested interrupts, Proc. ACM Design, Automation & Test in Europe Conf. & Exhibition (DATE 2015), Grenoble, March 2015, pp. 229-234.
[39] Mukherjee, S.; Kumar, A.; D’Souza, D., Verification, Model Checking, and Abstract Interpretation (2017), Cham: Springer Int. Publ., Cham
[40] Chopra, N.; Pai, R.; D’Souza, D., Programming Languages and Systems (2019), Cham: Springer Int. Publ., Cham
[41] Bai, J.-J., Lawall, J., Chen, Q.-L., and Hu, S.-M., Effective static analysis of concurrency use-after-free bugs in Linux device drivers, in Proc. USENIX Annu. Technical Conf. (USENIX ATC 19), Renton, WA: USENIX Assoc., July 2019, pp. 255-268.
[42] Beyer, D., Jakobs, M.-C., Lemberger, T., and Wehrheim, H., Reducer-based construction of conditional verifiers, in Proc. 40th Int. Conf. on Software Engineering, ICSE’18, New York: ACM, 2018, pp. 1182-1193.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.