Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > comp.compilers > #3739
| Path | csiph.com!weretis.net!feeder9.news.weretis.net!news.misty.com!news.iecc.com!.POSTED.news.iecc.com!nerds-end |
|---|---|
| From | John R Levine <johnl@taugh.com> |
| Newsgroups | comp.compilers |
| Subject | Paper: Formal Performance and Compile Time Guarantees for Compiler Optimization Heuristics |
| Date | Sat, 22 Aug 2026 18:35:01 -0400 |
| Organization | Compilers Central |
| Sender | johnl%iecc.com |
| Approved | comp.compilers@iecc.com |
| Message-ID | <26-08-002@comp.compilers> (permalink) |
| MIME-Version | 1.0 |
| Content-Type | text/plain; charset="UTF-8" |
| 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 |
| X-submission-address | compilers@iecc.com |
| X-moderator-address | compilers-request@iecc.com |
| X-FAQ-and-archives | http://compilers.iecc.com |
| Xref | csiph.com comp.compilers:3739 |
Show key headers only | View raw
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
Back to comp.compilers | Previous | Next | Find similar | Unroll thread
Paper: Formal Performance and Compile Time Guarantees for Compiler Optimization Heuristics John R Levine <johnl@taugh.com> - 2026-08-22 18:35 -0400
csiph-web