From Newsgroup: comp.compilers
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
--- Synchronet 3.22a-Linux NewsLink 1.2