Im Bereich des High-Performance Computing (HPC) kommt der Parallelisierung von Programmen eine große Bedeutung zu. Die Richtigkeit der Parallelisierung hängt jedoch vom zuverlässigen Ausschluss bestimmter Datenabhängigkeiten ab, beispielsweise von Read-After-Write-Abhängigkeiten, bei denen ein Lesezugriff auf einen Schreibzugriff auf einen bestimmten Speicherort folgt. Es ist zwingend erforderlich, dass Datenabhängigkeitsanalysen nicht nur korrekt, sondern auch so präzise wie möglich sind, um jede Gelegenheit zur Parallelisierung zu nutzen.

Während in der HPC-Community verschiedene statische, dynamische und hybride Analyseansätze vorgeschlagen wurden, basierte keiner auf Programmlogik und deduktiver Verifizierung, trotz der erheblichen Vorteile, die dieser Ansatz bietet, einschließlich Korrektheit, Präzision und Modularität.

In dieser Arbeit stellen wir einen automatischen, korrekten und hochpräzisen Ansatz zur Generierung von Datenabhängigkeiten basierend auf deduktiver Verifizierung vor. Wir definieren eine Programmlogik basierend auf einer präzisen Semantik für Datenabhängigkeiten. Da Schleifen in der Regel die Hauptquelle der Parallelisierung in HPC-Anwendungen sind, statten wir unseren Ansatz mit einer automatischen Technik zur Erzeugung von Schleifeninvarianten in derselben Programmlogik aus. Um eine vollständige Automatisierung zu erreichen, integrieren wir eine Prädikatenabstraktion, die auf die Anforderungen der Datenabhängigkeitsanalyse zugeschnitten ist. Um so viel Präzision wie möglich beizubehalten, verallgemeinern wir die logikbasierte symbolische Ausführung, um abstrakte Datenabhängigkeitsprädikate zu berechnen.

Der vorgestellte Ansatz wurde protptypisch implementiert und zeigt, dass eine vollautomatische Datenabhängigkeitsanalyse auf Basis deduktiver Verifizierung machbar ist und eine vielversprechende Alternative zu den im HPC üblicherweise verwendeten Abhängigkeitsanalysen darstellt. Wir implementierten unseren Ansatz für Java auf einem deduktiven Verifizierungstool und führten Evaluierungen durch, die seine Fähigkeit demonstrierten, hochpräzise Datenabhängigkeiten für repräsentativen Code zu analysieren, der aus HPC-Anwendungen extrahiert wurde.