Verifikationsherausforderungen bei der Multiplikation von Sparse-Matrix-Vektoren im High-Performance-Computing: Teil I

Grundinformationen

• Paper-ID: 2510.13427
• Titel: Verification Challenges in Sparse Matrix Vector Multiplication in High Performance Computing: Part I
• Autor: Junchao Zhang (Argonne National Laboratory)
• Klassifizierung: cs.LO cs.DC cs.MS
• Veröffentlichungskonferenz: International Workshop on Verification of Scientific Software (VSS 2025)
• Veröffentlichungsinformationen: EPTCS 432, 2025, S. 98–105
• Paper-Link: https://arxiv.org/abs/2510.13427

Zusammenfassung

Die Multiplikation von Sparse-Matrix-Vektoren (SpMV) ist ein fundamentaler Kernel in wissenschaftlichen Codes, die auf iterative Löser angewiesen sind. In diesem ersten Teil unserer Arbeit präsentieren wir sowohl eine sequenzielle als auch eine grundlegende MPI-parallele Implementierung von SpMV, um ein Herausforderungsproblem für die Verifikationsgemeinschaft wissenschaftlicher Software bereitzustellen. Die Implementierungen werden im Kontext der PETSc-Bibliothek beschrieben.

Forschungshintergrund und Motivation

Problemdefinition

Diese Forschung befasst sich mit Softwareverifikationsherausforderungen bei der Multiplikation von Sparse-Matrix-Vektoren (SpMV) im High-Performance-Computing. SpMV ist die Kernoperation zur Lösung von dünnbesetzten linearen Gleichungssystemen Ax=b und wird weit verbreitet in wissenschaftlichen Rechencodes verwendet, die auf iterativen Lösern basieren, insbesondere in großskaligen Krylov-Unterraum-Methoden.

Bedeutung

1. Grundlegender Charakter: SpMV ist ein fundamentaler Kernalgorithmus der wissenschaftlichen Berechnung, dessen Korrektheit die Zuverlässigkeit von Anwendungen auf höherer Ebene direkt beeinflusst
2. Komplexität: Obwohl die mathematische Definition einfach ist (yi = Σ(aij·xj)), machen Speicherformate, Datenverteilung, Parallelisierung und Optimierung die Implementierung komplex
3. Verifikationsherausforderungen: Vorhandene hochoptimierte Implementierungen stellen erhebliche Herausforderungen für die Softwareverifikation dar

Einschränkungen bestehender Methoden

• Die PETSc-Bibliothek enthält hochoptimierte MPI-parallele SpMV-Implementierungen, aber deren Komplexität macht die Verifikation schwierig
• Es fehlen standardisierte Herausforderungsprobleme, die speziell für die Verifikationsgemeinschaft wissenschaftlicher Software konzipiert sind

Forschungsmotivation

Bereitstellung eines strukturierten Herausforderungsproblems für die Verifikationsgemeinschaft wissenschaftlicher Software durch Bereitstellung von SpMV-Implementierungen mit zunehmender Komplexität, um die Entwicklung und Bewertung von Verifikationswerkzeugen und -methoden zu unterstützen.

Kernbeiträge

1. Bereitstellung eines standardisierten Verifikationsherausforderungsproblems: Entwurf standardisierter Testfälle für SpMV für die Verifikationsgemeinschaft wissenschaftlicher Software
2. Implementierung von zwei SpMV-Algorithmen unterschiedlicher Komplexität:
   • Sequenzielle Implementierung (seq.c)
   • Grundlegende MPI-parallele Implementierung (mpibasic.c)
3. Etablierung eines vollständigen Verifikationsrahmens: Einschließlich Eingabedatengenerierung, Korrektheitsprüfung und Fehlererkennung
4. Klare Definition von Verifikationszielen: Bereitstellung spezifischer Verifikationsanforderungen und Herausforderungen für jede Implementierung

Methodische Details

Aufgabendefinition

Eingabe:

• Sparse-Matrix A (M×N, NNZ Nicht-Null-Elemente), im CSR-Format gespeichert
• Vektor x (N-dimensional)
• Erwartetes Ergebnis z = Ax (M-dimensional)

Ausgabe:

• Berechnetes Ergebnis y = Ax
• Korrektheitsprüfung: ||y-z||² sollte 0 sein (unter Berücksichtigung von Gleitkomma-Rundungsfehlern)

Einschränkungen:

• Verwendung des Compressed Sparse Row (CSR)-Formats
• Unterstützung für MPI-parallele verteilte Berechnung

Datenstrukturdesign

CSR-Format-Darstellung

Die Sparse-Matrix A wird durch drei Arrays dargestellt:

• a[nnz]: Speichert Werte von Nicht-Null-Elementen
• j[nnz]: Speichert Spaltenindizes von Nicht-Null-Elementen
• i[m+1]: Zeilenzeiger, ik zeigt auf die Startposition der k-ten Zeile in a und j

Datentypdefinition

// Sequenzielle Version
typedef struct {
    int m, n;        // Matrixdimensionen
    int *i, *j;      // CSR-Format-Indizes
    double *a;       // Werte von Nicht-Null-Elementen
} Mat;

// MPI-parallele Version
typedef struct {
    int m, n, M, N;  // Lokale und globale Dimensionen
    int rstart, cstart; // Startzeilen- und Spaltenindizes
    int *i, *j;
    double *a;
} Mat;

Algorithmus-Implementierung

Sequenzielle Implementierung

for (i = 0; i < A.m; i++) {
    y.a[i] = 0.0;
    for (j = A.i[i]; j < A.i[i + 1]; j++)
        y.a[i] += A.a[j] * x.a[A.j[j]];
}

MPI-parallele Implementierung

1. Datenverteilungsstrategie:
   • Matrix wird zeilenweise blockweise verteilt: m = M/size + (M%size > rank ? 1 : 0)
   • Vektor x wird spaltenweise verteilt: n = N/size + (N%size > rank ? 1 : 0)
2. Kommunikationsmuster:
   • Verwendung von MPI_Allgather oder MPI_Allgatherv zur Erfassung des vollständigen Vektors x
   • Verwendung von MPI_Allreduce zur Berechnung der globalen Norm
3. Berechnungsablauf:
   • Berechnung des lokalen Matrixlayouts (rstart, cstart)
   • Extraktion lokaler Daten aus globalen Arrays
   • Erfassung des verteilten Vektors x in eine lokale vollständige Kopie X
   • Durchführung der lokalen SpMV-Berechnung
   • Berechnung der lokalen Fehlernorm und globale Reduktion

Technische Innovationen

1. Progressives Komplexitätsdesign: Von einfacher sequenzieller bis zu grundlegender paralleler Implementierung für progressive Werkzeugtests
2. Standardisierte Verifikationsschnittstelle: Einheitliches Ein- und Ausgabeformat sowie Korrektheitsprüfmechanismus
3. Praktischer Anwendungshintergrund: Basierend auf echten Implementierungsmustern der PETSc-Bibliothek mit praktischem Wert
4. Erweiterbares Framework: Grundlage für zukünftige komplexere optimierte Versionen (Teil II)

Experimentelle Einrichtung

Datensätze

• Matrixgröße: 32×36-Matrix mit 50 Nicht-Null-Elementen
• Datengenerierung: Verwendung des begleitenden Python-Skripts csr.py zur Generierung von Testdaten
• Hardcodierte Eingaben: Zur Vereinfachung der Verwendung sind Testdaten direkt in den Quellcode eingebettet
• Anpassbarkeit: Benutzer können Python-Skriptparameter ändern, um verschiedene Testfälle zu generieren

Bewertungsmetriken

• Korrheitsprüfung: Berechnung der quadrierten Norm ||y-z||²
• Erfolgskriterium: Norm ≤ 1e-6 (unter Berücksichtigung von Gleitkomma-Rundungsfehlern)
• Rückgabecodes: Rückgabe von 0 bei Korrektheit, Nicht-Null-Wert bei Fehler

Implementierungsdetails

• Programmiersprache: C
• Parallel-Framework: MPI
• Kompilierungsanforderungen: Nur C-Compiler oder MPI-Compiler erforderlich
• Code-Verfügbarkeit: Öffentlich verfügbar im GitHub-Repository

Experimentelle Ergebnisse

Verifikationsziele

Verifikationsanforderungen für sequenzielle Implementierung

Verifikation, dass das berechnete Ergebnis y erfüllt: yi = Σ(aij·xj), wobei aij, die nicht in der CSR-Darstellung gespeichert sind, als 0 behandelt werden

Verifikationsanforderungen für MPI-parallele Implementierung

1. Layout-Korrektheit: Verifikation, dass Σm = M, Σn = N
2. Lokale Berechnungskorrektheit: Verifikation, dass y auf jedem Prozess das korrekte Produkt der entsprechenden lokalen Submatrix und des vollständigen Vektors x ist

Testfälle

Das Paper stellt konkrete Testdaten bereit:

• Eingabematrix: 32×36 Sparse-Matrix (50 Nicht-Null-Elemente)
• Eingabevektor: 36-dimensionaler Vektor
• Erwartete Ausgabe: 32-dimensionaler Ergebnisvektor
• Alle Daten werden als Ganzzahl- und Gleitkomma-Arrays bereitgestellt

Verwandte Arbeiten

Verwandte Forschungsgebiete

1. Krylov-Unterraum-Methoden: SpMV ist die Kernkomponente iterativer Löser
2. PETSc-Bibliothek: Bietet umfangreiche Krylov-Methoden und SpMV-Implementierungen
3. Verifikation wissenschaftlicher Software: Korrektheitsprüfung von High-Performance-Wissenschaftssoftware

Positionierung dieses Papers

• Füllt die Lücke fehlender standardisierter SpMV-Verifikationsherausforderungen in der Verifikationsgemeinschaft
• Bietet Referenzbasis für Verifikation komplexer optimierter Implementierungen
• Verbindet theoretische Verifikationsmethoden mit praktischen HPC-Anforderungen

Schlussfolgerungen und Diskussion

Hauptschlussfolgerungen

1. Erfolgreiche Etablierung standardisierter Verifikationsherausforderungsprobleme für SpMV-Software
2. Bereitstellung von zwei Implementierungen unterschiedlicher Komplexität, geeignet für progressive Werkzeugtests
3. Basierend auf echten PETSc-Bibliotheksmustern mit praktischem Anwendungswert

Einschränkungen

1. Skalierungsbeschränkung: Aktuelle Testfälle haben begrenzte Größe (32×36-Matrix)
2. Fehlende Optimierungen: Grundlegende MPI-Implementierung enthält nicht die komplexen Optimierungen in echten Produktionsumgebungen
3. Verifikationsumfang: Deckt nur grundlegende Korrektheit ab, nicht Leistungs- und numerische Stabilitätsprüfung

Zukünftige Richtungen

1. Teil-II-Entwicklung: Geplante Bereitstellung komplexerer optimierter MPI-Implementierungen in nachfolgenden Arbeiten
2. Erweiterte Testfälle: Hinzufügung größerer Maßstäbe und verschiedener Sparse-Muster-Testmatrizen
3. Verifikationswerkzeug-Integration: Integration mit bestehenden Verifikationswerkzeugen

Tiefgreifende Bewertung

Stärken

1. Hoher praktischer Wert: Löst tatsächliche Anforderungen der Verifikationsgemeinschaft wissenschaftlicher Software
2. Vernünftiges Design: Progressives Komplexitätsdesign erleichtert Werkzeugentwicklung und Tests
3. Hoher Standardisierungsgrad: Bietet vollständige Ein-/Ausgabespezifikationen und Korrheitsprüfmechanismen
4. Starke Reproduzierbarkeit: Code ist öffentlich verfügbar, Testdaten sind eingebettet, leicht zu reproduzieren
5. Praktischer Hintergrund: Basierend auf weit verbreiteter PETSc-Bibliothek mit echtem Anwendungswert

Mängel

1. Mangel an theoretischer Analyse: Keine Algorithmus-Komplexitätsanalyse oder theoretische Eigenschaftsdiskussion
2. Begrenzte Testabdeckung: Nur ein einzelner Testfall bereitgestellt, unzureichende Vielfalt
3. Oberflächliche Verifikation: Konzentriert sich hauptsächlich auf funktionale Korrektheit, mangelnde numerische Genauigkeit und Grenzwertanalyse
4. Leistungsaspekte nicht berücksichtigt: Keine leistungsbezogenen Verifikationsherausforderungen

Auswirkungen

1. Feldbeitrag: Bietet wichtige standardisierte Testplattform für wissenschaftliche Softwareverifikation
2. Praktischer Wert: Kann direkt zur Entwicklung und Bewertung von Verifikationswerkzeugen verwendet werden
3. Erweiterbarkeit: Legt Grundlage für nachfolgende komplexere Implementierungen
4. Gemeinschaftswert: Fördert Zusammenarbeit zwischen HPC- und Verifikationsgemeinschaften

Anwendungsszenarien

1. Werkzeugentwicklung: Als standardisierte Testfälle zur Validierung von Werkzeugeffektivität
2. Lehranwendungen: Geeignet als Lehrfall für paralleles Rechnen und Softwareverifikation
3. Benchmark-Tests: Kann als Referenzbenchmark für SpMV-Implementierungskorrektheit dienen
4. Forschungsplattform: Bietet standardisierte Plattform für verwandte Algorithmen- und Optimierungsforschung

Literaturverzeichnis

1. S Balay et al. (2025): PETSc/TAO Users Manual. Technical Report ANL-21/39 - Revision 3.23, Argonne National Laboratory
2. Yousef Saad (2003): Iterative Methods for Sparse Linear Systems, second edition. Society for Industrial and Applied Mathematics

Gesamtbewertung: Dies ist eine praktisch sehr wertvolle Arbeit, die zwar begrenzte theoretische Innovationen bietet, aber der Verifikationsgemeinschaft wissenschaftlicher Software dringend benötigte standardisierte Herausforderungsprobleme bereitstellt. Das Paper hat klare Struktur, vollständige Implementierung und gute Reproduzierbarkeit sowie Erweiterbarkeit und hat wichtigen Wert für die Förderung der Entwicklung im HPC-Softwareverifikationsbereich.