FR
Racer vérifie que les noyaux GPU réécrits préservent leur fonction
Racer: Hunting GPU Kernel Bugs with Symbolic Equivalence Checking · arXiv:2610.28429
En termes simples
Les noyaux GPU sont de petits programmes qui effectuent des calculs sur un processeur graphique. Quand des développeurs en réécrivent un pour l’accélérer, les tests ordinaires comparent les résultats pour quelques entrées choisies.
Ils peuvent donc manquer des cas rares, des valeurs mémoire cachées ou des réponses fausses dont l’écart reste dans la tolérance admise. L’article présente Racer, qui compare deux noyaux à l’aide d’expressions représentant les entrées possibles, au lieu de se limiter à quelques essais.
Dans une étude portant sur 2,408 noyaux de production, les auteurs ont trouvé 82 bugs. Racer en a automatiquement révélé 76 ; les six autres ont nécessité une inspection manuelle.
La recherche
Quand des développeurs réécrivent des noyaux GPU pour les accélérer, comment vérifier que le nouveau code calcule toujours la même fonction ? Les tests sur des entrées échantillonnées ne comparent les sorties que pour quelques cas.
Ils peuvent manquer des situations rares, des valeurs mémoire cachées, des écritures supplémentaires ou des erreurs logiques assez petites pour rester dans la tolérance.
Racer compare symboliquement les noyaux GPU à leurs références pour vérifier s’ils calculent la même fonction pour les entrées possibles.
Pour vérifier qu’une réécriture de noyau GPU préserve sa fonction, les auteurs présentent Racer, un moteur qui compare symboliquement un noyau à une référence.
Il compare les expressions de sortie pour les entrées possibles et suit les écritures mémoire, ce qui répond aux angles morts des tests qui échantillonnent les entrées et comparent les sorties déclarées avec une tolérance.
Dans une étude portant sur 2,408 noyaux de production, les auteurs ont trouvé 82 bugs distincts. Racer en a automatiquement révélé 76 grâce à ses diagnostics ou à des contre-exemples de sortie.
Ces résultats indiquent que la méthode peut trouver de vrais défauts dans cet ensemble, y compris des défauts manqués par les tests classiques.
L’étude porte sur les noyaux collectés et les configurations de lancement testées. Racer a refusé d’exécuter 499 des 2,408 noyaux. Une preuve ne s’applique qu’aux sorties et aux affectations d’indices vérifiées pour la configuration concernée.
Ce que montrent les preuves
- Pourquoi les tests sur échantillons manquent des bugs
Une réécriture de noyau GPU doit préserver la fonction du code qu’elle remplace. Les tests différentiels courants exécutent le nouveau noyau et une référence fiable sur des entrées échantillonnées, puis comparent les sorties déclarées en appliquant une tolérance numérique.
L’étude des bugs dans des bibliothèques utilisées en production montre pourquoi ces tests peuvent en manquer : ils peuvent ne pas couvrir des valeurs rares, laisser inchangé l’état implicite de la mémoire, ignorer les écritures au-delà des sorties déclarées ou accepter un résultat erroné dont l’écart reste dans la tolérance.
- Comparer directement les fonctions
Racer vérifie l’équivalence de noyaux GPU. Il exécute symboliquement un noyau et sa référence avec les mêmes entrées symboliques, transforme leurs sorties en expressions, puis vérifie l’égalité des cellules correspondantes.
Il consigne aussi les adresses mémoire afin de repérer les écritures hors des sorties déclarées. Cette méthode cherche à savoir si les noyaux calculent la même fonction pour toutes les entrées possibles, plutôt que si leurs sorties sont proches pour quelques entrées choisies.
- Modéliser l’exécution avec des limites
La vérification symbolique analyse le PTX, l’ensemble d’instructions virtuelles de NVIDIA documenté publiquement. Pour éviter de répéter inutilement les preuves, Racer réutilise une preuve portant sur une cellule de sortie représentative, mais seulement après avoir vérifié que les expressions de l’autre cellule correspondent sous un renommage des entrées.
Il coordonne les threads GPU autour des points de synchronisation pris en charge par son modèle et suit les accès mémoire. S’il ne peut pas représenter fidèlement une exécution, il la refuse ; si une preuve reste sans conclusion, le verdict peut être « Inconnu ».
- Repérer des défauts dans du code de production
Dans une étude portant sur 2,408 noyaux de production provenant de 41 sources de collecte, les auteurs ont trouvé 82 bugs distincts dans 23 bibliothèques. Racer en a automatiquement révélé 76 grâce à ses diagnostics ou à des contre-exemples de sortie ; les six autres ont été identifiés par inspection manuelle de cas non résolus.
Ces résultats montrent que le moteur peut révéler de vrais défauts dans cet ensemble, y compris des bugs qui avaient échappé aux tests classiques. Parmi les 76 bugs jusque-là inconnus signalés aux responsables des projets, 41 ont été confirmés.
- Interpréter les comparaisons avec prudence
Sur le même ensemble de 82 bugs, les auteurs ont évalué qu’un test différentiel avec oracle pourrait en détecter 47 en vérifiant toutes les entrées possibles des tenseurs, pour une configuration de lancement déclenchant le bug, par comparaison avec une référence indépendante soumise à une tolérance.
Il s’agissait d’une évaluation bug par bug, et non d’une campagne de tests. Les exécutions consignées ont détecté 18 bugs avec compute-sanitizer et neuf avec Volta.
Par ailleurs, l’exécution a été refusée pour 499 des 2,408 noyaux : ces résultats ne démontrent donc pas que chaque noyau ou configuration a été vérifié.
Détails
- Auteurs de l’article original
- Tuan Truong Vu, Cheng Tan
- Soumis à arXiv
- Licence
- CC BY 4.0