The naive vision of cache memory is that it stores “the most recently accessed data”. In reality, each memory block can be stored in one specific part of the cache memory (the cache set suitable for the block’s address), and furthermore the block evicted from the cache set is not necessarily the least recently used (LRU). In fact, many processors implement “pseudo-LRU” policies cheaper to implement in hardware and that have similar practical performance. For safety-critical hard real time applications, it is necessary to prove bounds on the worst-case execution time (WCET). For this, it is necessary to know which accesses are cache hits or misses. There are several good analyses, including “exact” ones, for LRU caches in the scientific literature. There are no such good analyses for pseudo-LRU policies. In fact, it can be shown that static analysis for pseudo-LRU policies belongs to higher complexity classes than for LRU. The topic of the internship (possibly leading to a thesis) is to research good and practically efficient analysis for pseudo-LRU policies.
Browsing
New publications
- Some Recent Publications
(Ressources Partagées)
- Erwan Jahier, Karine Altisen, Stéphane Devismes: Exploring Worst Cases of Self-stabilizing Algorithms using Simulations
- Oussama Oulkaid, Bruno Ferres, Matthieu Moy, Pascal Raymond, Mehdi Khosravian, Ludovic Henrio, Gabriel Radanne: A Transistor Level Relational Semantics for Electrical Rule Checking by SMT Solving
- Léo Gourdin: Lazy Code Transformations in a Formally Verified Compiler
- Léo Gourdin, Benjamin Bonneau, Sylvain Boulmé, David Monniaux, Alexandre Bérard: Formally Verifying Optimizations with Block Simulations
- Karine Altisen, Stéphane Devismes, Anaïs Durand, Colette Johnen, Franck Petit: Self-stabilizing Systems in Spite of High Dynamics
- David Monniaux, Sylvain Boulmé: Chamois: agile development of CompCert extensions for optimization and security
- Karine Altisen, Alain Cournier, Geoffrey Defalque, Stéphane Devismes: Self-stabilizing synchronous unison in directed networks
- Erwan Jahier, Karine Altisen, Stéphane Devismes, Gabriel B. Sant'Anna: Model Checking of Distributed Algorithms using Synchronous Programs
Jobs and internships
- Jobs
and internships
(Ressources Partagées)
- [Master] Implementation of critical applications on multi-core: execution mode analysis to reduce interferences
- [PostDoc] Implementation of critical applications on multi-core: execution mode analysis to reduce interferences
- [Funded PhD] Modular Analysis for Formal Verification of Integrated Circuits at Transistor Level
- [Funded PhD] Improving Diagnosis for a Formal Verification Tool for Electrical Circuits at Transistor Level
- [Master] Analyzing fault parameters triggering timing anomalies
- [Master] Exploration by model-checking of timing anomaly cancellation in a processor
