Generation of Compiler Backends from Formal Models of Hardware

This thssis has some examples of how you might do that.


It sounds swell in theory, but it's far from clear how well it actually
works.


Abstract:


Compilers convert between representations -- usually, from higher-level,
human writable code to lower-level, machine-readable code. A compiler
backend is the portion of the compiler containing optimizations and code
generation routines for a specific hardware target. In this dissertation,
I advocate for a specific way of building compiler backends: namely, by
automatically generating them from explicit, formal models of hardware
using automated reasoning algorithms. I describe how automatically
generating compilers from formal models of hardware leads to increased
optimization ability, stronger correctness guarantees, and reduced
development time for compiler backends. As evidence, I present two case
studies: first, Glenside, which uses equality saturation to increase the
3LA compiler's ability to offload operations to machine learning
accelerators, and second, Lakeroad, a technology mapper for FPGAs which
uses program synthesis and semantics extracted from Verilog to map
hardware designs to complex, programmable hardware primitives.


Full paper here: https://arxiv.org/abs/2408.15429


Regards,
John Levine, johnl@taugh.com, Taughannock Networks, Trumansburg NY
Please consider the environment before reading this e-mail. https://jl.ly

Return to the comp.compilers page.
Search the comp.compilers archives again.