Optimale Interprozeduale Analyse von Programmen mit dynamischer Thread-Erzeugung
Final Report Abstract
Ein zentrales Thema des Projekts waren optimale Analysen für Programme mit rekursiven Prozeduren und dynamischer Threaderzeugung. Als Modellformalismus für derartige Programme verwendeten wir sogenannte dynamische Pushdown-Netzwerke (DPNs) und abstrahierten damit von unendlichen Datenbereichen und gemeinsam verwendeten Variablen. Aufbauend auf eigenen Vorarbeiten und Resultaten von Kahlon et al. konnten zunächst optimale Erreichbarkeitsanalysen für DPNs mit wohlgeschachtelt verwendeten Locks entwickelt werden, ein überraschendes und von uns ursprünglich nicht erwartetes Ergebnis, da andere Synchronisations- oder Kommunikationskonzepte zu unentscheidbaren Erreichbarkeitsproblemen führen. Wurden zunächst nur nicht re-entrante Locks und vergleichsweise einfache Erreichbarkeitsprobleme betrachtet, konnten die Verfahren später auch auf re-entrante Locks und Monitore sowie allgemeinere Analysefragestellungen erweitert werden. Auch gewisse Formen von join-Kommandos konnten optimal mitbehandelt werden, was wir ebenfalls urspünglich nicht erwartet hatten. Darüber hinaus haben wir die Entscheidbarkeit grundlegender Analyseprobleme von DPNs mit contextual locking gezeigt, einer von Chadha et al. vorgeschlagenen Lock-Disziplin, die über wohlgeschachtelte Verwendung hinausgeht, und die Komplexität dieser Probleme genauer charakterisiert. Ferner haben wir ein Verfahren entwickelt, das die Stärke der DPN-basierten Analysen für die präzisere Berechnung von Invarianten in parallelen Programmen mit gemeinsamen Variablen (shared state) nutzbar macht. Einige Varianten der DPN-basierten Analyseverfahren wurde implementiert, mithilfe des Wala-Frameworks an die Analyse von Java-Programmen angebunden und in einem experimentellen Analysator für data races verwendet. Ein weiteres wichtiges Thema innerhalb des Projekts war die Frage, inwiefern es möglich ist, exakte Analysen linearer Ungleichungen zu finden. Hier ermöglichte die neue Technik der Strategieiteration einen Durchbruch. Zumindest für muster-basierte Analysen ermöglichen die neuen Verfahren, die exakte kleinste Lösung der zugehörigen Gleichungssysteme auszurechnen. Die Idee der Strategieiteration wurde schließlich zu einer parametrischen Strategieiteration verallgemeinert. Im ganzzahligen Fall kann nun eine Aufteilung des Parameterraums in konvexe Bereiche berechnet werden, innerhalb derer für jedes Template die optimalen Schranken mit Hilfe desselben linearen Ausdrucks beschrieben werden kann. Bei dem Versuch, eine geeignete Infrastruktur zur Einbindung komplexer Analysen in ein Werkzeug zur statischen Analyse zu entwickeln, fiel unser Augenmerk generell auf Fixpunktalgorithmen zur bedarfsgetriebenen Analyse von Programmen. Unsere Untersuchungen zeigten, dass das bisherige Schema einer sukzessiven Iteration in eine Richtung, möglicherweise gefolgt von einer Iteration in die Gegenrichtung aufgegeben werden kann zugunsten einer Iteration, die lokal entscheidet, ob der gegenwärtige Wert vergröbert oder verfeinert werden soll. Als Testumgebung für die neuen Verfahren diente das System Goblint, mit dem nebenläufige C-Programme analysiert werden können. Die neuen Fixpunktalgorithmen ermöglichen, komplexere abstrakte Bereiche bei der Analyse zu verwenden und so die Genauigkeit zu erhöhen. Als besonders ergiebig erwies sich die Untersuchung nebenläufiger C-Programme unter Autosar/Osek. Für diese wurden Analysen für Dataraces sowie der Transaktionalität von Funktionen entwickelt. Wir bemühten uns auch um die Popularisierung unserer Ideen. In einer Veröffentlichung im Spektrum der Informatik werden verschiedene Ansätze zur Programmanalyse vorgestellt und auf ihre jeweiligen Vorzüge hin verglichen.
Publications
- Conflict analysis of programs with procedures, dynamic thread creation, and monitors. In SAS 2008, LNCS 5079, pages 205-220. Springer Verlag, 2008
P. Lammich and M. Müller-Olm
(See online at https://doi.org/10.1007/978-3-540-69166-2_14) - Predecessor sets of dynamic pushdown networks with tree-regular constraints. In CAV 2009, LNCS 5643, pages 525-539. Springer, 2009
P. Lammich, M. Müller-Olm, and A. Wenner
(See online at https://doi.org/10.1007/978-3-642-02658-4_39) - Normalization of linear Horn clauses. In SBMF 2010, LNCS 6527, pages 242-257. Springer Verlag, 2010
T. M. Gawlitza, H. Seidl, and K. N. Verma
(See online at https://doi.org/10.1007/978-3-642-19829-8_16) - Weighted dynamic pushdown networks. In ESOP 2010, LNCS 6012, pages 590- 609. Springer Verlag, 2010
A. Wenner
(See online at https://doi.org/10.1007/978-3-642-11957-6_31) - A decision procedure for detecting atomicity violations for communicating processes with locks. International Journal on Software Tools for Technology Transfer (STTT), 13, 2011
N. Kidd, P. Lammich, T. Touili, and T. Reps
(See online at https://doi.org/10.1007/s10009-010-0159-5) - Fast interprocedural linear two-variable equalities. ACM Trans. Program. Lang. Syst., 33(6):21:1–21:33, 2011
A. Flexeder, M. Müller-Olm, M. Petter, and H. Seidl
(See online at https://dx.doi.org/10.1145/2049706.2049710) - Join-lock-sensitive forward reachability analysis for concurrent programs with dynamic process creation. In VMCAI 2011, LNCS 6538, pages 199-213. Springer Verlag, 2011
T. M. Gawlitza, P. Lammich, M. Müller-Olm, H. Seidl, and A. Wenner
(See online at https://doi.org/10.1007/978-3-642-18275-4_15) - Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol. In POPL 2011, pages 93-104 . ACM, 2011
M. Schwarz, H. Seidl, V. Vojdani, P. Lammich, and M. Müller-Olm
(See online at https://dx.doi.org/10.1145/1925844.1926398) - Contextual Locking for Dynamic Pushdown Networks. In SAS 2013, LNCS 7935, pages 477-498. Springer Verlag, 2013
P. Lammich, M. Müller-Olm, H. Seidl and A. Wenner
(See online at https://doi.org/10.1007/978-3-642-38856-9_25) - Iterable forward reachability analysis of monitordpns. EPTCS 129, pages 384–403, 2013
B. Nordhoff, M. Müller-Olm, and P. Lammich
(See online at https://dx.doi.org/10.4204/EPTCS.129.24) - Parametric Strategy Iteration. In SCSS 2014, EPiC Series in Computing 30, pages 62-76. EasyChair, 2014
H. Seidl, T. M. Gawlitza and M. Schwarz
- Precise Analysis of Value-Dependent Synchronization in Priority Scheduled Programs. In VMCAI 2014, LNCS 8318, pages 21-38. Springer Verlag, 2014
M. Schwarz, H. Seidl, V. Vojdani and K. Apinis
(See online at https://doi.org/10.1007/978-3-642-54013-4_2)
