Skip to content
Menu
Technical University of Munich
Technical University of Munich

Optimale Interprozedurale Analyse von Programmen mit dynamischer Thread-Erzeugung

Bisher wurden im Rahmen des OpIAT Projekts, zusammen mit der Arbeitsgruppe von Prof. Dr. Markus Müller-Olm an der Westfälische Wilhelms-Universtität Münster, Methoden entwickelt, um den Kontrollfluss in nebenläufigen Programmen mit Synchronisationsprimitiven präzise zu analysieren. Dabei ging es einerseits um dynamische Pushdown-Netzwerke (DPNs) mit wohlgeschachtelten Locks oder Monitoren und andererseits um ein vereinfachtes Taskmodell, das dem Automobilstandard OSEK zu Grunde liegt, bei dem unterschiedliche Tasks mit Hilfe von Ressourcen und Prioritäten synchronisiert werden.

Darauf aufbauend sollen nun für diese Programmiermodelle Analyseframeworks entwickelt werden, die es erlauben, weiterreichende Programmeigenschaften statisch zu ermitteln. Insbesondere sollen sowohl für das OSEK-Modell als auch für DPNs Wertanalysen für Programme mit globalen Variablen entwickelt werden. Zur Steigerung der Präzision sollen diese Analysen Synchronisationsprimitive mitberücksichtigen. Neben den schon in der ersten Projektphase betrachteten Synchronisationsprimitiven sollen zudem weitere Synchronisationskonzepte identifiziert werden, die exakt behandelt werden können.

Personen:

Veröffentlichungen:

  • P. Lammich and M. Müller-Olm. Precise fixpoint-based analysis of programs with thread-creation and procedures. CONCUR 2007
  • P. Lammich and M. Müller-Olm. Conflict analysis of programs with procedures, dynamic thread creation, and monitors. SAS 2008
  • M. Müller-Olm and H. Seidl. Upper adjoints for fast inter-procedural variable equalities. ESOP 2008
  • N. Kidd, P. Lammich, T. Touili, and T. Reps. A decision procedure for detecting atomicity violations for communicating processes with locks. SPIN 2009
  • P. Lammich, M. Müller-Olm, and A. Wenner. Predecessor sets of dynamic pushdown networks with tree-regular constraints. CAV 2009
  • T. M. Gawlitza, H. Seidl, and K. N. Verma. Normalization of linear Horn clauses. SBMF 2010
  • A. Wenner. Weighted dynamic pushdown networks. ESOP 2010
  • T. M. Gawlitza, P. Lammich, M. Müller-Olm, H. Seidl, and A. Wenner. Join-lock-sensitive forward reachability analysis for concurrent programs with dynamic process creation. VMCAI 2011
  • M. Schwarz, H. Seidl, V. Vojdani, P. Lammich, and M. Müller-Olm. Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol. POPL 2011
To top