Interactive Source-to-Source Optimizations Validated using Static Resource Analysis
summary
OptiTrust is an interactive source-to-source optimizer for C that uses a lightweight Separation-Logic-based static resource analysis to verify each transformation and always emits plain C code rather than a blackbox backend. The prototype reaches complex rewrites for matrix multiplication via 8 script steps that expand to 55 basic Transformations plus 61 ghost operations (first step alone runs 18 basics), and validates legality using inferred function and loop contracts and fractional ownership so transformations are provably safe.
AI-written summary · about
chapters (6)
- 0:00OptiTrust framework intro
- 2:10Motivation for interactive optimizations
- 3:34Matrix multiplication case
- 8:10Transformation scripts & annotations
- 14:15Validation with static analysis
- 17:54Conclusion & future work
related talks
19mFormally Verifying Optimizations with Block Simulations
23mFormally Verified Speculation and Deoptimization in a JIT Compiler
24mVerified Tensor-Program Optimization Via High-Level Scheduling Rewrites
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
47mHow an Optimizing Compiler Works
21mTowards Compiler-Guided Static Analysis
48mOptView2 - Helping the Compiler Generate Better Code
19mMinotaur: A SIMD-Oriented Synthesizing Superoptimizer