- DOI: 10.4230/LITES-v005-i001-a003
- URN:
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}, doi = {10.4230/LITES-v005-i001-a003}, annote = {Keywords: caches, persistence analysis, WCET analysis} }
Feedback for Dagstuhl Publishing