Precise yet scalable resource analysis via symbolic execution

Abstract:

The expanding complexity of embedded systems has emerged the need for techniques to perform resource analysis. The thesis makes several contributions in the area of worst-case resource consumption analysis.
First, an integrated analysis framework is presented where micro-architectural modeling and systematic path-sensitivity are synergized. To the best of our knowledge, integrated methods were not scalable up to now. Integrated resource analysis would give us a very high precision for resource analysis, but at the same time, it is a huge challenge for scalability. Our contribution is then a dynamic programming algorithm with a powerful concept of reuse. Reuse, in turn, depends on the core concepts of interpolation and dominance. Our setting is novel not just because we are performing interpolation for resource analysis, but because our interpolation with dominance covers reuse under an environment where resource consumption of program paths are dynamic and/or symbolic.

Next, the analysis framework is customized for Worst-case Execution Time (WCET) Analysis. The main contribution here is performing precise integrated WCET analysis down to instruction and data caches. The key challenge, scalability, is obtained by using a notion of reuse in an environment where the contribution of each basic block to the overall WCET is dynamic. Thirdly, the analysis framework is customized for symbolic Memory High-watermark (MHW) Analysis. The main contributions of the Memory high-watermark analysis are (1) it is performed on a non-cumulative resource analysis where the resource of interest can be consumed or released and (2) the concept of reuse with interpolation and dominance is performed in the presence of symbolic bounds. Finally, the analysis framework is customized for Worst-case Energy Consumption (WCEC) Analysis in the presence of cache and in-order pipelines. Our contribution here is extending reuse to be performed in the presence of in-order pipeline and caches.