End-to-End Translation Validation for the Halide Language - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2022

End-to-End Translation Validation for the Halide Language

Résumé

This paper considers the correctness of domain-specific compilers for tensor programming languages through the study of Halide, a popular representative. It describes a translation validation algorithm for affine Halide specifications, independently of the scheduling language. The algorithm relies on "propheticž annotations added by the compiler to the generated array assignments. The annotations provide a refinement mapping from assignments in the generated code to the tensor definitions from the specification. Our implementation leverages an affine solver and a general SMT solver, and scales to complete Halide benchmarks.
Fichier principal
Vignette du fichier
oopsla_halide_tv.pdf (385.97 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03653857 , version 1 (28-04-2022)

Identifiants

Citer

Basile Clément, Albert Cohen. End-to-End Translation Validation for the Halide Language. OOPSLA 2022 - Conference on Object-Oriented Programming Systems, Languages, and Applications, Dec 2022, Auckland, New Zealand. ⟨10.1145/3527328⟩. ⟨hal-03653857⟩
202 Consultations
123 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More