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)
- Karine Altisen, Alain Cournier, Geoffrey Defalque, Stéphane Devismes: Pour battre à l'unisson, il faut que tous les chemins viennent de Rome
- Erwan Jahier, Karine Altisen, Stéphane Devismes, Gabriel B. Sant'Anna: Model Checking of Distributed Algorithms using Synchronous Programs
- Karine Altisen, Stéphane Devismes, Anaïs Durand, Colette Johnen, Franck Petit: Self-stabilizing Systems in Spite of High Dynamics
- Karine Altisen, Alain Cournier, Geoffrey Defalque, Stéphane Devismes: Self-stabilizing Synchronous Unison in Directed Networks
- David Monniaux, Sylvain Boulmé: Chamois: agile development of CompCert extensions for optimization and security
- 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
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
- [Master] Adapting Hardware Platforms to a Multi-Core Response Time Analysis Framework
- [Master] Towards New Frontiers in Multi-Core Response Time Analysis?
- [Master] Analyzing fault parameters triggering timing anomalies
- [Master] Exploration by model-checking of timing anomaly cancellation in a processor