vix.ing · top · new · best · stats · spec

Model Checking of Cache for WCET Analysis Refinement

2017/01/27 by Valentin Touzeau, Touzeau, Valentin, Claire Maïza +3
Computer Science · #Distributed systems and fault tolerance #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Parallel Computing and Optimization Techniques #Programming Languages (cs.PL) #Real-Time Systems Scheduling

paper · pdf · doi:10.48550/arxiv.1701.08030

openalex publication_date 2017/01/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Related