Scalable Deductive Verification of Data-Level Parallel Programs

Sintesi Tecnica: Verifica Deduttiva Scalabile di Programmi con Parallelismo a Livello di Dati

Enunciato del Problema
La verifica deduttiva di programmi con parallelismo a livello di dati (ad esempio, kernel GPU che utilizzano CUDA, OpenCL o SYCL) affronta sfide significative di scalabilità. Questi programmi manipolano tipicamente grandi array e matrici, portando a contratti formali ricchi di quantificatori nidificati. I principali colli di bottiglia identificati sono:

1. Istanteizzazione dei Quantificatori: I solver SMT faticano con i quantificatori nidificati contenenti espressioni aritmetiche negli indici degli array (ad esempio, A[i * stride + offset]). La standard E-matching (istantizzazione basata su trigger) richiede trigger che siano pattern semplici; le operazioni aritmetiche all'interno dei trigger spesso impediscono al solver di trovare istanze adatte, portando a fallimenti nella verifica o a tempi eccessivi.
2. Ragionamento sugli Alias: I programmi che utilizzano più array o matrici richiedono spesso di ragionare su whether queste strutture si sovrappongono (aliasing). Nella logica di separazione, verificare permessi non sovrapposti per array potenzialmente sovrapposti genera un numero quadratico di obblighi di prova, aumentando drasticamente il tempo di verifica.

Metodologia
Gli autori propongono tre tecniche integrate implementate all'interno di VerCors, un verificatore di programmi deduttivo basato sulla logica di separazione basata sui permessi e sul linguaggio intermedio di verifica Viper.

1. Riscrittura dei Quantificatori per la Generazione di Trigger:
   Il documento introduce una procedura per riscrivere espressioni con quantificatori nidificati o complessi in forme equivalenti con quantificatori singoli e trigger privi di aritmetica.

   • Meccanismo: Il metodo identifica pattern di indicizzazione aritmetica lineare della forma $f(x_1, \dots, x_k) = \sum a_i x_i + b$. Definisce una mappatura biunivoca (funzione inversa $f^{-1}$) dall'indice lineare alle variabili quantificate originali.
   • Trasformazione: Il quantificatore originale $\forall x_1, \dots, x_k; \dots; R(A[f(x_1, \dots, x_k)], \dots)$ viene riscritto in $\forall x; Y(x); R(A[x], f^{-1}(x))$. Ciò permette ad $A[x]$ di fungere da trigger valido per il solver SMT.
   • Correttezza: La correttezza della procedura è dimostrata formalmente utilizzando il teorema prover Lean (circa 2500 righe di codice), garantendo che il quantificatore riscritto sia logicamente equivalente all'originale in condizioni specifiche riguardanti limiti e coefficienti.

2. Qualificatori di Tipo Unici e Immutabili:
   Per affrontare l'aliasing e l'overhead dei permessi, gli autori introducono due qualificatori di tipo:

   • Immutabile: Indica che i dati puntati da un puntatore non cambiano durante l'esecuzione. Ciò permette al verificatore di modellare i dati come sequenze matematiche anziché blocchi di heap mutabili, eliminando la necessità di tracciamento dei permessi e riducendo la complessità degli snapshot dell'heap.
   • Unico: Assegna un numero di unicità ai puntatori. I puntatori con numeri di unicità diversi sono garantiti come non alias. Ciò permette al verificatore di codificare array non sovrapposti in campi distinti nel backend Viper, prevenendo l'esplosione quadratica dei confronti degli snapshot richiesti per verificare l'aliasing.
   • Integrazione: Questi qualificatori sono compatibili con le librerie esistenti e permettono un controllo dei tipi flessibile, garantendo che le funzioni che si aspettano array non unici possano comunque accettarne di unici se i vincoli di unicità sono rispettati.

3. Estrazione del Corpo del Kernel:
   Gli autori osservano che verificare kernel GPU monolitici è spesso più lento a causa del volume enorme di informazioni presentate al solver SMT. Propongono una strategia di estrazione automatizzata in cui il corpo del kernel viene spostato in una funzione separata con il proprio contratto. Questa modularizzazione riduce le dimensioni del contesto per il solver, migliorando le prestazioni.

Contributi Chiave

• Procedura di Riscrittura Formale: Un metodo matematicamente provato per appiattire i quantificatori nidificati con indici aritmetici in forme a quantificatore singolo adatte all'E-matching, implementato in VerCors.
• Riduzione dell'Aliasing Basata sui Tipi: L'introduzione dei qualificatori unique e immutable per guidare esplicitamente il verificatore sul layout della memoria e sulla mutabilità, riducendo significativamente lo spazio di ricerca per i controlli di aliasing.
• Valutazione Completa: Una valutazione sperimentale su larga scala che copre:
  • Libreria CLBlast: Una suite di kernel OpenCL che implementano le Sottoroutine di Algebra Lineare di Base (BLAS).
  • Pipeline del Radiotelescopio: Uno studio di caso che coinvolge l'algoritmo Padre e altri programmi CPU paralleli ottimizzati generati dal DSL Halide.
• Disponibilità dell'Artifatto: Tutti i dati sperimentali, la prova Lean e la specifica versione di VerCors utilizzata sono forniti in un artifatto allegato.

Risultati
Gli esperimenti dimostrano miglioramenti sostanziali nella scalabilità e nei tassi di successo:

• Kernel CLBlast: L'applicazione delle tecniche combinate (riscrittura, tipi unici/immutabili ed estrazione) ha portato a una riduzione media del tempo di verifica di un fattore di 9. In casi specifici anomali (ad esempio, il kernel xger), la verifica è stata 150 volte più veloce. Crucialmente, la combinazione di tecniche ha permesso la verifica di kernel (come xger e xher2) che erano precedentemente non verificabili o altamente fragili (fallendo in molte esecuzioni).
• Pipeline del Radiotelescopio: Le tecniche hanno permesso la verifica dell'algoritmo perform_iteration (Padre), che non era ottenibile negli studi precedenti. I tempi di verifica per i casi riusciti sono stati ridotti di fattori compresi tra 1,2 e 3,4 a seconda dell'algoritmo specifico e della configurazione.
• Dipendenza dalla Riscrittura: Gli autori notano che senza la procedura di riscrittura dei quantificatori, nessuno degli esperimenti riportati sarebbe stato verificabile in assoluto, evidenziandone il ruolo fondamentale.

Significato
Il documento afferma che queste tecniche affrontano i colli di bottiglia fondamentali nella verifica deduttiva di programmi paralleli a livello di dati. Automatizzando la generazione di trigger adatti per accessi complessi agli array e riducendo l'overhead del ragionamento sugli alias attraverso i qualificatori di tipo, gli autori abilitano la verifica di kernel GPU e CPU paralleli complessi e reali che erano precedentemente non fattibili. Il lavoro colma il divario tra la logica di separazione teorica e la verifica pratica e scalabile del codice per il calcolo ad alte prestazioni, dimostrando specificamente il successo sull'algoritmo Padre utilizzato nell'elaborazione dei dati dei radiotelescopi. Gli autori sottolineano che, sebbene la riscrittura manuale sia possibile, il rilevamento e l'applicazione automatici di questi pattern sono essenziali per la verifica strutturata e automatizzata dei kernel GPU.