Fully Symbolic Analysis of Loop Locality: Using Imaginary Reuse to Infer Real Performance

This paper introduces a fully symbolic compiler analysis that derives cache locality as polynomials for affine loop nests, achieving 99.6% accuracy in predicting data movement across 41 scientific kernels with negligible prediction time after an average 41-second derivation.

The Gist

Imagine you are a chef trying to cook a massive banquet. You have a small kitchen counter (the cache) where you keep ingredients you are currently using, and a giant, slow pantry (the main memory) where everything else is stored.

Every time you need an ingredient, you check the counter first.

• Hit: If it's there, you grab it instantly. (Fast!)
• Miss: If it's not there, you have to walk all the way to the pantry, get it, and bring it back. (Slow and wasteful!)

The goal of this paper is to answer a very specific question: "Before we even start cooking, can we predict exactly how many times we will have to run to the pantry, just by looking at the recipe?"

The Problem: The "First Time" Dilemma

Traditionally, computer scientists tried to predict this by looking at patterns. But they hit a wall with the very first time you grab an ingredient.

• If you grab a spice for the first time, it's not a "reuse" (you haven't used it before).
• In math terms, the time between "now" and "the last time you used this" is infinite.
• But you can't do math with infinity easily. It breaks the equations.

If you ignore these first-time grabs, your prediction is wrong because you miss the "cold start" penalty. If you count them as infinity, your math explodes.

The Solution: "Imaginary Reuses" (The Time Travel Trick)

The authors came up with a brilliant, slightly magical idea called Imaginary Reuses.

Imagine that instead of cooking just one banquet, you are cooking the same banquet an infinite number of times in a row.

• Run 1: You grab the salt for the first time. It's a "cold miss."
• Run 2: You grab the salt again. But wait! In this imaginary timeline, you just used it in Run 1. So, for Run 2, it counts as a "reuse."
• Run 3, 4, 5...: You keep reusing the salt.

By pretending the program runs forever, every single ingredient eventually becomes a "reuse." The "infinite" gap disappears because the gap is now just the time between the end of Run 1 and the start of Run 2.

This allows the computer to turn the messy, infinite problem into a neat, finite math equation. They call these "Imaginary Reuses" because they are fake (you aren't actually running the program forever), but they are necessary to make the math work.

The Magic Formula: Turning Recipes into Polynomials

Once they fix the "first time" problem with this time-travel trick, they can derive a Polynomial.

Think of a polynomial as a super-recipe formula.

• Old way: "If your matrix is 10x10, you miss 50 times. If it's 20x20, you miss 200 times." (You have to calculate this for every single size).
• New way: "Your misses = $\frac{1}{2} \times (\text{Size})^2 + \frac{1}{\text{Block Size}}$."

This formula works for any size. Whether you are cooking for 10 people or 10 million, you just plug the number into the formula, and boom, you know exactly how many trips to the pantry you'll make.

How They Built the Machine (The Compiler)

The authors built a special tool (a compiler) that reads code written in a specific style (called Affine Loops).

1. Translation: It translates the code into a geometric shape (a polytope).
2. Counting: It counts every single time an ingredient is grabbed, using advanced math to group them by how far apart they are in time.
3. Prediction: It spits out that magic polynomial formula.

The Results: Why Should You Care?

They tested this on 41 different scientific programs (like simulating weather or crunching data for AI).

• Speed: The tool took about 41 seconds to analyze a program and write the formula. Once the formula exists, predicting the result for any future scenario takes less than a millisecond.
• Accuracy: It was 99.6% accurate compared to actually running the program on real hardware.
• The "Moving Cliff" Fix: Old methods often guessed when the performance would drop, but they were usually a little early or late. This method gets the timing perfect.

The "Square Root of 2" Rule

There is a famous rule of thumb in computing: "If you double your data size, you need to increase your cache size by $\sqrt{2}$ (about 1.41) to keep performance the same."

This paper proves that rule is too simple.
Using their new formulas, they showed that sometimes the rule works, but other times, the relationship is much more complex. They can tell you the exact number of misses, not just a rough estimate. It's like having a GPS that tells you the exact traffic delay, rather than just saying "it might be a little slow."

Summary

In short, this paper teaches computers how to predict the future of memory usage by:

1. Pretending the program runs forever to fix the "first time" math problem (Imaginary Reuses).
2. Turning the code into a mathematical formula (Polynomial) that works for any size.
3. Giving us a tool that is fast, incredibly accurate, and understands the deep math of how computers think.

It's like moving from guessing how long a trip will take based on the weather, to having a perfect equation that calculates the exact travel time based on the car, the road, and the distance.

Technical Summary

Here is a detailed technical summary of the paper "Fully Symbolic Analysis of Loop Locality: Using Imaginary Reuse to Infer Real Performance."

1. Problem Statement

Modern data-intensive applications rely heavily on memory locality for performance. While compilers and transformation frameworks optimize for locality, existing analysis techniques suffer from significant limitations:

• Lack of Full Symbolism: Traditional symbolic analyses (e.g., those using integer-set equations) are limited to linear expressions. They cannot derive quadratic or reciprocal terms required to accurately model cache scaling (e.g., how miss ratios change with symbolic cache sizes or loop bounds).
• The "Cold-Start" Dilemma: In standard locality theory (Denning Recursion), the first access to a memory location (first-touch) has an infinite reuse interval (RI). This causes the working-set size to diverge to infinity, making symbolic analysis of finite programs impossible without excluding cold misses (which are critical for performance) or accepting infinite results.
• Empirical vs. Analytical: Current scaling rules (like the $\sqrt{2}$ rule) are empirical approximations. They lack the precision to predict exact miss ratios or distinguish between different scaling behaviors that follow the same rule.

2. Methodology

The authors propose Algebraic Locality, a fully symbolic framework that derives cache performance metrics (miss count and miss ratio) as polynomials of program and cache parameters.

A. Core Theory: Imaginary Reuses and Infinite Repeat

To resolve the cold-start dilemma, the paper introduces the concept of Infinite Repeat:

• Concept: Theoretically, the program runs an infinite number of times.
• Imaginary Reuse: A "first-touch" access in the first run becomes a "reuse" in the second run (connecting the last access of run $r$ to the first access of run $r+1$).
• Finite RI: This assigns a finite Reuse Interval (RI) to every access, even the first ones. The RI of an imaginary reuse is at most the program length ($n$).
• Correctness: The authors prove Working-set Correctness, showing that under Infinite Repeat, Denning Recursion correctly computes the average working-set size (footprint) for deterministic sequences without stochastic assumptions.

B. Symbolic Derivation Process

1. Timestamp Space Construction: The compiler translates affine loop nests (from MLIR's Affine dialect) into a parametric polytope representing the sequence of memory accesses (timestamps).
2. Reuse Interval (RI) Distribution:
   • The system identifies "backward reuses" (accessing the same data as a previous access).
   • Using Integer Set Programming and Barvinok decomposition, the compiler counts the occurrences of each symbolic RI value.
   • The result is a Piecewise Quasi-polynomial distribution of RIs.
3. Polynomial Derivation:
   • The RI distribution is fed into Denning Recursion to derive the Miss Ratio Polynomial $m(x)$ and Working-Set Size Polynomial $s(x)$.
   • The theory introduces Imaginary Reuse Invariance: The sum of (RI value $\times$ portion) must equal the total data size. This serves as a symbolic test to verify the correctness of the derived polynomials.
4. LRU Approximation & Correction:
   • The derived miss ratio assumes the infinite repeat (where first touches are hits).
   • To get the Real Performance, the compiler "undoes" the infinite repeat by converting the imaginary reuse hits back into cold-start misses, adjusting the final miss ratio polynomial.

C. Compiler Implementation

• Built on MLIR (Affine Dialect).
• Uses a two-pass algorithm:
  1. Translate loops to parametric polytopes.
  2. Count RI lengths and portions using integer-set libraries (ISL/Barvinok).
• Handles affine loop bounds, imperfectly nested loops, and conditional branches.

3. Key Contributions

1. Algebraic Locality Theory: A new theoretical framework that derives cache performance as closed-form algebraic expressions (polynomials), capable of representing quadratic and reciprocal relationships.
2. Imaginary Reuse Mechanism: A novel technique to assign finite RIs to first-touch accesses, enabling the application of Denning Recursion to finite, deterministic programs while maintaining mathematical rigor.
3. Formal Properties: Proofs of Working-set Correctness and RI Sum Invariance, providing a mathematical guarantee for the derived polynomials.
4. Symbolic Compiler: An implementation that analyzes affine loops to produce symbolic locality polynomials in linear time relative to the number of symbolic RI values.
5. Min-Max Scaling Analysis: The first method to automatically derive exact cache scaling rules (e.g., specific cache sizes required to bound miss ratios) rather than relying on empirical rules like $\sqrt{2}$.

4. Evaluation Results

The compiler was evaluated on 41 benchmarks (30 from PolyBench, 11 from Einsum tensor operations) against cache simulations (Cachegrind) and hardware counters (Nvidia GB10).

• Accuracy:
  • Data Movement Prediction: 99.6% accuracy across all tests (comparing predicted hit/miss sequences to simulated ones).
  • Miss Ratio: Average error is 1.1% for fully associative caches and 1.3% for 12-way set-associative caches.
  • Comparison: Significantly outperforms previous tools that rely on empirical rules or numerical simulation.
• Performance:
  • Derivation Time: Average of 41 seconds for non-fused loops; up to 224 seconds for complex fused loops (due to higher dimensionality).
  • Prediction Time: < 1 millisecond to predict miss counts for any input size or cache configuration once polynomials are derived.
• Scaling Analysis: Successfully demonstrated that while different programs may follow the $\sqrt{2}$ scaling rule, their actual miss ratios can differ by a factor of two, a nuance captured only by the symbolic polynomials.

5. Significance

• Paradigm Shift: Moves locality analysis from empirical estimation and numerical simulation to exact symbolic derivation.
• Compiler Optimization: Provides compilers with precise, parameterized models of data movement, enabling better decisions for loop fusion, tiling, and prefetching without needing to run the code.
• Scalability: Allows architects and developers to predict performance for arbitrary problem sizes and cache configurations instantly, without re-simulation.
• Theoretical Foundation: Establishes that while deriving RI distributions is theoretically NP-hard (proven via 3-SAT reduction), practical affine programs with low-dimensional polytopes can be solved efficiently using Barvinok's algorithm.

In summary, this paper presents a breakthrough in compiler analysis by transforming the complex, stochastic problem of cache locality into a deterministic, algebraic problem solvable via symbolic polynomials, offering unprecedented precision and speed in performance prediction.