Resource Usage Analysis of Logic Programs via Abstract Interpretation Using Sized Types*
Resource Usage Analysis of Logic Programs via Abstract Interpretation Using Sized Types*
复制标题
通过使用大小类型的抽象解释来分析逻辑程序的资源使用情况*
DOI：
--
复制
发表时间：
2014
影响因子：
1.4
通讯作者：
M. Hermenegildo
中科院分区：
文献类型：
--
作者：
A. Serrano;P. López;M. Hermenegildo
提出了一种基于大小类型的逻辑程序通用资源分析方法。大小类型是包含结构（形状）信息的表示，允许在任何位置和深度表示一组术语及其子术语的大小的下界和上界。它们还允许关联逻辑谓词中出现在不同参数位置的术语和子术语的大小。使用这些大小的类型，资源分析可以推断程序中所有过程使用的资源的下限和上限，作为输入项（和子项）大小的函数，克服了现有资源分析的限制并提高了其精度。我们的新资源分析是在抽象解释框架内开发的，作为大小类型抽象领域的扩展，并已集成到Ciao预处理器CiaoPP中。将抽象的域运算与递归方程的建立和求解相结合，以推断大小和资源使用函数。我们表明，该分析是对CiaoPP中先前的资源分析的改进，并且在功率方面与最先进的系统相比较。
Abstract We present a novel general resource analysis for logic programs based on sized types. Sized types are representations that incorporate structural (shape) information and allow expressing both lower and upper bounds on the size of a set of terms and their subterms at any position and depth. They also allow relating the sizes of terms and subterms occurring at different argument positions in logic predicates. Using these sized types, the resource analysis can infer both lower and upper bounds on the resources used by all the procedures in a program as functions on input term (and subterm) sizes, overcoming limitations of existing resource analyses and enhancing their precision. Our new resource analysis has been developed within the abstract interpretation framework, as an extension of the sized types abstract domain, and has been integrated into the Ciao preprocessor, CiaoPP. The abstract domain operations are integrated with the setting up and solving of recurrence equations for inferring both size and resource usage functions. We show that the analysis is an improvement over the previous resource analysis present in CiaoPP and compares well in power to state of the art systems.