Optimizing Program Efficiency with Global Profitability Heuristics
Explore how Global Profitability Heuristics mitigate phase ordering problems and enhance program efficiency through CFG PEG conversion, equality saturation, and more. Learn about non-destructive updates and referential transparency in program representation.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Ross Tate Ross Tate, Mike Stepp, Zach Tatlock, Sorin Lerner University of California, San Diego
Phase Ordering Problem Original Program Optimized Program Optimizations Local Profitability Heuristics
Program Expression Graph CFG PEG Conversion
Equality Saturation Global Profitability Heuristic CFG PEG Conversion PEG CFG Conversion Equality Saturation
Global Profitability Heuristic Global Profitability Heuristic CFG PEG Conversion PEG CFG Conversion Equality Saturation
PEGCFG Conversion Global Profitability Heuristic CFG PEG Conversion PEG CFG Conversion Equality Saturation
Mitigates Phase Ordering Problem Non-destructive updates allow exponential search Global Profitability Heuristic Explore first, then decide Translation Validation Verify translations using equality saturation Global Profitability Heuristic CFG PEG Conversion PEG CFG Conversion Equality Saturation
sum = 0; for (i = 0; i < 10; i++) sum += 4 * i; return sum; Global Profitability Heuristic CFG PEG Conversion PEG CFG Conversion Equality Saturation
sum = 0; for (i = 0; i < 10; i++) sum += 4 * i; return sum; * 4 4 1 1 Complete Representation Referentially Transparent No Intermediate Variables 0 0 + + 1 1 Global Profitability Heuristic CFG PEG Conversion PEG CFG Conversion Equality Saturation
Identify Equalities PEG Node Granularity Equality Axioms X. 4*X = (X 2) X. 4*X = (X 2) << * 2 2 4 4 1 1 0 0 + + 1 1 Global Profitability Heuristic CFG PEG Conversion PEG CFG Conversion Equality Saturation
X. 4*X = (X2) X,Y. 4* (X, Y) = (4*X, 4*Y) 1 1 X,Y,Z. X*(Y+Z) = X*Y+ X*Z << * + + 2 2 4 4 1 1 * * 4 4 0 0 + + 4 4 X. X*0 = 0 0 0 * * 1 1 4 4 1 1 4 4 X. X*1 = X Global Profitability Heuristic CFG PEG Conversion PEG CFG Conversion Equality Saturation
1 1 << * + + 2 2 4 4 1 1 * * 4 4 0 0 + + 4 4 0 0 * 1 1 4 4 1 1 Global Profitability Heuristic CFG PEG Conversion PEG CFG Conversion Equality Saturation
1 1 << * + + 2 2 Profitability Heuristic 4 4 1 1 * Global * 4 4 0 0 + + 4 4 0 0 * 1 1 4 4 1 1 Global Profitability Heuristic CFG PEG Conversion PEG CFG Conversion Equality Saturation
1 1 0 0 + + 4 4 Global Profitability Heuristic CFG PEG Conversion PEG CFG Conversion Equality Saturation
sum = 0; for(j = 0; j < 40; j += 4) sum += j; return sum; 1 1 0 0 + + 4 4 Global Profitability Heuristic CFG PEG Conversion PEG CFG Conversion Equality Saturation
sum = 0; for(i = 0; i < 10; i++) sum += 4 * i; return sum; sum = 0; for(j = 0; j < 40; j += 4) sum += j; return sum; Loop Induction Variable Strength Reduction Global Profitability Heuristic CFG PEG Conversion PEG CFG Conversion Equality Saturation
Optimizations composed from simple rules Loop Induction Variable Strength Reduction Loop-Operation Factoring Loop-Operation Distributing Inter-Loop Strength Reduction Temporary Object Removal Partial Inlining Global Profitability Heuristic CFG PEG Conversion PEG CFG Conversion Equality Saturation
Global Profitability Heuristic CFG PEG Conversion PEG CFG Conversion Equality Saturation
Global Profitability Heuristic Heuristic Global Profitability CFG PEG Conversion Conversion CFG PEG PEG CFG Conversion Conversion PEG CFG Equality Saturation Saturation Equality Algorithm provided in the Technical Report Model heap with values having linear types
Global Profitability Heuristic CFG PEG Conversion PEG CFG Conversion Equality Saturation Tarjan s Union-Find Algorithm tracks equivalence classes in the E-PEG Rete Pattern Matching Algorithm incrementally finds significant nodes in the E-PEG Equality Analyses: PEG Operator Axioms Language-Specific Axioms Domain-Specific Axioms
Global Profitability Heuristic CFG PEG Conversion PEG CFG Conversion Equality Saturation Pseudo-Boolean Solver Assign a cost to each operation in the E-PEG Impose constraints for a well-formed PEG Minimize the cost of the selected PEG
Observed Emergent Optimizations Traditionally need to be explicitly implemented Domain-Specific Analyses: 7% runtime improvement on Java ray tracer Compilation of SpecJVM (per method): 1030 programs found in less than 200MB memory Average compilation time per stage: Global Profitability Heuristic 1499 msec Global Profitability Heuristic CFG PEG Conversion Conversion CFG PEG PEG CFG Conversion Conversion PEG CFG Equality Saturation Saturation Equality 14 msec 88 msec 1499 msec 43 msec
CFGPEG Conversion ? Equality Saturation CFG PEG Conversion Validation of Soot optimizer on SpecJVM: 98% of optimized methods successfully validated Optimization bug found within remaining 2%
P Powerful Simultaneous Exponential Search Emergent Optimizations E Extensible Cooperative Equality Analyses Domain-Specific Axioms G General Optimization Translation Validation
E-Graphs Denali: Basic Block Assembly Superoptimizer Simplify: Theorem Prover Representations Thinned-Gated SSA Lucid programming language Value Dependence Graph Dependence Flow Graph Program Dependence Graph/Web Rewrite-Based Optimizers TAMPR ASF+SDF Stratego
