Return to the
comp.compilers page.
Search the
comp.compilers archives again.
| Related articles |
|---|
| Paper: Formal Performance and Compile Time Guarantees for Compiler Optimization Heuristics johnl@taugh.com (John R Levine) (2026-08-22) |
| From: | John R Levine <johnl@taugh.com> |
| Newsgroups: | comp.compilers |
| Date: | Sat, 22 Aug 2026 18:35:01 -0400 |
| Organization: | Compilers Central |
| Injection-Info: | gal.iecc.com; posting-host="news.iecc.com:2001:470:1f07:1126:0:676f:7373:6970"; logging-data="49307"; mail-complaints-to="abuse@iecc.com" |
| Keywords: | optimize, paper |
| Posted-Date: | 22 Aug 2026 18:35:58 EDT |
Nice little paper does a simple model of an inlining optimization and
shows it's equivalent to a well known game theory problem.
Abstract
Modern optimizing compilers rely on heuristic search algorithms for
NP-hard optimization problems, which can result in poor generated-code
performance and long or unpredictable compile times. These are considered
bugs by users, but verified compilers rarely reason beyond semantic
preservation. We propose verifying performance and compile time properties
of compiler passes. As a proof-of-concept, we formulate inline expansion
using a cost model estimating instruction-cache performance. We mechanize
this in Rocq, prove semantic preservation of the inlining transformation,
and verify the algorithm's monotone improvement, convergence-time bound,
and performance bounds for intermediate and final solutions.
https://arxiv.org/abs/2608.20137
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.