~/talk

Verified Code Generation for the Polyhedral Model

on YouTube 23m
Talkat POPL 2021 · 2021-01-17..01-22· [compilers-and-language-design]

speakers

name:Nathanaëlle Courant
links:none on file
name:Xavier Leroy
links:none on file

resources

video:https://youtu.be/MJ_NjnIqM38
slides:none on file

summary

A formally verified code generator turns a polyhedral IR into sequential counted loops and is mechanized in Coq producing about 8k lines of development; it proves semantics preservation across passes that remove schedules, build a high‑level AST with polyhedral guards and loops, eliminate redundant constraints, and emit for‑loops with concrete bounds. The formalization uses list‑of‑lists matrices (no dependent types), reuses a verified polyhedral library, and exposes a rare incompleteness in prior projection ordering resolved by further splitting.

AI-written summary · about

chapters (22)

  1. 0:00Intro
  2. 0:15Loops in numerical computing Example: matrix multiplication
  3. 0:31Loop nests
  4. 1:09Loop optimizations
  5. 2:35A loop nest as a polyhedron
  6. 3:10Transformations in the polyhedral model
  7. 3:37Loop interchange as a polyheral transformation Loop interchange is a simple change of schedule
  8. 4:00Structure of a polyhedral optimizer
  9. 5:40Our formally verified code generator In this paper formalization and verification (in Coq) of a code generator from a polyhedral representation
  10. 7:32Polyhedral programs and instructions
  11. 8:29Semantics of polyhedral programs
  12. 9:12Intermediate language
  13. 11:15Simple case: only one polyhedral instruction
  14. 11:45Example of code generation with one polyhedral instruction
  15. 13:06General case: several polyhedral instructions
  16. 14:16Example with several polyhedra
  17. 15:55An incompleteness of the algorithm
  18. 18:21Generation of counted loops
  19. 19:18The impact of redundant constraint elimination
  20. 20:02The Coq formalization
  21. 21:37Future work
  22. 22:25Conclusions

related talks

~/search
type to search 6,249 conferences, 138,987 speakers and 185,172 talks
~/help
cmdctrl k
search every conference, speaker and series
/
focus the filter search
h
home
c
conferences
s
speakers
e
series
t
light / dark — the status bar button does the same
?
this help
esc
close this, then clear every filter — or just the search, while you are typing in it

Ignored while you are typing. Pages without a filter rail have no search to focus.