一句话：提出基于抽象解释的 LRU 缓存精确分析，兼顾高效与精确，并证明该分析问题一般 NP 完全。
针对最坏执行时间分析与安全场景，需要静态判定内存访问在 LRU 缓存上是否命中。传统基于区间抽象的抽象解释方法速度快但精度不足；已有精确分析需调用模型检测，代价高昂。本文提出一种基于抽象解释的 LRU 缓存分析方法，在保持与模型检测相同的精确分类能力的同时，接近传统方法的效率，实验中获得数个数量级的加速。作为次要贡献，作者证明一般的 LRU 缓存分析问题是 NP 完全的。
For applications in worst-case execution time analysis and in security, it is desirable to statically classify memory accesses into those that result in cache hits, and those that result in cache misses. Among cache replacement policies, the least recently used (LRU) policy has been studied the most and is considered to be the most predictable. The state-of-the-art in LRU cache analysis presents a tradeoff between precision and analysis efficiency: The classical approach to analyzing programs running on LRU caches, an abstract interpretation based on a range abstraction, is very fast but can be imprecise. An exact analysis was recently presented, but, as a last resort, it calls a model checker, which is expensive. In this paper, we develop an analysis based on abstract interpretation that comes close to the efficiency of the classical approach, while achieving exact classification of all memory accesses as the model-checking approach. Compared with the model-checking approach we observe speedups of several orders of magnitude. As a secondary contribution we show that LRU cache analysis problems are in general NP-complete.
@article{paperbot651,
title = {Fast and exact analysis for LRU caches},
author = {Valentin Touzeau and Claire Maïza and David Monniaux and Jan Reineke},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290367}
}