Formale Verifikation der COO-zu-CSR-Konvertierung von Sparse Matrices (Eingeladenes Papier)

Grundinformationen

• Papier-ID: 2510.13412
• Titel: Formal Verification of COO to CSR Sparse Matrix Conversion (Invited Paper)
• Autor: Andrew W. Appel (Princeton University)
• Klassifizierung: math.NA cs.LO cs.NA
• Veröffentlichungszeit/Konferenz: VSS 2025 (International Workshop on Verification of Scientific Software), EPTCS 432, 2025
• Papierlink: https://arxiv.org/abs/2510.13412

Zusammenfassung

Dieses Papier beschreibt einen maschinell überprüften Korrektheitsbeweis zur Verifikation eines C-Programms, das Sparse Matrices im Koordinatenformat (COO) in das komprimierte Sparse-Row-Format (CSR) konvertiert. Der klassische Algorithmus (Sortierung von COO-Einträgen nach lexikographischer Ordnung von Zeilen und Spalten; Füllung der CSR-Arrays von links nach rechts) ist zwar prägnant, weist jedoch erheblich komplexe Invarianten auf. Der Artikel präsentiert eine Bottom-up-Methodik zur Ableitung von Invarianten aus dem Programm.

Forschungshintergrund und Motivation

Problemdefinition

1. Kernproblem: Sparse Matrices werden in der numerischen Berechnung weit verbreitet verwendet, aber bestehende Sparse-Matrix-Konvertierungsalgorithmen mangelt es an formaler Verifikation, was zu schwer zu findenden Fehlern führen kann
2. Bedeutung: Die Sparse-Matrix-Vektor-Multiplikation ist eine grundlegende Operation in numerischen Methoden; fehlerhafte Konvertierungen führen zum Versagen der gesamten Berechnungskette
3. Bestehende Einschränkungen: Traditionelle Verifikationsmethoden verlassen sich auf Regressionstests und ähnliche Mittel und können keine mathematische Korrektheit garantieren
4. Forschungsmotivation: Durch maschinell überprüfte formale Beweise die absolute Korrektheit der COO-zu-CSR-Konvertierung sicherstellen und damit eine Grundlage für verifizierbare numerische Software schaffen

Anwendungshintergrund

• Sparse-Matrix-Darstellung: COO-Format ist konstruktionsfreundlich, CSR-Format ist multiplikationsfreundlich
• Finite-Element-Analyse: Jeder innere Knoten in einem Netz erzeugt mehrere Koordinaten-Tupel und produziert natürlicherweise doppelte Einträge
• Numerische Genauigkeit: Die Nichtassoziativität von Gleitkommaoperationen macht die Summationsreihenfolge doppelter Einträge auswirkungsreich auf das Ergebnis

Kernbeiträge

1. Erstmals maschinell überprüfter Korrektheitsbeweis für COO-zu-CSR-Konvertierung: Verwendung des Verifiable Software Toolchain (VST) und des Coq-Beweisassistenten
2. Innovative Methodik zur Ableitung von Schleifeninvarianten: Vorschlag einer Bottom-up-Methodik, die komplexe Schleifeninvarianten aus den Eigenschaften ableitet, die das Programm erfüllen muss
3. Trennung von Datenstruktur- und Approximationslogik: Trennung der Datenstrukturlogik von C-Programmen von der Gleitkomma-Approximationslogik zur Vereinfachung der Verifikationskomplexität
4. Zusammensetzbare Verifikationskomponenten: Bereitstellung eines verifizierten Sparse-Matrix-Konvertierungsmoduls, das in größeren Verifikationssystemen wiederverwendet werden kann
5. Praktische Fehlererkennung: Entdeckung und Behebung von 5 Programmfehlern während des Beweisprozesses (4 Off-by-one-Fehler und 1 Fehler bei der Behandlung von vorzeichenlosen Ganzzahlen)

Methodische Details

Aufgabendefinition

Eingabe: COO-Sparse-Matrix – enthält Dimensionen rows×cols und n Koordinaten-Tripel (row_indk, col_indk, valk) Ausgabe: CSR-Sparse-Matrix – enthält drei eindimensionale Arrays (val, col_ind, row_ptr) Einschränkungen: Beibehaltung der mathematischen Matrix-Semantik, korrekte Behandlung der Gleitkomma-Summation doppelter Einträge

Kernalgorithmus

struct csr_matrix *coo_to_csr_matrix(struct coo_matrix *p) {
    // 1. Sortierung von COO-Einträgen nach (Zeile, Spalte) lexikographischer Ordnung
    coo_quicksort(p, 0, n);
    
    // 2. Zählung der Anzahl eindeutiger Koordinatenpaare
    k = coo_count(p);
    
    // 3. Speicherallokation für CSR-Arrays
    // 4. Durchlaufen der sortierten COO-Einträge, Konstruktion der CSR-Struktur
    for (i=0; i<n; i++) {
        // Behandlung doppelter Einträge, neuer Spalten, neuer Zeilen usw.
    }
}

Architektur der formalen Spezifikation

1. Definition mathematischer Objekte

Record coo_matrix (t: type) := {
    coo_rows: Z;
    coo_cols: Z;
    coo_entries: list (Z * Z * ftype t)
}.

Record csr_matrix {t: type} := {
    csr_cols: Z;
    csr_vals: list (ftype t);
    csr_col_ind: list Z;
    csr_row_ptr: list Z;
    csr_rows: Z := Zlength (csr_row_ptr) - 1
}.

2. Speicherdarstellungsrelation

• coo_rep (sh: share) (coo: coo_matrix Tdouble) (p: val) : mpred
• csr_rep (sh: share) (csr: csr_matrix Tdouble) (p: val) : mpred

3. Matrix-Semantikrelation

Definition coo_to_matrix {t: type} (coo: coo_matrix t) (m: matrix t) : Prop :=
    coo_rows coo = matrix_rows m ∧
    matrix_cols m (coo_cols coo) ∧
    ∀ i j, sum_any (Liste doppelter Einträge) (matrix_index m i j).

Technische Innovationen

1. Nichtdeterministische Modellierung der Gleitkomma-Summation

Inductive sum_any {t}: list (ftype t) → ftype t → Prop :=
| Sum_Any_0: sum_any nil (Zconst t 0)
| Sum_Any_1: ∀ x, sum_any [x] x  
| Sum_Any_split: ∀ al bl a b, sum_any al a → sum_any bl b →
    sum_any (al++bl) (BPLUS a b)
| Sum_Any_perm: ∀ al bl s, Permutation al bl → sum_any al s → sum_any bl s.

2. Definition partieller CSR-Relationen

Die Schlüsselinnovation ist die partial_CSR i r coo ROWPTR COLIND VAL-Relation, die den partiellen CSR-Zustand bei der Verarbeitung des i-ten COO-Eintrags und der r-ten Zeile darstellt.

3. Systematische Ableitung von Schleifeninvarianten

Durch Analyse kritischer Zustandsübergangspunkte im Programm werden systematisch erforderliche Invarianteneigenschaften abgeleitet:

• partial_CSR_0: Initialzustand
• partial_CSR_duplicate: Behandlung doppelter Einträge
• partial_CSR_newcol: Neue Spalteneintrag
• partial_CSR_newrow: Neue Zeileneintrag
• partial_CSR_skiprow: Überspringen leerer Zeilen

Experimentelle Einrichtung

Verifikations-Toolchain

• Coq-Beweisassistent: Für formale Spezifikation und Beweise
• Verifiable Software Toolchain (VST): Für Hoare-Logik-Verifikation von C-Programmen
• Verifiable C: Programmlogik in VST, eingebettet in Coq

Verifikationsumfang

• Definitionen und Lemmata: 1571 Zeilen Coq-Code für Definitionen und Eigenschaften von coo_csr und partial_CSR
• VST-Beweis: 412 Zeilen für den Hauptbeweis der Hoare-Logik
• Vertrauensbasis: Kernspezifikation etwa 39 Zeilen, kritische Teile erfordern manuelle Überprüfung

Verifikationsmethode

1. Schichtweise Verifikation: Zunächst Beweis, dass C-Programm Low-Level-Spezifikation implementiert, dann Beweis der mathematischen Korrektheit der Low-Level-Spezifikation
2. Modulares Design: Trennung von Datenstrukturlogik und Gleitkomma-Approximationslogik
3. Bottom-up-Ableitung: Rückwärts-Ableitung von Schleifeninvarianten aus Anforderungen des Hoare-Logik-Beweises des Programms

Experimentelle Ergebnisse

Hauptergebnisse

1. Vollständiger Korrektheitsbeweis: Erfolgreicher Beweis der vollständigen Korrektheit der COO-zu-CSR-Konvertierung
2. Fehlererkennung: Entdeckung von 5 tatsächlichen Fehlern während der Verifikation:
   • 4 Off-by-one-Fehler
   • 1 komplexer Fehler bei der Initialisierung der vorzeichenlosen Ganzzahl r auf -1
3. Zusammensetzbarkeit: Verifiziertes Modul kann mit anderen verifizierten Sparse-Matrix-Operationen kombiniert werden

Verifikationsabdeckung

• Funktionsspezifikation: Vollständige Vor- und Nachbedingungen
• Schleifeninvarianten: Komplexe Invarianten für drei verschachtelte Schleifen
• Speichersicherheit: Sicherheit von Array-Grenzen und Speicherallokation
• Mathematische Korrektheit: Beibehaltung der Matrix-Semantik

Leistungsmerkmale

• Kompilierzeit-Verifikation: Keine Laufzeit-Overhead
• Vertrauenswürdigkeit: Maschinell überprüfter Beweis basierend auf Coq-Kern
• Wartbarkeit: Modulares Spezifikationsdesign ermöglicht nachfolgende Änderungen und Erweiterungen

Verwandte Arbeiten

Formale Verifikation

1. Verifikation numerischer Software: Dieses Papier ist ein wichtiger Fall für End-to-End-Verifikation numerischer Algorithmen
2. VST-Toolchain: Erweiterung des bestehenden C-Programm-Verifikationsrahmens auf Sparse-Matrix-Anwendungen
3. Gleitkomma-Verifikation: Integration mit Tools wie VCFloat2 zur Behandlung von Gleitkomma-Genauigkeitsanalyse

Sparse-Matrix-Algorithmen

1. Klassische Algorithmen: COO-zu-CSR-Konvertierung ist ein Standard-Algorithmus seit Jahrzehnten
2. Numerische lineare Algebra: Konsistent mit Algorithmen aus klassischen Literaturwerken wie Templates for Linear Systems
3. Hochleistungsrechnen: Bereitstellung grundlegender Komponenten für verifizierbare wissenschaftliche Computersoftware

Programmverifikationsmethodik

1. Ableitung von Schleifeninvarianten: Die vorgeschlagene Bottom-up-Methode hat allgemeine Anwendbarkeit
2. Separationslogik: Effektive Behandlung komplexer Speicherdatenstrukturen
3. Spezifikations-Engineering: Demonstration von Spezifikationsdesign-Prinzipien für große Verifikationsprojekte

Schlussfolgerungen und Diskussion

Hauptschlussfolgerungen

1. Machbarkeitsbeweis: Vollständige formale Verifikation komplexer numerischer Algorithmen ist machbar
2. Methodologischer Beitrag: Die Bottom-up-Methode zur Ableitung von Invarianten hat breite Anwendbarkeit
3. Praktischer Wert: Von der Verifikation entdeckte tatsächliche Fehler beweisen den Wert formaler Methoden
4. Infrastruktur: Grundlage für großflächigere Verifikation wissenschaftlicher Computersoftware

Einschränkungen

1. Bit-für-Bit-Reproduzierbarkeit: Aktuelle Spezifikation erlaubt unterschiedliche Gleitkomma-Summationsreihenfolgen, garantiert keine Bit-Level-Reproduzierbarkeit
2. Leistungsüberlegungen: Verifizierter Algorithmus ist nicht für Leistung optimiert
3. Reassembly-Funktionalität: Optimierte Version mit CSR-Struktur-Wiederverwendung nicht implementiert
4. Verifikationskosten: Relativ kurzes Programm erfordert erhebliche Verifikationsarbeit

Zukünftige Richtungen

1. Stärkere Spezifikation: Spezifikationsversion mit Unterstützung für Bit-für-Bit-Reproduzierbarkeit
2. Leistungsoptimierung: Verifikation hochperformanter Varianten von Sparse-Matrix-Algorithmen
3. Größere Systeme: Integration dieses Moduls in vollständige PDE-Solver-Verifikation
4. Automatisierung: Entwicklung besserer Tools zur Unterstützung der automatischen Ableitung von Schleifeninvarianten

Tiefgreifende Bewertung

Stärken

1. Technische Tiefe: Behandlung mehrerer technischer Herausforderungen in Sparse-Matrix-Algorithmen, einschließlich Gleitkommaoperationen, Speicherverwaltung, komplexer Kontrollfluss
2. Methodologische Innovation: Bottom-up-Methode zur Ableitung von Invarianten bietet replizierbares Paradigma für ähnliche Verifikationen
3. Praktischer Wert: Entdeckung tatsächlicher Fehler beweist praktischen Nutzen formaler Verifikation
4. Engineering-Qualität: Modulares Design und klare Spezifikationsstruktur zeigen hochwertige Verifikations-Engineering
5. Vollständigkeit: End-to-End-Verifikation von C-Code bis zur mathematischen Spezifikation

Schwächen

1. Verifikationskosten: 1983 Zeilen Verifikationscode für relativ kurzes C-Programm, hohe Kosten
2. Generalisierbarkeitsbeschränkungen: Spezialisiert auf COO-zu-CSR-Konvertierung, begrenzte Verallgemeinerungsfähigkeit
3. Unzureichende Leistungsüberlegungen: Keine Berücksichtigung von Leistungsoptimierungen in praktischen Anwendungen
4. Tool-Abhängigkeit: Hohe Abhängigkeit von VST- und Coq-Ökosystem

Einfluss

1. Akademischer Beitrag: Wichtige Fallstudie und Methodik für Verifikation numerischer Software
2. Praktischer Einfluss: Kann als Grundkomponente für hochzuverlässige wissenschaftliche Computersoftware dienen
3. Methodologie-Verbreitung: Methode zur Ableitung von Schleifeninvarianten anwendbar auf Verifikation anderer komplexer Algorithmen
4. Tool-Entwicklung: Förderung der Anwendung von VST und ähnlichen Verifikations-Tools im numerischen Rechnen

Anwendungsszenarien

1. Kritische wissenschaftliche Berechnungen: Numerische Simulationen und Analysen mit hohem Zuverlässigkeitsanforderungen
2. Sicherheitskritische Systeme: Sicherheitskritische Software mit numerischen Berechnungskomponenten
3. Verifikationsforschung: Referenzfall für formale Verifikation komplexer Algorithmen
4. Bildungszwecke: Demonstration der Fähigkeiten und Methoden moderner Programmverifikation

Literaturverzeichnis

Wichtige Literaturquellen dieses Papiers umfassen:

1. Barrett et al. (1994): Templates for the Solution of Linear Systems – Klassische Referenz für Sparse-Matrix-Algorithmen
2. Appel & Kellison (2024): VCFloat2 – Tool zur Gleitkomma-Fehleranalyse
3. Cao et al. (2018): VST-Floyd – Verifikations-Tool für Separationslogik
4. Kellison et al. (2023): LAProof – Formale Beweis-Bibliothek für lineare Algebra-Programme

Zusammenfassung: Dieses Papier demonstriert die Machbarkeit vollständiger formaler Verifikation komplexer numerischer Algorithmen, präsentiert praktische Verifikationsmethodik und leistet wichtige Beiträge zur Entwicklung vertrauenswürdiger wissenschaftlicher Computersoftware. Obwohl die Verifikationskosten erheblich sind, machen der Wert der Fehlererkennung und die bereitgestellte methodologische Anleitung dies zu einem wichtigen Werk in diesem Bereich.