Statische WCET-Analyse ist für komplexe Prozessoren einsetzbar und liefert präzise Resultate [5]. Eine Voraussetzung ist jedoch, dass das Zeitverhalten des Prozessors vorhersagbar ist [6]. Bereits bei Single-Core-Prozessoren wird die Vorhersagbarkeit durch spekulative Hardware-Mechanismen wie Caches, Out-of-Order Pipelining oder Sprungvorhersage-Mechanismen beeinträchtigt. Wird eine Task T1 auf einem Prozessor mit Caches von einer anderen Task unterbrochen, können von T1 benötigte Speicherblöcke aus dem Cache verdrängt werden. Wird T1 nach der Unterbrechung fortgesetzt, können dadurch zusätzliche Cache Misses auftreten. Eine Berücksichtigung aller möglichen Unterbrechungsszenarien ist unmöglich durch Messungen zu realisieren. Cache-bezogene Unterbrechungskosten können von statischen Analysen wie aiT berücksichtigt werden, aber der Unterschied zwischen durchschnittlicher und maximaler Ausführungszeit wächst. Durch Cache-Partitionierung oder Cache Locking lässt sich die Vorhersagbarkeit verbessern; die mögliche Varianz der Ausführungszeit sinkt. An diesem Beispiel wird deutlich, dass durch Zugriffe auf gemeinsam genutzte Hardware-Ressourcen Interferenzen entstehen können, die die Vorhersagbarkeit beeinträchtigen, da die Abfolge der Zugriffe stark variieren kann.
Bei Multicore-Prozessoren sind nicht nur die Interferenzen innerhalb der einzelnen Cores zu berücksichtigen; hinzukommen sind nun auch Interferenzen durch Zugriffe auf gemeinsam genutzte Ressourcen von unterschiedlichen Cores. Greifen mehrere Cores auf denselben Cache zu und läuft auf jedem Core ein separater Scheduler, kann die Ausführungszeit einer Task auch durch eine völlig andere Applikation beeinflusst werden, die auf einem anderen Core läuft und nicht der Steuerung desselben Scheduler untersteht. Da verschiedene Applikationen meist erst in der Integrationsphase gemeinsam betrachtet werden können, besteht zudem die Gefahr, dass Timing-Probleme erst sehr spät erkannt werden.
Bild 2 zeigt den Nachweis der Abwesenheit von Laufzeitfehlern und Race Conditions mit Hilfe von Astrée. Astrée ist eine Software zur statischen Programmanalyse, die C-Programme automatisch auf Laufzeitfehler überprüft. Astrée analysiert handgeschriebene oder automatisch erzeugte C-Programme mit komplexer Speichernutzung, aber ohne Rekursion oder dynamische Speicherallokation. Damit bietet sich Astrée vor allem zur Analyse von sicherheitskritischen eingebetteten Anwendungen an, insbesondere in den Bereichen Transport, Medizintechnik, Nuklearanlagen, Luft- und Raumfahrt. Astrée überprüft, ob die C-Sprache korrekt eingesetzt wurde, und sucht nach Laufzeitfehlern in allen möglichen Ausführungsszenarien unter allen möglichen Bedingungen. Dabei meldet es jeden Gebrauch der Sprache, der laut ISO/IEC 9899:1999, der internationalen Norm für C, ein undefiniertes Verhalten aufweist, sowie jeden Verstoß gegen Hardware-spezifische Einschränkungen der Implementierung. Im Einzelnen meldet Astrée Division durch Null, Feldzugriffe außerhalb der gültigen Feldgrenzen, ungültige Zeigermanipulationen und -dereferenzierungen (NULL-Zeiger, uninitialisierte und hängende Zeiger), ganzzahlige arithmetische Überläufe und Gleitkommaüberläufe, Verstöße gegen optionale benutzerdefinierte Annahmen zur Überprüfung von sonstigen Laufzeiteigenschaften (ähnlich der „assert“-Diagnostik), garantiert unerreichbaren Code sowie Lesezugriffe auf uninitialisierte Variablen. Gleitkommaberechnungen werden von Astrée präzise und sicher behandelt. Alle möglichen Rundungsfehler werden stets berücksichtigt.
Caches mit Konfliktpotenzial
Die Gewährleistung von Zeitschranken auf Multicore-Prozessoren wurde in zahlreichen nationalen und internationalen Forschungsprojekten untersucht – Beispiele sind Predator, Certainty oder Aramis. Dennoch stehen dem Einsatz von Multicore-Systemen in sicherheitskritischen Anwendungen auch heute noch Hürden entgegen, die in einem 2014 veröffentlichten Report der Luftfahrtsicherheitsbehörden zusammengefasst werden [7]. Aktuelle Multicore-Designs wurden nicht im Hinblick auf vorhersagbare Rechenleistung entwickelt. Konflikte können z.B. bei Zugriffen auf gemeinsame Caches, aber auch auf gemeinsame Speicherbänke oder gemeinsame Flash Prefetch Buffers auftreten. Für eine gegebene Multicore-Architektur müssen mögliche Interferenzen sorgfältig untersucht und eine Konfiguration bestimmt werden, die eine vorhersagbare Ausführung ermöglicht.
In [6] werden Konfigurationsbeispiele für zwei aktuelle Multicore-Prozessoren gegeben, die eine vorhersagbare Rechenleistung zulassen. Zu den Konfigurierungsmaßnahmen zählen die exklusive Zuordnung einzelner Speicherbänke oder Prefetch Buffers zu bestimmten Cores oder die Verwendung eines gemeinsamen L2-Cache als Scratchpad für einen einzelnen Core. Sind mehrere Cores durch ein gemeinsames Bussystem an den Hauptspeicher angebunden, müssen die Aktivitäten zwischen den Cores koordiniert werden, um Zugriffskonflikte zu kontrollieren [8]. Der Nachweis des korrekten Zeitverhaltens von Echtzeitsystemen ist von entscheidender Bedeutung für die Systemkorrektheit. Statische Analysatoren auf Basis der abstrakten Interpretation liefern garantierte obere Schranken für die Ausführungszeit von Tasks. Statische Analyseverfahren werden von aktuellen Sicherheitsstandards empfohlen. Bei Multicore-Architekturen für sicherheitskritische Echtzeitsysteme muss die Hardware sorgfältig im Hinblick auf vorhersagbare Performance untersucht und geeignet konfiguriert werden, um Integrations- und Stabilitätsprobleme zu vermeiden.
Literatur
[1] Kästner, D.: Applying Abstract Interpretation to Demonstrate Functional Safety. In Boulanger, J.-L., editor, Formal Methods Applied to Industrial Complex Systems, ISTE/Wiley, London, UK, 2014.
[2] Kästner, D.; Ferdinand, C.: Proving the Absence of Stack Overflows. Proceedings of the 33th International Conference on Computer Safety, Reliability and Security (SAFECOMP), Florence, 2014. Springer LNCS 8666, Springer, Heidelberg.
[3] 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. Embedded Real Time Software and Systems Congress ERTS², Toulouse, 2010.
[4] www.absint.com/ait.
[5] Souyris,J.; Le Pavec,E.; Himbert,G.; Jégu,V.; Borios,G.; Heckmann,R.: Computing the worst case execution time of an avionics program by abstract interpretation. Proceedings of the WCET Workshop, 2005.
[6] Cullmann,C.; Ferdinand,C.; Gebhard,G.; Grund,D.; Burguière,C.; Reineke,J.; Triquet,B.; Wegener,S.; Wilhelm,R.: Predictability Considerations in the Design of Multi-Core Embedded Systems. Ingénieurs de l‘Automobile, volume 807, 2010.
[7] Certification Authorities Software Team (CAST). Position Paper CAST-32: Multi-core Processors. 2014. www.faa.gov/aircraft/air_cert/design_approvals/air_software/cast/cast_papers/media/cast-32.pdf.
[8] Nowotsch,J.; Paulitsch,M.; Bühler,D.; Theiling,H.; Wegener,S.; Schmidt,M.: Multi-core Interference-Sensitive WCET Analysis Leveraging Runtime Resource Capacity Enforcement. 26th Euromicro Conference on Real-Time Systems (ECRTS² 2014).
Der Autor
Dr. Daniel Kästner |
---|
arbeitet als CTO bei der AbsInt GmbH in Saarbrücken. |
kaestner@absint.com