Analysing memory resource bounds for low-level programs
Analysing memory resource bounds for low-level programs
复制标题
DOI：
10.1145/1375634.1375656
复制
发表时间：
2008-06
期刊：
影响因子：
--
通讯作者：
W. Chin;Huu Hai Nguyen;C. Popeea;S. Qin
中科院分区：
文献类型：
--
作者：
W. Chin;Huu Hai Nguyen;C. Popeea;S. Qin
嵌入式系统正在得到越来越广泛的应用，但这些系统往往受到资源的限制。这些系统的编程模型应该正式考虑堆栈和堆等资源。在这篇文章中，我们展示了如何为汇编级程序推断内存资源界限。我们的推理过程根据其参数的符号值捕获每个方法的内存需求。为了提高精度，我们通过一种新的守卫表达格式来推断路径敏感信息。我们目前的方案依赖于Presburger求解器来象征性地捕获内存需求，并执行循环和递归的定点分析。除了在内存充分性方面的安全性外，我们的建议还可以提供对嵌入式设备内存成本的估计，并通过减少对内存限制的运行时检查来提高性能。
Embedded systems are becoming more widely used but these systems are often resource constrained. Programming models for these systems should take into formal consideration resources such as stack and heap. In this paper, we show how memory resource bounds can be inferred for assembly-level programs. Our inference process captures the memory needs of each method in terms of the symbolic values of its parameters. For better precision, we infer path-sensitive information through a novel guarded expression format. Our current proposal relies on a Presburger solver to capture memory requirements symbolically, and to perform fixpoint analysis for loops and recursion. Apart from safety in memory adequacy, our proposal can provide estimate on memory costs for embedded devices and improve performance via fewer runtime checks against memory bound.