Verified Code Generation for the Polyhedral Model

Nathanaël Courant (1) , Xavier Leroy (2)

1 CAMBIUM - Langages de programmation : systèmes de types, concurrence, preuve de programme
2 Collège de France - Chaire Sciences du logiciel

The polyhedral model is a high-level intermediate representation for loop nests that supports elegantly a great many loop optimizations. In a compiler, after polyhedral loop optimizations have been performed, it is necessary and difficult to regenerate sequential or parallel loop nests before continuing compilation. This paper reports on the formalization and proof of semantic preservation of such a code generator that produces sequential code from a polyhedral representation. The formalization and proofs are mechanized using the Coq proof assistant.

Mots clés: Compilers; Domain-specific languages; Software verification; Program proof; Compiler verification; Polyhedral code generation; Polyhedral model

Domaines: Langage de programmation [cs.PL]; Logique en informatique [cs.LO]

Nathanaël Courant, Xavier Leroy. Verified Code Generation for the Polyhedral Model. Proceedings of the ACM on Programming Languages, 2021, 5 (POPL), pp.40:1-40:24. ⟨10.1145/3434321⟩. ⟨hal-03000244⟩