×

Static analysis of embedded real-time concurrent software with dynamic priorities. (English) Zbl 1412.68042

Mastroeni, Isabella (ed.), Proceedings of the 6th international workshop on numerical and symbolic abstract domains, NSAD 2016, Edinburgh, UK, September 11, 2016. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 331, 3-39 (2017).
Summary: In previous work, we developed a sound static analysis by abstract interpretation to check the absence of run-time errors in concurrent programs, focusing on embedded C programs composed of a fixed set of threads in a shared memory. The method is thread-modular: it considers each thread independently, analyzing them with respect to an abstraction of the effect of the other threads, so-called interference, which are also inferred automatically as part of analyzing the threads. The analysis thus proceeds in a series of rounds that reanalyze all threads, gathering an increasing set of interference, until stabilization. We proved that this method is sound and covers all possible thread interleavings. This analysis was integrated into the Astrée industrial-scale static analyzer, deployed in avionics and automotive industries.
In this article, we consider the more specific case of programs running under a priority-based real-time scheduler, as is often the case in embedded systems. In such programs, higher priority threads cannot be preempted by lower priority ones (except when waiting explicitly for some resource). The programmer exploits this property to reduce the reliance on locks when protecting critical sections. We show how our analysis can be refined through partitioning in order to take into account the real-time hypothesis, remove spurious interleavings, and gain precision on programs that rely on priorities. Our analysis supports in particular dynamic priorities: we handle explicit modifications of the priorities by the program, as well as implicit ones through the priority ceiling protocol.
We illustrate our construction formally on an idealized language. Following previous work, we first provide a concrete semantics in thread-modular denotational form that is complete for safety properties, and then show how to apply classic abstractions to obtain an effective static analyzer, able to detect all run-time errors, data-races, as well as deadlocks. Finally, we briefly discuss our implementation inside the Astrée analyzer and on-going experimentation, with results limited for now to small programs.
For the entire collection see [Zbl 1375.68021].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q55 Semantics in the theory of computing
68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] AUTOSAR (AUTomotive Open System ARchitecture)
[2] DO-178C: Software considerations in airborne systems and equipment certification, 2011.
[3] Adve, S. V.; Hill, M. D., Weak ordering - A new definition, Proc. of the 17th ACM SIGARCH Symp. on Comp. Arch. (ISCA’90), vol. 18, 2-14, (June 1990), ACM
[4] Aeronautical radio inc. ARINC 653
[5] Atig, M. F.; Bouajjani, A.; Burckhardt, S.; Musuvathi, M., On the verification problem for weak memory models, (POPL’10, (Jan. 2010), ACM), 7-18 · Zbl 1312.68050
[6] Bertrane, J.; Cousot, P.; Cousot, R.; Feret, J.; Mauborgne, L.; Miné, A.; Rival, X., Static analysis and verification of aerospace software by abstract interpretation, (AIAA Infotech@Aerospace, AIAA, vol. 2010-3385, (Apr. 2010), AIAA (American Institute of Aeronautics and Astronautics)), 1-38
[7] Boehm, H.-J., How to miscompile programs with “benign” data races, (Proceedings of the 3rd USENIX Conference on Hot Topic in Parallelism, HotPar’11, (2011), USENIX Association), 3
[8] Bourdoncle, F., Efficient chaotic iteration strategies with widenings, (Proc. of the Int. Conf. on Formal Methods in Programming and their Applications (FMPA’93), LNCS, vol. 735, (June 1993), Springer), 128-141
[9] Cai, Y.; Chan, W. K., Magiclock: scalable detection of potential deadlocks in large-scale multithreaded programs, IEEE Trans. Softw. Eng., 40, 266-281, (2014)
[10] Carré, J.-L.; Hymans, C., From single-thread to multithreaded: an efficient static analysis algorithm, (Oct. 2009), EADS, Technical Report
[11] Cousot, P., Constructive design of a hierarchy of semantics of a transition system by abstract interpretation, Theoretical Computer Science, 277, 1-2, 47-103, (2002) · Zbl 0996.68119
[12] Cousot, P.; Cousot, R., Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints, (POPL’77, (Jan. 1977), ACM), 238-252
[13] Cousot, P.; Cousot, R., Invariance proof methods and analysis techniques for parallel programs, (Automatic Program Construction Techniques, (1984), Macmillan New York, NY, USA), 243-271, chapter 12
[14] Delmas, D.; Souyris, J., Astrée: from research to industry, (SAS’07, LNCS, vol. 4634, (Aug. 2007), Springer), 437-451
[15] Flanagan, C.; Qadeer, S., Thread-modular model checking, (SPIN’03, LNCS, vol. 2648, (2003), Springer), 213-224 · Zbl 1023.68529
[16] Godefroid, P., Partial-order methods for the verification of concurrent systems - an approach to the state-explosion problem, (1994), University of Liege, Computer Science Department, PhD thesis
[17] IEEE computer society and the open group. portable operating system interface (POSIX) - application program interface (API) amendment 2: threads extension (C language), (1995), Technical report, ANSI/IEEE Std. 1003.1c-1995
[18] Jeannet, B., Relational interprocedural verification of concurrent programs, Software & Systems Modeling, 12, 2, 285-306, (2013)
[19] Jones, C. B., Development methods for computer programs including a notion of interference, (Jun. 1981), Oxford University, PhD thesis
[20] Kästner, D.; Wilhelm, S.; Nenova, S.; Cousot, P.; Cousot, R.; Feret, J.; Mauborgne, L.; Miné, A.; Rival, X., Astrée: proving the absence of runtime errors, (Proc. of Embedded Real Time Software and Systems (ERTS2 2010), (May 2010)), 9
[21] Levis, P.; Madden, S.; Polastre, J.; Szewczyk, R.; Whitehouse, K.; Woo, A.; Gay, D.; Hill, J.; Welsh, M.; Brewer, E.; Culler, D., Tinyos: an operating system for sensor networks, 115-148, (2005), Springer Berlin Heidelberg
[22] Malkis, A.; Podelski, A.; Rybalchenko, A., Thread-modular verification is Cartesian abstract interpretation, (ICTAC’06, LNCS, vol. 4281, (2006)), 183-197 · Zbl 1168.68423
[23] Mauborgne, L.; Rival, X., Trace partitioning in abstract interpretation based static analyzer, (ESOP’05, LNCS, vol. 3444, (2005), Springer), 5-20 · Zbl 1108.68427
[24] Miné, A., Static analysis of run-time errors in embedded critical parallel C programs, (Proc. of the 20th European Symp. on Programming (ESOP’11), LNCS, vol. 6602, (Mar. 2011), Springer), 398-418 · Zbl 1239.68021
[25] Miné, A., Static analysis by abstract interpretation of sequential and multi-thread programs, (MOVEP’12, (Dec. 2012)), 35-48
[26] Miné, A., Relational thread-modular static value analysis by abstract interpretation, (Proc. of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’14), LNCS, vol. 8318, (2014), Springer), 39-58 · Zbl 1428.68119
[27] Miné, A.; Delmas, D., Towards an industrial use of sound static analysis for the verification of concurrent embedded avionics software, (Proc. of the 15th International Conference on Embedded Software (EMSOFT’15), (Oct. 2015), IEEE CS Press), 65-74
[28] Miné, A.; Mauborgne, L.; Rival, X.; Feret, J.; Cousot, P.; Kästner, D.; Wilhelm, S.; Ferdinand, C., Taking static analysis to the next level: proving the absence of run-time errors and data races with astrée, (Proc. of Embedded Real Time Software and Systems (ERTS2 2016), (Jan 2016)), 570-579
[29] Monniaux, D., Verification of device drivers and intelligent controllers: a case study, (Proc. of the 7th ACM & IEEE International conference on Embedded software (EMSOFT’07), (Oct. 2007), ACM), 30-36
[30] Naik, M.; Park, C.-S.; Sen, K.; Gay, D., Effective static deadlock detection, (Proceedings of the 31st International Conference on Software Engineering, ICSE ’09, (2009), IEEE Computer Society), 386-396
[31] Ouadjaout, A.; Miné, A.; Lasla, N.; Badache, N., Static analysis by abstract interpretation of functional properties of device drivers in tinyos, Journal of Systems and Software (JSS), 120, 114-132, (2016)
[32] Qadeer, S.; Rehof, J., Context-bounded model checking of concurrent software, (Proc. of the 11th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’05), LNCS, vol. 3440, (2005), Springer), 93-107 · Zbl 1087.68598
[33] Qadeer, S.; Wu, D., KISS: keep it simple and sequential, (Proc. of the ACM SIGPLAN Conf. on Programming Languages Design and Implementation (PLDI’04), (June 2004), ACM), 14-24
[34] Reynolds, J. C., Toward a grainless semantics for shared-variable concurrency, (Proc. of the Annual Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’04), LNCS, vol. 3328, (Dec. 2004), Springer), 35-48 · Zbl 1117.68449
[35] 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, SIGPLAN Not., 46, 1, 93-104, (January 2011) · Zbl 1284.68199
[36] Suzanne, T.; Miné, A., From array domains to abstract interpretation under store-buffer-based memory models, (Proc. of the 23st International Static Analysis Symposium (SAS’16), LNCS, vol. 9837, (Sep. 2016), Springer), 469-488
[37] Vojdani, V.; Goblint, V. Vene, Path-sensitive data race analysis, Annales Univ. Sci. Budapest, Sect. Comp., 30, (2009) · Zbl 1199.68107
[38] Watkins, C. B.; Walter, R., Transitioning from federated avionics architectures to integrated modular avionics, DASC’07, vol. 2.A.1, 1-10, (Oct. 2007), IEEE
[39] Wu, W.; Chen, L.; Miné, A.; Dong, D.; Wang, J., Numerical static analysis of interrupt-driven programs via sequentialization, ACM Transactions on Embedded Computing Systems (TECS), 15, 70, 26, (Aug. 2016)
[40] Zhang, H.; Aoki, T.; Chiba, Y., A spin-based approach for checking OSEK/VDX applications, (Formal Techniques for Safety-Critical Systems: Third International Workshop, FTSCS 2014, (2015), Springer), 239-255
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.