Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.compilers > #3594 > unrolled thread

Generation of Compiler Backends from Formal Models of Hardware

Back to article view | Back to comp.compilers

Contents

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

#3594 — 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

[toc] | [standalone]

Back to top | Article view | comp.compilers

csiph-web