Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Bringing LTL Model Checking to Biologists Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

Detecting All High-Level Dataraces in an RTOS Kernel

verfasst von : Suvam Mukherjee, Arun Kumar, Deepak D’Souza

Erschienen in: Verification, Model Checking, and Abstract Interpretation

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

A high-level race occurs when an execution interleaves instructions corresponding to user-annotated critical accesses to shared memory structures. Such races are good indicators of atomicity violations. We propose a technique for detecting all high-level dataraces in a system library like the kernel API of a real-time operating system (RTOS) that relies on flag-based scheduling and synchronization. Our methodology is based on model-checking, but relies on a meta-argument to bound the number of task processes needed to orchestrate a race. We describe our approach in the context of FreeRTOS, a popular RTOS in the embedded domain.

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 Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions
Nächstes Kapitel Reachability for Dynamic Parametric Processes
Literatur
1.
Abadi, M., Flanagan, C., Freund, S.N.: Types for safe locking: static race detection for Java. ACM Trans. Program. Lang. Syst. (TOPLAS) 28(2), 207–255 (2006)CrossRef
2.
Alur, R., McMillan, K.L., Peled, D.A.: Model-checking of correctness conditions for concurrent objects. Inf. Comput. 160(1–2), 167–188 (2000)MathSciNetCrossRefMATH
3.
Artho, C., Havelund, K., Biere, A.: High-level data races. Software Test., Verification & Reliab. 13, 207–227 (2003)CrossRef
4.
Chandrasekaran, P., Kumar, K.B.S., Minz, R.L., D’Souza, D., Meshram, L.: A multi-core version of FreeRTOS verified for datarace and deadlock freedom. In: Proceedings of ACM/IEEE Formal Methods and Models for Codesign (MEMOCODE), pp. 62–71 (2014)
5.
Choi, J.-D., Lee, K., Loginov, A., O’Callahan, R., Sarkar, V., Sridharan, M.: Efficient and precise datarace detection for multithreaded object-oriented programs. In: Proceedings of ACM SIGPLAN Programming Languages Design and Implementation (PLDI), pp. 258–269. ACM, New York (2002)
6.
Dias, R.J., Pessanha, V., Lourenço, J.M.: Precise detection of atomicity violations. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 8–23. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-39611-3_​8 CrossRef
7.
Dinning, A., Schonberg, E.: Detecting access anomalies in programs with critical sections. In: Proceedings of ACM/ONR Workshop on Parallel and Distributed Debugging (PADD), pp. 85–96. ACM, New York (1991)
8.
Elmas, T., Qadeer, S., Tasiran, S.: Precise race detection and efficient model checking using locksets. Technical Report MSR-TR–118, Microsoft Research (2005)
9.
Engler, D., Ashcraft, K.: Racerx: effective, static detection of race conditions and deadlocks. SIGOPS Oper. Syst. Rev. 37(5), 237–252 (2003)CrossRef
10.
11.
Flanagan, C., Freund, S.N.: Atomizer: a dynamic atomicity checker for multithreaded programs. Sci. Comput. Program. 71(2), 89–109 (2008)MathSciNetCrossRefMATH
12.
Flanagan, C., Freund, S.N.: Fasttrack: Efficient and precise dynamic race detection. In: Proceedings of ACM SIGPLAN PLDI, pp. 121–133. ACM, New York (2009)
13.
Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: Proceedings of ACM SIGPLAN Programming Language Design and Implementation (PLDI), pp. 338–349 (2003)
14.
Havelund, K., Lowry, M.R., Penix, J.: Formal analysis of a space-craft controller using SPIN. IEEE Trans. Softw. Eng. 27(8), 749–765 (2001)CrossRef
15.
Havelund, K., Skakkebæk, J.U.: Applying model checking in Java verification. In: Dams, D., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 216–231. Springer, Heidelberg (1999). doi:10.​1007/​3-540-48234-2_​17 CrossRef
16.
Henzinger, T.A., Jhala, R., Majumdar, R.: Race checking by context inference. In: Proceedings of ACM SIGPLAN Programming Language Design and Implementation (PLDI), pp. 1–13 (2004)
17.
Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463–492 (1990)CrossRef
18.
Holzmann, G.J.: The model checker spin. IEEE Trans. Softw. Eng. 23, 279–295 (1997)CrossRef
19.
Kahlon, V., Sinha, N., Kruus, E., Zhang, Y.: Static data race detection for concurrent programs with asynchronous calls. In: ACM SIGSOFT FSE, pp. 13–22. ACM, New York (2009)
20.
Lu, S., Tucek, J., Qin, F., Zhou, Y.: AVIO: detecting atomicity violations via access interleaving invariants. In: Proceedings of Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp. 37–48 (2006)
21.
Mukherjee, S., Arunkumar, S., D’Souza, D.: Proving an RTOS kernel free of data-races. Technical Report CSA-TR-2016-1, Department of Computer Science and Automation, IISc (2016)
22.
Qadeer, S., Wu, D.: KISS: keep it simple and sequential. In: Proceedings of ACM SIG-PLAN Programming Languages Design and Implementaion (PLDI), pp. 14–24 (2004)
23.
Real Time Engineers Ltd., The FreeRTOS Real Time Operating System (2014)
24.
Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.: Eraser: a dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst. (TOCS) 15(4), 391–411 (1997)CrossRef
25.
Schwarz, M.D., Seidl, H., Vojdani, V., Apinis, K.: Precise analysis of value-dependent synchronization in priority scheduled programs. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 21–38. Springer, Heidelberg (2014). doi:10.​1007/​978-3-642-54013-4_​2 CrossRef
26.
Schwarz, M.D., Seidl, H., Vojdani, V., Lammich, P., Müller-Olm, M.: Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol. In: Proceedings ACM SIGPLAN-SIGACT Principles of Programming Languages (POPL), pp. 93–104 (2011)
27.
Sterling, N.: WARLOCK - a static data race analysis tool. In: Proceedings of Usenix Winter Technical Conference, pp. 97–106 (1993)
28.
von Praun, C., Gross, T.R.: Static detection of atomicity violations in object-oriented programs. J. Object Technol. 3(6), 103–122 (2004)CrossRef
29.
Voung, J. W., Jhala, R., Lerner, S.: RELAY: static race detection on millions of lines of code. In: Proceedings of ESEC/SIGSOFT Foundation of Software Engineering (FSE), pp. 205–214 (2007)
30.
Wang, L., Stoller, S.D.: Runtime analysis of atomicity for multithreaded programs. IEEE Trans. Softw. Eng. 32(2), 93–110 (2006)CrossRef
31.
Xu, M., Bodík, R., Hill, M.D.: A serializability violation detector for shared-memory server programs. In: Proceedings of ACM SIGPLAN Programming Language Design and Implementation (PLDI), pp. 1–14 (2005)
32.
Zeng, R., Sun, Z., Liu, S., He, X.: McPatom: a predictive analysis tool for atomicity violation using model checking. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 191–207. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-31759-0_​14 CrossRef
Metadaten
Titel
Detecting All High-Level Dataraces in an RTOS Kernel
verfasst von
Suvam Mukherjee
Arun Kumar
Deepak D’Souza
Copyright-Jahr
2017
Buch
Verification, Model Checking, and Abstract Interpretation

Print ISBN: 978-3-319-52233-3

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

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-52234-0_22