On Complexity Bounds and Confluence of Parallel Term Rewriting

Panoramica del Problema

Il paper affronta un vuoto significativo nella letteratura sulla complessità computazionale: l'assenza di tecniche automatiche per analizzare la complessità di sistemi di riscrittura di termini (TRS) quando valutati con strategie parallele.
Mentre esistono strumenti maturi per stimare i limiti di complessità (superiori e inferiori) per la riscrittura sequenziale (in particolare la strategia innermost, che corrisponde alla valutazione call-by-value in linguaggi come OCaml, Scala, Rust), non esisteva un approccio sistematico per la versione parallela.
La sfida principale è determinare quanto velocemente un programma può essere eseguito su macchine con parallelismo illimitato (es. GPU), distinguendo tra il "lavoro" totale (tempo CPU sequenziale) e il "tempo di span" (tempo di parete o wall time in parallelo). Inoltre, per derivare limiti inferiori precisi, è necessario garantire che il sistema sia confluenza (i risultati siano deterministici), una proprietà che non è sempre ovvia nella riscrittura parallela.

Metodologia

Gli autori propongono un approccio trasformativo che riutilizza le tecniche esistenti per la complessità sequenziale, adattandole al contesto parallelo. La metodologia si articola in tre pilastri principali:

1. Parallel Dependency Tuples (PDT):

   • Estendono il concetto classico di Dependency Tuples (DT), usato per l'analisi sequenziale.
   • Invece di raggruppare tutte le chiamate di funzione di una regola in un singolo tuple (come nella versione sequenziale), i PDT generano multiple regole di dipendenza per ogni regola di riscrittura.
   • Ogni regola PDT corrisponde a una "catena di dipendenza strutturale" massimale (Maximal Structural Dependency Chain - MSDC). Questo permette di modellare il fatto che, in esecuzione parallela, il costo di una regola è dato dal massimo dei costi dei suoi rami indipendenti, non dalla somma.
   • Questo approccio permette di riutilizzare direttamente i processori esistenti (come le interpretazioni polinomiali) per calcolare limiti superiori.

2. Trasformazione in Riscrittura Relativa (Per i Limiti Inferiori):

   • Per calcolare i limiti inferiori, gli autori trasformano il problema dei PDT in un TRS relativo ($S / ((D \setminus S) \cup R)$).
   • In questo sistema, le regole dei PDT sono considerate "costose" (contano per la complessità), mentre le regole originali del TRS e quelle di supporto sono "gratuite".
   • Questa trasformazione permette di utilizzare strumenti esistenti (come APROVE e TCT) per calcolare limiti inferiori sulla complessità sequenziale del sistema relativo, che corrispondono poi ai limiti inferiori per la complessità parallela originale (a condizione di confluenza).

3. Criteri di Confluenza per la Riscrittura Parallela:

   • Poiché la derivazione dei limiti inferiori richiede confluenza, il paper introduce criteri sintetici efficienti per provare la confluenza della relazione di riscrittura parallela-innermost ($\stackrel{i}{\rightarrow}_R$).
   • Corollario 6.10: Se un TRS è non-overlapping (nessun sovrapposizione tra le parti destre delle regole), la riscrittura parallela è deterministica e quindi confluenza.
   • Teorema 6.18 (Nuovo Contributo): Una condizione più forte e generale. Se tutti i critical overlays innermost (sovrapposizioni che possono avvenire in una riscrittura innermost) sono triviali (entrambi i lati del critical pair sono identici), allora la riscrittura parallela-innermost è deterministica e confluenza. Questo criterio è più potente di quelli esistenti per la riscrittura sequenziale in questo contesto specifico.

Contributi Chiave

1. Definizione Formale: Introduzione della complessità parallel-innermost runtime complexity ($pirc_R$) come misura dello span temporale su macchine parallele illimitate.
2. Framework PDT: Sviluppo dei Parallel Dependency Tuples, che catturano le dipendenze strutturali e permettono di riutilizzare l'infrastruttura esistente dei DT per l'analisi parallela.
3. Teoremi di Correttezza: Dimostrazione che la complessità calcolata sui PDT (tramite chain tree) fornisce un limite superiore corretto per $pirc_R$, e un limite esatto se il sistema è confluenza.
4. Criteri di Confluenza: Proposta di criteri sintetici (Corollario 6.10 e Teorema 6.18) per verificare automaticamente la confluenza della riscrittura parallela, essenziale per l'analisi dei limiti inferiori.
5. Implementazione e Sperimentazione: Integrazione di queste tecniche nel tool APROVE e valutazione su un vasto set di benchmark (TPDB e COPS).

Risultati Sperimentali

Gli esperimenti sono stati condotti su 294 TRS del TPDB (selezionati per avere potenziale di parallelismo) e su 577 TRS dal benchmark COPS per la confluenza.

• Limiti Superiori: L'approccio proposto ha migliorato significativamente i limiti superiori rispetto all'uso dei limiti sequenziali come approssimazione. Ad esempio, per alcuni casi, il limite è passato da $O(n^{10})$ (sequenziale) a $O(n)$ (parallelo), identificando correttamente strutture ricorsive altamente parallelizzabili (simili a loop vettoriali).
• Limiti Inferiori: Utilizzando la trasformazione in TRS relativo e i nuovi criteri di confluenza, è stato possibile derivare limiti inferiori non banali per un numero significativo di casi.
• Confluenza: Il nuovo criterio (Teorema 6.18) ha dimostrato di essere molto più efficace di quello basato sulla non-sovrapposizione (Corollario 6.10). Su COPS, ha provato la confluenza per il 47.5% dei TRS contro il 10.4% del criterio precedente.
• Precisione: Per 49 TRS, il tool è riuscito a trovare limiti superiori e inferiori che coincidono asintoticamente ($\Theta$), fornendo una stima precisa della complessità parallela.
• Efficienza: I controlli di confluenza sono estremamente veloci (pochi millisecondi) poiché puramente sintattici, senza problemi di ricerca.

Significato e Impatto

Questo lavoro è fondamentale per diversi motivi:

• Compilatori Paralleli: Fornisce agli sviluppatori di compilatori paralleli (es. per GPU) strumenti statici per decidere se una funzione merita di essere parallelizzata. Se la complessità parallela è asintoticamente uguale a quella sequenziale, la parallelizzazione potrebbe non essere vantaggiosa.
• Analisi di Programmi Funzionali: Offre un metodo rigoroso per analizzare la complessità di programmi su strutture dati induttive (liste, alberi) in linguaggi funzionali moderni che usano la valutazione call-by-value.
• Ponte tra Teoria e Pratica: Dimostra che tecniche avanzate di analisi statica (Dependency Tuples) possono essere estese con successo a modelli di calcolo parallelo, riutilizzando l'ecosistema esistente di strumenti di verifica.
• Sicurezza: La capacità di provare la confluenza in modo automatico è cruciale per garantire che l'esecuzione parallela non introduca non-determinismo nei risultati, un requisito fondamentale per l'affidabilità del software.

In sintesi, il paper stabilisce le basi teoriche e pratiche per l'analisi automatica della complessità parallela nei sistemi di riscrittura, offrendo un metodo robusto per quantificare il potenziale di accelerazione dei programmi funzionali.