Combining Path and Cache Analyses

De Ensiwiki
Aller à : navigation, rechercher
  • Where? Verimag lab, IMAG building
  • Who? Claire Maiza, Catherine Vigouroux, Valentin Touzeau (contact: prenom.nom@univ-grenoble-alpes.fr)
  • What?

CPUs are usually much faster than the main memory. Thus, to avoid the processor being stalled waiting for data coming from the memory, modern architectures make heavy use of small but fast memories called caches. The basic idea is to keep in the cache a copy of blocks that are frequently accessed to retrieve them faster.

We are currently developing a tool[1] at Verimag to statically analyze programs and caches. This tool is able to classify memory accesses into "accessed block is guaranteed to be in the cache" and "accessed block is guaranteed not to be in the cache". This information can then be used - for example - to prove that the execution time of the program can not exceed a given bound.

This analysis (performed by abstract interpretation) relies on the hypothesis that all the execution paths in the program are feasible to avoid misclassification of blocks. This is however not the case (example: if (x < 5) {if (x >= 5) {printf("Unfeasible");}} ) and can lead to precision loss during the analysis.

The aim of this internship is to improve the precision of the existing cache analysis by combining it with a path analysis that would eliminate some unfeasible paths. In addition, one can be interesting in focussing the path analysis on a specific part of the program (because this part has the worst execution time for example). In this case, the interdependency of the two analyses leads to interesting questions: Does the two analyses converge ? How many iterations does it need to terminate ? How much information does each iteration bring ? Etc.

[1] Ascertaining Uncertainty for Efficient Exact Cache Analysis, Valentin Touzeau, Claire Maïza, David Monniaux and Jan Reineke, CAV2017 (http://www-verimag.imag.fr/TR/TR-2017-2.pdf)