nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Predicate Abstraction Based Configurable Method for Data Race Detection in Linux Kernel

verfasst von : Pavel Andrianov, Vadim Mutilin, Alexey Khoroshilov

Erschienen in: Tools and Methods of Program Analysis

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

The paper presents a configurable method for static data race detection. The method is based on a lightweight approach that implements Lockset algorithm with a simplified memory model. The paper contributes two heavyweight extensions which allow to adjust required precision of the analysis by choosing the balance between spent resources and a number of false alarms. The extensions are (1) counterexample guided refinement based on predicate abstraction and (2) thread analysis. The approach was implemented in the CPALockator tool and was applied to Linux kernel modules. Real races found by the tool have been approved and fixed by Linux kernel developers.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Distributed Analysis of the BMC Kind: Making It Fit the Tornado Supercomputer

Nächstes Kapitel Extended Context-Free Grammars Parsing with Generalized LL

Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 141–157. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_9 CrossRef

Andrianov, P., Khoroshilov, A., Mutilin, V.: Lightweight static analysis for data race detection in operating system kernels. In: Proceedings of TMPA-2014, pp. 128–135 (2014)

Beyer, D., Keremoglu, M., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Formal Methods in Computer-Aided Design, FMCAD 2010 (2010)

Beyer, D., Henzinger, T.A., Théoduloz, G.: Configurable software verification: concretizing the convergence of model checking and program analysis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 504–518. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73368-3_51 CrossRef

Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_15 CrossRef

Craig, W.: Three uses of the herbrand-gentzen theorem in relating model theory and proof theory. J. Symbolic Logic 22(3), 269–285 (1957), https://www.cambridge.org/core/article/three-uses-of-the-herbrand-gentzen-theorem-in-relating-model-theory-and-proof-theory/7674DE501824D8FC294FB396CD5617DB

Gupta, A., Popeea, C., Rybalchenko, A.: Threader: a constraint-based verifier for multi-threaded programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 412–417. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_32 CrossRef

Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. SIGPLAN Not. 39(1), 232–244 (2004)CrossRefMATH

Inverso, O., Tomasco, E., Fischer, B., La Torre, S., Parlato, G.: Bounded model checking of multi-threaded C programs via lazy sequentialization. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 585–602. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_39

10.

Levenson, N.: Safeware: system safety and computers (1995)

11.

Mutilin, V., Novikov, E., Khoroshilov, A.: Analysis of typical faults in Linux operating system drivers (in Russian). Proc. Inst. Syst. Program. RAS 22, 349–374 (2012)CrossRef

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(5), 27–37 (1997)CrossRef

13.

Zakharov, I.S., Mutilin, V.S., Khoroshilov, A.V.: Pattern-based environment modeling for static verification of Linux kernel modules. Program. Comput. Softw. 41(3), 183–195 (2015)MathSciNetCrossRefMATH

14.

Zakharov, I., Mandrykin, M., Mutilin, V., Novikov, E., Petrenko, A., Khoroshilov, A.: Configurable toolset for static verification of operating systems kernel modules. Program. Comput. Softw. 41(1), 49–64 (2015), http://dx.doi.org/10.1134/S0361768815010065

Titel: Predicate Abstraction Based Configurable Method for Data Race Detection in Linux Kernel
verfasst von: Pavel Andrianov
Vadim Mutilin
Alexey Khoroshilov
Verlag: Springer International Publishing
Buch: Tools and Methods of Program Analysis
Print ISBN: 978-3-319-71733-3

Electronic ISBN: 978-3-319-71734-0

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-71734-0_2

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"