Scalable Deductive Verification of Data-Level Parallel Programs

Technische Samenvatting: Schaalbare Deductieve Verificatie van Data-Level Parallelle Programma's

Probleemstelling
Deductieve verificatie van data-level parallelle programma's (bijvoorbeeld GPU-kernels met CUDA, OpenCL of SYCL) staat voor aanzienlijke schaalbaarheidsuitdagingen. Deze programma's manipuleren doorgaans grote arrays en matrices, wat leidt tot formele contracten die rijk zijn aan geneste kwantoren. De belangrijkste knelpunten die zijn geïdentificeerd, zijn:

1. Kwantoren-instantiatie: SMT-oplossers worstelen met geneste kwantoren die rekenkundige expressies bevatten in array-indexen (bijvoorbeeld A[i * stride + offset]). Standaard E-matching (trigger-gebaseerde instantiatie) vereist dat triggers eenvoudige patronen zijn; rekenkundige bewerkingen binnen triggers verhinderen vaak dat de oplossingner geschikte instantiaties vindt, wat leidt tot verificatiefouten of excessive tijdsinvestering.
2. Aliasredenering: Programma's die meerdere arrays of matrices gebruiken, vereisen vaak redenering over de vraag of deze structuren overlappen (aliasing). In separatielogica genereert het verifiëren van niet-overlappende rechten voor potentieel overlappende arrays een kwadratisch aantal bewijsplichten, wat de verificatietijd drastisch verhoogt.

Methodologie
De auteurs stellen drie geïntegreerde technieken voor die zijn geïmplementeerd binnen VerCors, een deductieve programma-verificator gebaseerd op permission-based separatielogica en de Viper-intermediaire verificatietaal.

1. Kwantoren-herschrijving voor Triggergeneratie:
   Het artikel introduceert een procedure om expressies met geneste of complexe kwantoren om te zetten in equivalente vormen met enkele kwantoren en rekenkundevrije triggers.

   • Mechanisme: De methode identificeert lineair-rekenkundige indexeringspatronen van de vorm $f(x_1, \dots, x_k) = \sum a_i x_i + b$. Er wordt een bijectieve mapping (inverse functie $f^{-1}$) gedefinieerd van de lineaire index terug naar de oorspronkelijke gekwantificeerde variabelen.
   • Transformatie: De oorspronkelijke kwantor $\forall x_1, \dots, x_k; \dots; R(A[f(x_1, \dots, x_k)], \dots)$ wordt herschreven naar $\forall x; Y(x); R(A[x], f^{-1}(x))$. Hierdoor kan $A[x]$ dienen als een geldige trigger voor de SMT-oplosser.
   • Correctheid: De correctheid van de procedure is formeel bewezen met de Lean-theoremaprover (ongeveer 2500 regels code), waarbij wordt gegarandeerd dat de herschreven kwantor logisch equivalent is aan de oorspronkelijke onder specifieke voorwaarden met betrekking tot grenzen en coëfficiënten.

2. Unieke en Onveranderlijke Typekwalificatoren:
   Om aliasing en overhead van rechten aan te pakken, introduceren de auteurs twee typekwalificatoren:

   • Immutable (Onveranderlijk): Geeft aan dat de data waarnaar een pointer verwijst, niet verandert tijdens de uitvoering. Hierdoor kan de verificator de data modelleren als wiskundige sequenties in plaats van mutabele heap-blokken, wat de noodzaak van rechten-tracking elimineert en de complexiteit van heap-snapshots verlaagt.
   • Unique (Uniek): Wijs een uniekheidscijfer toe aan pointers. Pointers met verschillende uniekheidscijfers garanderen dat ze niet aliassen. Hierdoor kan de verificator niet-overlappende arrays coderen in afzonderlijke velden in de Viper-backend, waardoor de kwadratische explosie van snapshot-vergelijkingen die nodig zijn om aliasing te controleren, wordt voorkomen.
   • Integratie: Deze kwalificatoren zijn compatibel met bestaande bibliotheken en staan flexibele typecontrole toe, zodat functies die niet-unieke arrays verwachten, nog steeds unieke kunnen accepteren zolang de uniekheidsbeperkingen worden gerespecteerd.

3. Extraheren van Kernel-lichaam:
   De auteurs merken op dat het verifiëren van monolithische GPU-kernels vaak trager is vanwege de enorme hoeveelheid informatie die aan de SMT-oplosser wordt gepresenteerd. Zij stellen een geautomatiseerde extractiestrategie voor waarbij het kernel-lichaam wordt verplaatst naar een aparte functie met een eigen contract. Deze modularisatie verkleint de contextgrootte voor de oplossingner, wat de prestaties verbetert.

Belangrijkste Bijdragen

• Formele Herschrijvingsprocedure: Een wiskundig bewezen methode om geneste kwantoren met rekenkundige indexen te flattenen tot vormen met enkele kwantoren die geschikt zijn voor E-matching, geïmplementeerd in VerCors.
• Type-gebaseerde Aliasreductie: De introductie van unique en immutable kwalificatoren om de verificator expliciet te sturen over de geheugenindeling en mutabiliteit, wat de zoekruimte voor aliascontroles aanzienlijk verkleint.
• Uitgebreide Evaluatie: Een grootschalige experimentele evaluatie die de volgende omvat:
  • CLBlast-bibliotheek: Een suite van OpenCL-kernels die Basic Linear Algebra Subprograms (BLAS) implementeren.
  • Radio-telescooppijplijn: Een case study die het Padre-algoritme en andere geoptimaliseerde parallelle CPU-programma's omvat die zijn gegenereerd vanuit de Halide DSL.
• Beschikbaarheid Artefact: Alle experimentele data, het Lean-bewijs en de specifieke versie van VerCors die is gebruikt, worden geleverd in een bijbehorend artefact.

Resultaten
De experimenten tonen aanzienlijke verbeteringen in schaalbaarheid en slagingspercentages aan:

• CLBlast-kernels: Het toepassen van de gecombineerde technieken (herschrijving, unieke/onveranderlijke types en extractie) resulteerde in een gemiddelde reductie van de verificatietijd met een factor van 9. Bij specifieke uitschieters (bijvoorbeeld de xger-kernel) was de verificatie 150 keer sneller. Cruciaal is dat de combinatie van technieken de verificatie mogelijk maakte van kernels (zoals xger en xher2) die eerder onverifieerbaar waren of zeer breekbaar (in veel runs falend).
• Radio-telescooppijplijn: De technieken maakten de verificatie mogelijk van het perform_iteration-algoritme (Padre), wat in eerdere studies niet haalbaar was. Verificatietijden voor succesvolle gevallen werden met factoren tussen 1,2 en 3,4 verlaagd, afhankelijk van het specifieke algoritme en de configuratie.
• Afhankelijkheid van Herschrijving: De auteurs merken op dat zonder de kwantoren-herschrijvingsprocedure geen van de gerapporteerde experimenten überhaupt had kunnen worden geverifieerd, wat de fundamentele rol ervan onderstreept.

Betekenis
Het artikel stelt dat deze technieken fundamentele knelpunten in de deductieve verificatie van data-parallelle programma's aanpakken. Door de automatische generatie van geschikte triggers voor complexe array-toegang en het verminderen van de overhead van aliasredenering via typekwalificatoren, stellen de auteurs de verificatie mogelijk van complexe, real-world GPU- en parallelle CPU-kernels die eerder onhaalbaar waren. Het werk overbrugt de kloof tussen theoretische separatielogica en praktische, schaalbare verificatie van high-performance computing-code, met name door succes te tonen met het Padre-algoritme dat wordt gebruikt bij de verwerking van data van radio-telecopen. De auteurs benadrukken dat hoewel handmatige herschrijving mogelijk is, de automatische detectie en toepassing van deze patronen essentieel zijn voor de gestructureerde, geautomatiseerde verificatie van GPU-kernels.