Model Checking of Cache for WCET Analysis Refinement
Valentin Touzeau (VERIMAG - IMAG), Claire Ma\"iza (VERIMAG - IMAG),, David Monniaux (VERIMAG - IMAG)

TL;DR
This paper enhances cache analysis for real-time systems' WCET estimation by applying model checking with a new LRU cache model, aiming to reduce over-approximation in timing analysis.
Contribution
It introduces a novel model checking approach for cache analysis with a new LRU cache model to improve WCET estimation accuracy.
Findings
Refined cache analysis reduces over-approximation in WCET estimates.
Model checking improves the precision of cache hit/miss classification.
New LRU cache model enhances analysis of hardware behavior.
Abstract
On real-time systems running under timing constraints, scheduling can be performed when one is aware of the worst case execution time (WCET) of tasks. Usually, the WCET of a task is unknown and schedulers make use of safe over-approximations given by static WCET analysis. To reduce the over-approximation, WCET analysis has to gain information about the underlying hardware behavior, such as pipelines and caches. In this paper, we focus on the cache analysis, which classifies memory accesses as hits/misses according to the set of possible cache states. We propose to refine the results of classical cache analysis using a model checker, introducing a new cache model for the least recently used (LRU) policy.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsReal-Time Systems Scheduling · Distributed systems and fault tolerance · Parallel Computing and Optimization Techniques
