Model Checking of Cache for WCET Analysis Refinement

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.