Groups | Search | Server Info | Login | Register

Groups > comp.compilers > #3594

Generation of Compiler Backends from Formal Models of Hardware

Show all headers | View raw

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

Back to comp.compilers | Previous | Next | Find similar

Thread

Generation of Compiler Backends from Formal Models of Hardware John R Levine <johnl@taugh.com> - 2024-08-30 22:36 -0400

csiph-web