Source-linked AI summary
Ascertaining Uncertainty for Efficient Exact Cache Analysis
Valentin Touzeau, Claire Maïza, David Monniaux, Jan Reineke
TL;DR
Static cache analysis must classify memory accesses precisely, but classical abstract interpretations leave some accesses unknown, affecting WCET and side-channel analyses. The paper introduces an existence-based abstract interpretation and exact model-checking refinement, using the first phase to prune the second. It precisely classifies accesses at reasonable cost, while its evaluation scope is limited to single-level LRU instruction caches at LLVM bitcode level.
Problem
Classical cache analysis leaves some accesses unknown even though they may always hit, always miss, or vary across executions, limiting precision for WCET and side-channel analysis.
Method
The approach combines a novel abstract interpretation that proves existential hit or miss behavior with model checking based on an exact cache-replacement abstraction.
Results
The method precisely classifies accesses as always hits, always misses, or mixed, with abstract-interpretation results reducing model-checking complexity.
Takeaways & Limitations
Combining abstract interpretation with model checking provides optimal precision for the modeled LRU cache while keeping analysis cost reasonable.
Takeaways & Limitations
The analysis is limited to a single-level LRU instruction cache and operates on LLVM bitcode rather than industrial machine-code configurations.
Abstract
from arXiv · showhide
Static cache analysis characterizes a program's cache behavior by determining in a sound but approximate manner which memory accesses result in cache hits and which result in cache misses. Such information is valuable in optimizing compilers, worst-case execution time analysis, and side-channel attack quantification and mitigation.Cache analysis is usually performed as a combination of `must' and `may' abstract interpretations, classifying instructions as either `always hit', `always miss', or `unknown'. Instructions classified as `unknown' might result in a hit or a miss depending on program inputs or the initial cache state. It is equally possible that they do in fact always hit or always miss, but the cache analysis is too coarse to see it.Our approach to eliminate this uncertainty consists in (i) a novel abstract interpretation able to ascertain that a particular instruction may definitely cause a hit and a miss on different paths, and (ii) an exact analysis, removing all remaining uncertainty, based on model checking, using abstract-interpretation results to prune down the model for scalability.We evaluated our approach on a variety of examples; it notably improves precision upon classical abstract interpretation at reasonable cost.
1 Introduction
Cache analysis must distinguish accesses that always hit, always miss, or vary across executions, yet classical abstractions leave some accesses unknown. The paper combines a novel abstract interpretation with model checking to remove this uncertainty while reducing model-checking complexity.
- Caches bridge the processor–memory speed gap by serving recently accessed data at lower latency than main memory.
- Unknown cache accesses can grossly overestimate WCET because analyses must account for both hit and miss possibilities.
- Classical cache analysis identifies accesses that always hit or always miss but leaves others unknown because its abstractions are incomplete.
- The approach adds an abstract interpretation proving that accesses may hit, miss, or both on different executions.
- Model checking then refines remaining unknown classifications using an exact cache-policy abstraction, while abstract-interpretation results simplify the model.
- The combined method is necessary for tractability because model checking alone does not scale, despite resolving all accesses.
2 Background: Caches and Static Cache Analysis
Caches store recently accessed memory blocks in small, fast memories, while static cache analysis abstracts reachable cache states to classify accesses as hits, misses, or unknown.
- Caches: Caches partition memory into blocks mapped to cache sets, whose associativity limits how many blocks each set can hold.Replacement policies decide which block to evict after a miss, and sets are generally analyzed independently.
- Caches: Under LRU, a block is cached exactly when its age—the number of distinct same-set blocks accessed since its last access—is below associativity k.Unaccessed blocks have age ∞, and ages are truncated at k in the cache-state model.
- Programs as Control-flow Graphs: Programs are modeled as control-flow graphs whose edges carry accessed memory-block addresses, with all graph paths treated as feasible.Multiple edges may represent alternative blocks accessed by one instruction; functional instruction semantics are omitted.
- Collecting Semantics: Collecting semantics records all concrete cache states reachable at each control location, but explicitly computing them is infeasible.Abstract interpretation therefore uses compact domains that overapproximate large sets of concrete states.
- Classical Abstract Interpretation: Classical may and must analyses use age bounds to soundly prove that accesses may miss or must hit, leaving other accesses unknown.Their soundness is stated as safe approximation of the collecting semantics.
3 Abstract Interpretation for Definitely Unknown
The paper introduces EH and EM abstract interpretations to establish whether accesses can hit or miss on some executions, identifying definitely unknown accesses before model checking.
- Definitely Unknown: An access is definitely unknown when one concrete execution makes it miss and another makes it hit.This existential two-execution property differs from classical analyses that establish properties over all executions.
- EH and EM Analyses: EH computes safe upper bounds on minimum ages to establish exists-hit cases, while EM computes safe lower bounds on maximum ages to establish exists-miss cases.A hit is possible when the minimum age is below associativity; a miss is possible when the maximum age is sufficiently large.
- Example: In the loop example, accesses to v and w miss initially and hit later, so EH and EM together classify them as definitely unknown where classical analysis reports unknown.This holds for fully associative caches with associativity 2 or greater.
- EH and EM Analyses: The EH domain represents hyperproperties over sets of reachable cache states rather than properties of individual states.Its abstract state combines bounds on minimal ages with a must-analysis component for upper age bounds.
- EH and EM Analyses: The EH transformer updates minimal-age bounds according to whether the accessed block is younger or older, while preserving soundness under LRU updates.The corresponding local transformer and join operators are proven correct.
- Analysis Flow: EH and EM results classify some accesses as definitely unknown and reduce model-checking work for accesses classified as exists-hit or exists-miss.For an exists-hit access, model checking only needs to determine whether a miss is possible to complete classification.
4 Cache Analysis by Model Checking
The analysis combines classical abstract interpretation, a definitely-unknown analysis, and focused-cache model checking to classify every access as always hit, always miss, or definitely unknown without losing precision relative to the concrete cache model.
- Abstract-interpretation phase: The abstract-interpretation phase uses may, must, ExistsHit, and ExistsMiss analyses to classify accesses or identify remaining uncertainty.Accesses classified as ExistsHit and ExistsMiss can help reduce subsequent model-checking effort.
- Model-checking phase: The model-checking phase is sound and complete relative to the control-flow-graph model, leaving every access classified as always hit, always miss, or definitely unknown.The analysis assumes that every control-flow path is semantically feasible.
- Model-checking phase: The model checker receives a finite-state program-and-cache model focused on the particular memory block being classified.The focused model discards program and cache information that cannot affect that block’s caching status.
- Focused cache model: For an LRU cache, the focused model tracks the set of blocks younger than the target block, representing an uncached target with ε.The target is cached exactly when its age is less than the associativity k.
- Focused cache model: The focused cache update is sound and complete with respect to the concrete cache update, so it classifies the focused access without precision loss.The paper states that the focused collecting semantics is exactly the abstraction of the concrete collecting semantics.
5 Related Work
Related approaches also refine cache analysis using program semantics, but they use different analysis levels and techniques; the paper compares their scalability while noting that precision comparisons remain difficult.
- Model-checking refinements: Chattopadhyay and Roychoudhury refine AI-unknown accesses with bounded model checking that incorporates program semantics.Their approach enriches the source program with annotations counting conflicting accesses.
- Semantic refinement: Chu et al. use symbolic execution and an SMT solver to prune infeasible paths when refining cache-analysis results.The paper compares the scalability of their approach with its own.
- Relationship to WCET analysis: The paper’s refined cache classifications complement WCET analyses, while related model-checking work that omits caches does not address the same low-level feature.The cited WCET work uses classical cache classifications as a basis but does not model cache behavior itself.
6 Experimental Evaluation
Experiments on TACLeBench evaluate precision gains, definitely-unknown pruning, and full-analysis efficiency, showing more classifications and substantially fewer model-checking calls under a focused LRU instruction-cache model.
- Scope: The analysis is limited to a single-level LRU instruction cache at LLVM bitcode level rather than industrial processor-specific binary-cache configurations.Implementing or interfacing with a full industrial-strength analyzer and pointer-value analysis is outside the paper’s scope.
- Experimental setup: The evaluation uses TACLeBench with an initially empty cache configured as 8 instructions per block, 4 ways, and 8 cache sets.Benchmark size is measured by CFG blocks, where each block contains instructions mapped to the same memory block.
- Precision: More than 60% of benchmarks improve in always-hit or always-miss classifications after model checking, and 45% improve by more than 5%.The comparison is against the pure abstract-interpretation phase.
- Definitely-unknown analysis: The definitely-unknown analysis reduces model-checking calls by around a factor of 100 on some larger benchmarks, and to zero on the three smallest.For 28 of 46 benchmarks, fewer than 10 model-checking calls remain.
- Definitely-unknown analysis: The total model-checking execution time falls by a geometric-mean factor of 3.7 compared with using only may and must results.The definitely-unknown analysis itself takes less than one second on every benchmark.
- Model scalability: The focused cache model is necessary for scalability: without it, all but the six smallest benchmarks time out after one hour.The results also indicate that one model classifying all accesses at once is practically infeasible.
- Model-checking efficiency: With AI-based model simplifications, the maximum execution time of individual model-checking calls is always lower, although the mean can increase after cheap calls are suppressed.Some benchmarks lack a no-AI result because analysis did not terminate within one hour.
- Comparison with related work: For statemate, the approach makes 3 or 0 calls and finishes in under 3 seconds or 1.5 seconds, versus 395 seconds for one related tool; for ndes, it takes under one second versus 38 seconds.The paper cautions that a careful comparison of analysis precision remains to be done.
7 Conclusion and Perspectives
The paper combines abstract interpretation and model checking to precisely classify all accesses to an LRU cache at reasonable cost, while identifying limitations and possible improvements related to path feasibility.
- The approach precisely classifies all accesses to an LRU cache at reasonable cost.
- Abstract interpretation classifies most accesses, while model checking classifies the remaining accesses.The combination is presented as the basis for precise LRU-cache access classification.
- The analysis assumes that all control-flow-graph paths are feasible regardless of functional semantics.This is shared with other known abstraction-interpretation-based cache analyses.
- Possible improvements include encoding functional semantics into model checking or using trace partitioning or path focusing during abstract interpretation.
A Proofs for the Definitely-Unknown Abstract Interpretation
The appendix establishes soundness of the definitely-unknown abstract interpretation by proving local-transformer and join consistency, then deriving analysis soundness through finite fixed-point iteration.
- EH analysis: The EH abstract transformer updateEH soundly approximates its concrete counterpart updateC.
- EH analysis: The EH join operator is correct, so joined abstract states safely represent unions of reachable concrete states.
- EH analysis: The abstract EH semantics includes the collecting semantics: ∀v ∈V : RC(v) ∈γEH (REH (v)).
- Analysis soundness: Finite domains and finite ascending chains allow both collecting and abstract semantics to reach least fixed points through finite Kleene iteration.
- EM analysis: The EM transformer updateEM soundly approximates concrete cache updates, and its join combines lower age bounds using a maximum.The appendix states that EM soundness follows similarly after establishing transformer and join consistency.
B Proofs for Reduced Models in Model Checking
The appendix proves that the focused cache update abstracts the concrete LRU update exactly by inspecting cases based on whether the focused block and accessed block are present and their cache positions.
- The focused cache update is proved locally sound and complete with respect to the concrete cache update.
- The proof considers reachable cache states and separates states that do not contain the focused block from states that do.
- For states containing the focused block, the proof further distinguishes whether the accessed block is the focused block and whether eviction is relevant.
- When the accessed block differs, the proof examines whether it is younger than, older than, or absent from the cache, including least-recently-used cases.
- Each examined case preserves consistency between the concrete update and the focused abstract update.
C Additional Results from Experimental Evaluation
The additional experiments examine how cache configuration affects model-checking refinements and how the definitely-unknown and abstract-interpretation phases affect model-checking effort and model size.
- The evaluation treats missing plots as cases where a one-hour timeout was reached.
- Figures 10–12 report the number of accesses refined to hits or misses while varying block size, associativity, and cache sets.
- Figures 13–15 report the share of total accesses refined by model checking for each benchmark under corresponding cache configurations.
- Figures 16 and 17 evaluate the definitely-unknown analysis using model-checker call counts and cumulative model-checking time.
- The abstract-interpretation phase reduces model-checker calls, while the maximum model size remains quite close with and without that phase.Because there are fewer calls with the AI phase, the average model-checking cost may be larger.