Ascertaining uncertainty for efficient exact cache analysis

DOI10.1007/978-3-319-63390-9_2MaRDI QIDQ2164207zbMATH OpenOpenAlexFDO

Authors Valentin Touzeau, David Monniaux, Jan Reineke, Claire Maiza

Publication date 12 August 2022

Full work available at URL https://arxiv.org/abs/1709.10008

zbMATH Keywords

abstract cache statescache analysisclassical abstract interpretationWCET analysisworst-case execution time (WCET)

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: 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.

Recommendations

• Cache behavior prediction by abstract interpretation
• Cache behavior prediction by abstract interpretation
• Path sensitive cache analysis using cache miss paths
• The complexity gap in the static analysis of cache accesses grows if procedure calls are added
• Data cache organization for accurate timing analysis

Cited in

(6)

• On the analysis of random replacement caches using static probabilistic timing methods for multi-path programs
• Cache behavior prediction by abstract interpretation
• Data cache organization for accurate timing analysis
• Cache behavior prediction by abstract interpretation
• Path sensitive cache analysis using cache miss paths
• The complexity gap in the static analysis of cache accesses grows if procedure calls are added

This page was built for publication: Ascertaining uncertainty for efficient exact cache analysis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2164207)