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.
Navigation
Nouvelles publications
- Quelques Publications
Récentes
(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
- David Monniaux, Sylvain Boulmé: Chamois: agile development of CompCert extensions for optimization and security
- 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
- Karine Altisen, Pierre Corbineau, Stéphane Devismes: Complexité certifiée d'algorithmes autostabilisants en rondes
- Karine Altisen, Alain Cournier, Geoffrey Defalque, Stéphane Devismes: Self-stabilizing synchronous unison in directed networks
- Bruno Ferres, Oussama Oulkaid, Ludovic Henrio, Mehdi Khosravian, Matthieu Moy, Gabriel Radanne, Pascal Raymond: Electrical Rule Checking of Integrated Circuits using Satisfiability Modulo Theory
- Léo Gourdin, Benjamin Bonneau, Sylvain Boulmé, David Monniaux, Alexandre Bérard: Formally Verifying Optimizations with Block Simulations
Offres d'emploi et stages
- Offres d'emploi et stages
(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] Modular Analysis for Formal Verification of Integrated Circuits at Transistor Level
- [Master] Analyzing fault parameters triggering timing anomalies
- [Master] Exploration by model-checking of timing anomaly cancellation in a processor