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

Groups > comp.compilers > #3739 > unrolled thread

Paper: Formal Performance and Compile Time Guarantees for Compiler Optimization Heuristics

Back to article view | Back to comp.compilers

Contents

  Paper: Formal Performance and Compile Time Guarantees for Compiler Optimization Heuristics John R Levine <johnl@taugh.com> - 2026-08-22 18:35 -0400

#3739 — Paper: Formal Performance and Compile Time Guarantees for Compiler Optimization Heuristics

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

[toc] | [standalone]

Back to top | Article view | comp.compilers

csiph-web