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.

@article{paperbot1527,
  title = {End-to-end translation validation for the halide language},
  author = {Basile Clément and Albert Cohen},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {6},
  number = {OOPSLA1},
  year = {2022},
  doi = {10.1145/3527328}
}