Sintesi Tecnica: Logica di Separazione per il Rilevamento dei Conflitti di Memoria nella Sintesi di Alto Livello

Definizione del Problema

La Sintesi di Alto Livello (HLS) accelera lo sviluppo dell'hardware traducendo codice C/C++ in design a livello di trasferimento di registro (RTL), sfruttando l'unrolling dei cicli e la partizione degli array per massimizzare il parallelismo. Tuttavia, un collo di bottiglia critico sorge quando si pianificano accessi alla memoria concorrenti che coinvolgono l'aritmetica non affine (ad esempio, moltiplicazione simbolica, divisione o operazione modulo).

I framework HLS tradizionali si affidano al modello poliedrico per l'analisi delle dipendenze. Questo approccio geometrico richiede che i limiti dei cicli e le funzioni di accesso agli array siano affini (combinazioni lineari di variabili di ciclo). Quando si affrontano indici non affini, i solver poliedrici ricorrono sistematicamente all'approssimazione eccessiva delle dipendenze per garantire la sicurezza. Ciò forza un fallback conservativo: assumere che tutte le istruzioni di memoria dipendano l'una dall'altra, risultando in un'allocazione monolitica dell'heap e nella serializzazione di operazioni che potrebbero invece essere eseguite in parallelo. Questa serializzazione artificiale degrada il throughput e l'efficienza dell'hardware. Inoltre, le tecniche dinamiche esistenti richiedono spesso controlli a runtime o controller specializzati, aggiungendo overhead.

Metodologia

Il documento propone un framework di verifica spaziale che opera direttamente sulla Rappresentazione Intermedia (IR) di LLVM per rilevare conflitti di memoria senza fare affidamento su vincoli geometrici affini. La metodologia centrale integra la Logica di Separazione (SL) con la risoluzione tramite Satisfiability Modulo Theories (SMT).

1. Modellazione Spaziale al Livello LLVM IR

A differenza dei precedenti approcci che analizzano gli Alberi di Sintassi Astratta (AST) del C/C++, questo framework opera sull'IR di LLVM. Esso sfrutta l'istruzione getelementptr (GEP), che il compilatore utilizza per appiattire meccanicamente gli indici di array multidimensionali in espressioni aritmetiche 1D.

• Architettura a Stato Duale: Il framework modella lo stato del sistema utilizzando due componenti distinte:
  • Store Monotono ($s$): Mappa i registri virtuali Static Single Assignment (SSA) immutabili ai valori. Grazie all'SSA, i registri non vengono mai sovrascritti, semplificando il tracciamento dello stato.
  • Heap Spaziale ($h$): Mappa gli indirizzi fisici di memoria (sottoinsieme di valori) ai dati, rappresentando i banchi di memoria SRAM on-chip.
• Predicati di Banco Polimorfici: Il framework definisce i predicati spaziali bank(k, A, N) che assertano la proprietà esclusiva del $k$-esimo banco di memoria per l'array $A$ partizionato in $N$ banchi. Questi predicati si adattano dinamicamente in base alla strategia di partizione (Ciclica, a Blocchi o Completa) estratta dai metadati LLVM.

2. La Condizione di Unrolling Senza Conflitti (CFU)

Per verificare che $U$ iterazioni di un ciclo unrolled possano eseguire in modo concorrente senza hazard strutturali, il framework formula la condizione di Unrolling Senza Conflitti (Conflict-Free Unrolling - CFU).

• Congiunzione Separante ($\ast$): Il cuore della verifica è la congiunzione separante iterata:
  $$cfu(E, A, N) \triangleq \ast_{i=1}^{U} bank(B(expr_i, N), A, N)$$
  Questa asserzione stabilisce che le $U$ accessi concorrenti alla memoria devono possedere $U$ regioni di memoria fisica strettamente disgiunte.
• Collasso Spaziale: Un assioma fondamentale della Logica di Separazione è che una risorsa non può essere posseduta disgiuntamente da se stessa ($P \ast P \implies \bot$). Se due iterazioni concorrenti puntano allo stesso banco fisico $k$, la formula spaziale tenta di valutare $bank(k) \ast bank(k)$, che logicamente collassa in una contraddizione ($\bot$). Questo collasso funge da rilevamento matematico di un conflitto di memoria.

3. Traduzione in SMT e Fallback

Per rendere computabile la logica spaziale, il framework impiega una funzione di traduzione $T$ che riduce il requisito di disgiunzione spaziale in una matrice di disuguaglianze a coppie su variabili SSA.

• Condizione di Verifica (VC): Il requisito spaziale viene tradotto in una formula di logica del primo ordine:
  $$\pi \implies \bigwedge_{1 \le i < j \le U} (k_i \neq k_j)$$
  dove $\pi$ è la condizione di percorso e $k_i$ sono gli indici di banco simbolici.
• Oracolo SMT: Un solver SMT (ad esempio, Z3) tenta di provare la VC.
  • Sat (Satisfiable): Gli indici sono provabilmente distinti; la sintesi parallela procede.
  • Unsat/Unknown/Timeout: Se il solver non può provare la disgiunzione (a causa di un'aritmetica non lineare indecidibile), il framework attiva un fallback sequenziale deterministico. Assume che esista un hazard, serializzando le operazioni tramite una logica di stall guidata da multiplexer per garantire la sicurezza fisica.

Contributi Chiave

1. Modello di Memoria Hardware Formale: Il documento stabilisce un framework di memoria statica sull'IR di LLVM, astrando gli indici di array multidimensionali tramite istruzioni GEP e legandoli a predicati spaziali polimorfici che gestiscono la partizione ciclica, a blocchi e completa.
2. Condizione di Unrolling Senza Conflitti (CFU): Viene formulata un requisito di esecuzione spaziale definitivo utilizzando la congiunzione separante iterata. Essa rileva gli hazard dei banchi di memoria attraverso l'automatica collisione della logica spaziale ($cfu \implies \bot$) anziché tramite l'approssimazione geometrica eccessiva.
3. Traduzione SMT Automatica e Fallback: Una funzione di traduzione matematicamente solida riduce le proposizioni spaziali a disuguaglianze a coppie su registri SSA immutabili. Fondamentalmente, include un modello di fallback sequenziale conservativo per garantire l'assoluta sicurezza quando l'aritmetica intera non lineare è indecidibile.
4. Teorema di Soundness (Correttezza): Il documento dimostra che se la Condizione di Verifica algebrica è validata dal solver SMT, il design RTL risultante è strutturalmente immune alle collisioni dei banchi di memoria.

Risultati e Significato

Il documento sostiene di colmare il divario tra la teoria della logica di separazione formale e la sintesi hardware pratica. Spostando l'onere della verifica dai modelli poliedrici geometrici alla risoluzione algebrica SMT sull'IR di LLVM, il framework:

• Minimizza la Serializzazione Conservativa: Evita il fallback "sicuro ma lento" degli strumenti tradizionali quando incontrano indici non affini, a patto che il solver SMT sia in grado di risolvere i vincoli algebrici.
• Garantisce la Sicurezza Strutturale: Attraverso il meccanismo di "Collasso Spaziale" e il fallback conservativo, il framework garantisce che nessun hardware sintetizzato soffrirà di collisioni strutturali della memoria, anche in presenza di aritmetica indecidibile.
• Supera i Limiti Affini: Risolve complesse dipendenze di mappatura dei banchi senza richiedere limiti geometrici lineari o generare ulteriore overhead di macchine a stati a runtime.

Il significato risiede nel fornire un'alternativa algebrica rigorosa al modello poliedrico per la pianificazione HLS, consentendo un maggiore parallelismo nei design con pattern di accesso alla memoria non affini, pur mantenendo le garanzie di sicurezza assoluta richieste dalla generazione dell'hardware. Gli autori notano che il lavoro futuro comporterà l'implementazione di questo come un pass custom di LLVM ed esplorerà le permessi frazionarie per ottimizzare gli accessi concorrenti di sola lettura.