Détails sur le séminaire

Abstract: The certification of real-time safety critical programs requires bounding their execution time. Due to the high impact of cache memories on memory access latency, modern Worst-Case Execution Time estimation tools include a cache analysis. The aim of this analysis is to statically predict if memory accesses result in a cache hit or a cache miss. This problem is undecidable in general, thus usual cache analyses perform some abstractions that lead to precision loss. One common assumption made to remove the source of undecidability is that all execution paths in the program are feasible. Making this hypothesis is reasonable because the safety of the analysis is preserved when adding spurious paths to the program model. However, classifying memory accesses as cache hits or misses is still hard in practice under this assumption, and efficient cache analysis usually involve additional approximations, again leading to precision loss. This thesis investigates the possibility of performing an optimally precise cache analysis under the common assumption that all execution paths in the program are feasible.
We formally define the problems of classifying accesses as hits and misses, and prove that they are NP-hard or PSPACE-hard for common replacement policies (LRU, FIFO, NMRU and PLRU). However, if these theoretical complexity results legitimate the use of additional abstraction, they do not preclude the existence of algorithms efficient in practice on industrial workloads.
Because of the abstractions performed for efficiency reasons, cache analyses can usually classify accesses as Unknown in addition to Always-Hit (Must analysis) or Always-Miss (May analysis). Accesses classified as Unknown can lead to both a hit or a miss, depending on the program execution path followed. However, it can also be that they belong to one of the Always-Hit or Always-Miss category and that the cache analysis failed to classify them correctly because of a coarse approximation. We thus designed a new analysis for LRU instruction that is able to soundly classify some accesses into a new category, called Definitely Unknown, that represents accesses that can lead to both a hit or a miss. For those accesses, one knows for sure that their classification does not result from a coarse approximation but is a consequence of the program structure and cache configuration. By doing so, we also reduce the set of accesses that are candidate for a refined classification using more powerful and more costly analyses.
Our main contribution is an analysis that can perform an optimally precise analysis of LRU instruction caches. We use a method called block focusing that allows an analysis to scale by only analyzing one cache block at a time. We thus take advantage of the low number of candidates for refinement left by our Definitely Unknown analysis. This analysis produces an optimal classification of memory accesses at a reasonable cost (a few times the cost of the usual May and Must analyses).
We evaluate the impact of our precise cache analysis on the pipeline analysis. Indeed, when the cache analysis is not able to classify an access as Always-Hit or Always-Miss, the pipeline analysis must consider both cases. By providing a more precise memory access classification, we thus reduce the state space explored by the pipeline analysis and hence the WCET analysis time.
Aside from this application of precise cache analysis to WCET estimation, we investigate the possibility of using the Definitely Unknown analysis in the domain of security. Indeed, caches can be used as side-channel to extract some sensitive data from a program execution, and we propose a variation of our Definitely Unknown analysis to help a developer finding the source of some information leakage.



Jury:
PhD supervisors:
* David Monniaux, Grenoble Alpes University, France
* Claire Maïza, Grenoble Alpes University, France
Reviewers:
* Björn Lisper, Mälardalen University, Sweden
* Kenneth McMillan, Microsoft Research, Redmond, USA
Examiners:
* Frédéric Pétrot, Grenoble Alpes University, France
* Jan Reineke, Saarland University, Saarbrücken, Germany
* Hugues Cassé, Paul Sabatier University, Toulouse, France
* Sébastien Faucou, Nantes University, France