Creative Commons Attribution 3.0 Germany license
We clarify the notion of cache persistence and contribute to the understanding of persistence analysis for caches with least-recently-used replacement.To this end, we provide the first formal definition of persistence as a property of a trace semantics. Based on this trace semantics we introduce a semantics-based, i.e., abstract-interpretation-based persistence analysis framework.We identify four basic persistence analyses and prove their correctness as instances of this analysis framework.Combining these basic persistence analyses via two generic cooperation mechanisms yields a lattice of ten persistence analyses.Notably, this lattice contains all persistence analyses previously described in the literature. As a consequence, we obtain uniform correctness proofs for all prior analyses and a precise understanding of how and why these analyses work, as well as how they relate to each other in terms of precision.
@Article{reineke:LITES-v005-i001-a003,
author = {Reineke, Jan},
title = {{The Semantic Foundations and a Landscape of Cache-Persistence Analyses}},
journal = {Leibniz Transactions on Embedded Systems},
pages = {03:1--03:52},
ISSN = {2199-2002},
year = {2018},
volume = {5},
number = {1},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LITES-v005-i001-a003},
URN = {urn:nbn:de:0030-drops-192748},
doi = {10.4230/LITES-v005-i001-a003},
annote = {Keywords: caches, persistence analysis, WCET analysis}
}