Résumé Technique : Logique de Séparation pour la Détection de Conflits Mémoire en Synthèse de Haut Niveau

Énoncé du Problème

La Synthèse de Haut Niveau (HLS) accélère le développement matériel en traduisant du code C/C++ en conceptions de niveau de transfert de registres (RTL), en exploitant le déroulement de boucles (loop unrolling) et le partitionnement de tableaux pour maximmer le parallélisme. Cependant, un goulot d'étranglement critique surgit lors de l'ordonnancement d'accès mémoire concomitants impliquant une arithmétique non affine (par exemple, multiplication, division ou modulo symboliques).

Les frameworks HLS traditionnels s'appuient sur le modèle polyédrique pour l'analyse de dépendance. Cette approche géométrique exige que les bornes de boucle et les fonctions d'accès aux tableaux soient affines (combinaisons linéaires de variables de boucle). Face à des indices non affines, les solveurs polyédriques sur-approximent systématiquement les dépendances pour garantir la sécurité. Cela impose un repli conservateur : supposer que toutes les instructions mémoires dépendent les unes des autres, ce qui entraîne une allocation de tas monolithique et la sérialisation d'opérations qui pourraient autrement s'exécuter en parallèle. Cette sérialisation artificielle dégrade le débit et l'efficacité du matériel. De plus, les techniques dynamiques existantes nécessitent souvent des vérifications au moment de l'exécution ou des contrôleurs spécialisés, ce qui ajoute une surcharge (overhead).

Méthodologie

Le papier propose un framework de vérification spatiale opérant directement sur la représentation intermédiaire (IR) de LLVM pour détecter les conflits mémoire sans dépendre des contraintes géométriques affines. La méthodologie centrale intègre la Logique de Séparation (SL) avec la résolution par Théorie de la Saturation de Modèles (SMT).

1. Modélisation Spatiale au Niveau de l'IR LLVM

Contrairement aux approches précédentes qui analysent les arbres de syntaxe abstraite (AST) de C/C++, ce framework opère sur l'IR de LLVM. Il exploite l'instruction getelementptr (GEP), que le compilateur utilise pour aplatir mécaniquement les indices de tableaux multidimensionnels en expressions arithmétiques unidimensionnelles.

• Architecture à Double État : Le framework modélise l'état du système en utilisant deux composants distincts :
  • Magasin Monotone ($s$) : Cartographie les registres virtuels immuables de la forme SSA (Static Single Assignment) vers des valeurs. En raison de la SSA, les registres ne sont jamais écrasés, ce qui simplifie le suivi de l'état.
  • Tas Spatial ($h$) : Cartographie les adresses physiques de la mémoire (sous-ensemble de valeurs) vers des données, représentant les banques de SRAM intégrées.
• Prédicats de Banque Polymorphes : Le framework définit des prédicats spatiaux bank(k, A, N) qui affirment la propriété exclusive de la $k$-ième banque de mémoire pour le tableau $A$ partitionné en $N$ banques. Ces prédicats s'adaptent dynamiquement selon la stratégie de partitionnement (Cyclique, par Bloc, ou Complète) extraite des métadonnées LLVM.

2. La Condition de Déroulement Sans Conflit (CFU)

Pour vérifier que $U$ itérations de boucle déroulées peuvent s'exécuter de manière concomitante sans aléas structurels, le framework formule la condition de Déroulement Sans Conflit (Conflict-Free Unrolling - CFU).

• Conjonction Séparante ($\ast$) : Le cœur de la vérification est la conjonction séparante itérée :
  $$cfu(E, A, N) \triangleq \ast_{i=1}^{U} bank(B(expr_i, N), A, N)$$
  Ceci affirme que les $U$ accès mémoire concomitants doivent posséder $U$ régions de mémoire physique strictement disjointes.
• Effondrement Spatial : Un axiome fondamental de la Logique de Séparation est qu'une ressource ne peut pas être possédée de manière disjointe par elle-même ($P \ast P \implies \bot$). Si deux itérations concomitantes ciblent la même banque physique $k$, la formule spatiale tentera d'évaluer $bank(k) \ast bank(k)$, ce qui aboutit logiquement à une contradiction ($\bot$). Cet effondrement sert de détection mathématique d'un conflit mémoire.

3. Traduction en SMT et Repli (Fallback)

Pour rendre la logique spatiale calculable, le framework emploie une fonction de traduction $T$ qui réduit l'exigence de disjointivité spatiale en une matrice d'inégalités par paires sur les variables SSA.

• Condition de Vérification (VC) : La exigence spatiale est traduite en une formule de logique du premier ordre :
  $$\pi \implies \bigwedge_{1 \le i < j \le U} (k_i \neq k_j)$$
  où $\pi$ est la condition de chemin et $k_i$ sont les indices de banque symboliques.
• Oracle SMT : Un solveur SMT (par exemple, Z3) tente de prouver la VC.
  • Sat (Satisfaisable) : Les indices sont prouvés distincts ; la synthèse parallèle peut procéder.
  • Unsat/Unknown/Timeout : Si le solveur ne peut prouver la disjointivité (en raison d'une arithmétique entière non linéaire indécidable), le framework déclenche un repli séquentiel déterministe. Il suppose l'existence d'un aléa, sérialisant les opérations via une logique de blocage pilotée par multiplexeur pour garantir la sécurité physique.

Contributions Clés

1. Modèle de Mémoire Matériel Formel : Le papier établit un cadre de mémoire statique sur l'IR de LLVM, abstrayant les indices de tableaux multidimensionnels via les instructions GEP et les liant à des prédicats spatiaux polymorphes qui gèrent le partitionnement cyclique, par bloc et complet.
2. Condition de Déroulement Sans Conflit (CFU) : Une exigence d'exécution spatiale définitive est formulée en utilisant la conjonction séparante itérée. Elle détecte les aléas de banques physiques par un effondrement automatique de la logique spatiale ($cfu \implies \bot$) plutôt que par sur-approximation géométrique.
3. Traduction SMT Automatisée et Repli : Une fonction de traduction mathématiquement saine réduit les propositions spatiales à des inégalités par paires sur des registres SSA immuables. Crucialement, elle inclut un modèle de repli séquentiel conservateur pour assurer une sécurité absolue lorsque l'arithmétique entière non linéaire est indécidable.
4. Théorème de Correction (Soundness) : Le papier prouve que si la Condition de Vérification algébrique est validée par le solveur SMT, le RTL synthétisé résultant est structurellement immunisé contre les collisions de banques mémoire.

Résultats et Signification

Le papier affirme combler le fossé entre la théorie de la logique de séparation formelle et la synthèse matérielle pratique. En déplaçant la charge de vérification des modèles polyédriques géométriques vers la résolution algébrique SMT sur l'IR de LLVM, le framework :

• Minimise la Sérialisation Conservatrice : Il évite le repli "sûr mais lent" des outils traditionnels lors de la rencontre d'indices non affines, à condition que le solveur SMT puisse résoudre les contraintes algébriques.
• Garantit la Sécurité Structurelle : Grâce au mécanisme d'« Effondrement Spatial » et au repli conservateur, le framework garantit qu'aucun matériel synthétisé ne souffrira de collisions de banques mémoire structurelles, même en présence d'une arithmétique indécidable.
• Contourne les Limitations Affines : Il résout les dépendances complexes de mappage de banques sans nécessiter de bornes géométriques linéaires ou de générer une surcharge supplémentaire de machine à états au moment de l'exécution.

La signification réside dans la fourniture d'une alternative algébrique rigoureuse au modèle polyédrique pour l'ordonnancement HLS, permettant un parallélisme plus élevé dans les conceptions avec des modèles d'accès mémoire non affines tout en maintenant les garanties de sécurité absolue requises pour la génération de matériel. Les auteurs notent que les travaux futurs impliqueront l'implémentation de cela en tant que passage (pass) LLVM personnalisé et l'exploration des permissions fractionnaires pour optimiser les accès concomitants en lecture seule.