成本关系系统：独立于存储的递归成本分析

理论计算机科学电子笔记248（2009）31-46www.elsevier.com/locate/entcs成本关系系统：一种与存储无关的成本分析ElviraAlbert1PuriArenas1SamirGenaim1Germ'anPuebla21DSIC，马德里康普顿斯大学，{elvira，puri}@ sip.ucm.es，clip.dia.fi.upm.es2马德里技术大学，clip.dia.fi.upm.es摘要成本分析的目的是获得有关项目执行成本的信息。 本文研究成本关系系统（CRS）：成本分析中使用的递归方程组，其目的是根据程序输入参数的大小来获取程序的执行成本。 我们从一个独立于特定成本分析框架的一般角度来研究CRS的概念。 我们的主要贡献是：我们提供了执行成本和CRS的正式定义，它不依赖于特定的编程语言;我们提出了健全CRS的概念，即，它正确地近似相应的程序的成本，我们确定的递归关系系统，其可能的应用和新的挑战，他们带来的挑战。 我们的一般框架说明了它的成本分析的Java字节码，Haskell和Prolog的实例。关键词：成本分析，资源使用，静态分析，复杂性。1介绍关于自动成本分析的研究可以追溯到Wegbreit在1975年的开创性工作[22]，该工作提出通过导出捕获其执行成本的闭合表达式此外，Cousot和Cousot在他们1977年关于抽象解释的开创性论文中已经概述了性能分析的方法。从那时起，已经为各种编程语言设计了大量的成本分析框架，包括函数式[22，16，18，21，19，8]，逻辑[13，17]和命令式[1，2]编程这项工作的部分资金来自欧盟委员会信息社会技术计划，IST-15905 MOBIUS和IST-231620 HATS项目下的未来和新兴技术，西班牙教育部（MEC）在TIN-2005-09207 MERIT和TIN-2008-05624 DOVES项目下，以及马德里地区政府在S-0505/TIC/0407 PROMESAS项目下。1571-0661 © 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.07.05732E. Albert等人/理论计算机科学电子笔记248（2009）31语言本文的一个重要发现是，不同语言和编程范式的代价分析结果往往可以统一表示为代价关系系统（CostRelationSystem，简称CRS）。一般来说，给定一个程序，成本分析师首先通过静态分析技术计算程序行为在大多数情况下，这是通过依靠抽象解释技术获得程序的抽象本质上，抽象包括推断参数之间的大小关系和替换输入参数（数值、数组、动态数据结构等）。对应的大小。请注意，一段数据的大小是它所包含的实际信息的抽象。例如，一个数组的大小可以是它的长度，而对于一个链接的数据结构，我们可以把它的大小取为最长引用路径的长度。此外，为了生成CRS，程序中的迭代构造（循环和递归）被转换为递归。因此，CRS是一组递归方程，其目的是根据输入参数的大小来捕获程序的成本。CRS有两个特点使它们成为有趣和强大的工具：（1）它们原则上不限于任何复杂性类。因此，它们可以用来推断成本是多项式的，对数的，指数的，等等。（2）它们可以用来捕获各种非平凡的资源概念，如堆消耗，调用特定方法的次数，执行的字节码指令等。本文的第一个目标是描述CRS的概念，并激励其作为成本分析的通用目标语言。直观的想法是，CRS抽象掉了特定的语言特征，只是程序的抽象版本的一种工具，允许近似其成本。此外，我们描述的概念CRS是正确的。为此，我们需要为CRS定义一个评估机制。我们将看到，CRS可以独立于编写成本分析输入程序的编程语言而因此，CRS可以被视为通用语言，因为它们可以用作任何语言的成本分析目标。因此，我们认为，在CRS的研究进展感兴趣的任何编程语言的成本分析。本文的第二个目标是介绍CRS带来的特点和挑战。由于CRS在许多方面类似于递归关系系统（RRS），因此通常假设成本分析的输出只是RRS。我们澄清CRS和RRS之间的区别，并指出现有的计算机代数系统（CAS）处理它们的局限性。最后，CRS的有用性进行了讨论，通过描述其在性能调试和代码认证的背景下的应用。本文的主要贡献i) 我们提供了一个统一的成本分析视图，该视图捕获了不同编程范式的现有分析仪的主要组件ii) 给出了CRS的形式化定义，并给出了独立于语言和代价模型的运行时评估机制。E. Albert等人/理论计算机科学电子笔记248（2009）3133iii) 确定CRS和RRS之间的差异，以及现有CAS处理它们的局限性iv) 解决和界定CRS构成的挑战进行了描述，并概述了CRS的几个应用我们认为，我们的工作澄清了CRS的概念，并表明CRS可以用作成本分析仪开发中的通用语言本文的其余部分组织如下。在第2节中，我们提出了执行成本的一般概念。第3节介绍了成本分析仪所包含的组成部分。在第4节中，我们通过Java字节码、Haskell和Prolog中的一个例子来激励CRS的语言独立性。第5节提供了CRS的正式定义。我们在第6节中强调CRS和RRS之间的差异。CRS的运行时评估机制在第7节中给出，同时给出了正确CRS的概念。节中8，我们确定了解决和绑定CRS的挑战最后，在第9节中，我们总结并回顾了相关工作。2执行成本的一般概念及成本模型我们首先提供了一个一般的概念，执行成本，这是执行的特点，CRS的目的是捕捉。对于给定的输入数据执行程序的成本自然与计算期间执行的各个计算步骤的成本有关。每一种编程语言都配备了一个描述如何执行计算的操作语义。在这种设置中，执行从初始状态s0开始，并且在每个执行步骤中，由操作语义规定的规则用于通过计算其后继者来扩展每个非最终状态。严格表示执行的一种常见方法是通过状态转换系统（STS），它是一个抽象机器，由一组状态和一个表示状态之间转换的二元关系~ ×我们用si~sj，其中si，sj∈ ij，来表示从si到sj有一个过渡，我们说sj是si的后继。一个国家是最终的，它没有继承人。在许多编程语言中，表示执行的STS仅由一个分支组成然而，对于像Prolog这样的一些某些节点可以具有多个后继节点。注意，在这种操作语义下，Prolog是确定性的，因为我们总是计算所有可能的结果。给定一个初始调用，只有一个STS代表它的执行。将成本概念与执行期间执行的转换联系起来是很自然的，即，STS中的弧。由于从成本的角度来看，并非所有的转换都必须是等价的，因此我们允许将不同的标签分配给不同的转换。为了达到这个目的，我们将引入一组标签L，并使用标签转移系统，这是状态转移系统，其中每个转移si~sj都标记有标签l∈ L，我们用si~lsj表示。因此，现在转换对应于三元关系× L ×。显然，一个未标记的转移系统等价于一个只有一个标记的转移系统，34E. Albert等人/理论计算机科学电子笔记248（2009）31一个标签。我们为每个转换分配的标签的选择很重要，因为它考虑了我们可以用来获得成本的可观察信息。例如，在低级编程语言中，如Java字节码（简称JBC），我们可以用转换期间执行的字节码指令来标记每个转换。我们可以通过在标签中编码指令的输入参数（可能是隐式的）的值来进一步细化标签。在Prolog的情况下，我们可以用在相应的解决步骤中使用的子句（的标识符）来标记转换。我们可以选择在相应的谓词调用中对输入值进行编码。对于函数式程序，我们可以用函数定义w.r.t.其表达减少。我们可以在相应的函数调用中对输入值进行可选编码。 成本模型是 函数M： L →Q+，即 它为每个变量指定一个正有理数，label. 不同的成本模型衡量执行的不同方面给予STSt，我们使用Labels（t）来表示出现在t的转换中的标签集合。然后，执行t的成本被定义为相应的成本。Σ标签，即成本（t，M）=l∈Labels（t）M（l）.不同类别的标签和相关联的成本模型可用于测量使用不同的利益资源。例如，[2]的Java字节码成本分析器可以用于观察执行步骤的数量、执行期间分配的堆的数量以及对某些相关方法的调用数量特别地，计算执行步骤的数量的成本模型可以被定义为对于任何l，Mninst（l）= 1。 计算堆上分配的字节数的成本模型Mheap已经在[4]中定义，其中成本模型为所有不分配堆中内存的字节码指令返回零，并为实际分配堆空间的指令返回相应的字节数。在成本分析中，只需提供相应的定义即可直接插入新的成本模型，并且可以通过工具推断出所提供模型的CRS，通常无需在分析引擎中进行任何修改。在我们的例子中，为了保持演示的简单性，我们使用了一个计算执行步骤数量的成本模型：对于JBC，它计算执行的字节码指令的数量;对于Prolog，它计算解析步骤;对于函数式程序，它计算缩减（重写）步骤。原则上，这种执行成本概念的直接应用对于确定性编程语言是可能的，只要执行终止并涉及以下步骤：（1）给定初始状态，产生其相应的STSt，（2）收集t中所有转换的标签集，（3）将成本模型应用于每个标签，（4）通过将这些数字相加获得最终结果。从实践的角度来看，交错这些阶段通常更好，以便在执行程序时累积成本。这可以通过用额外的参数来检测程序来完成，这些参数会累积成本，或者通过使用操作语义来实现。这两种方法都有一个缺点，即它们需要运行程序来计算每个感兴趣的输入值的成本另一方面，对于给定的初始状态s，静态方法的目标是E. Albert等人/理论计算机科学电子笔记248（2009）3135基于规则的表达式。无用变量程序语言系分析CRS接口成本模型大小关系Fig. 1. 成本分析在近似成本（t，M）s. t。t对应于从s0开始但不构造t的执行，即，它们允许对某些输入数据的程序成本进行近似，而不必为这些数据实际运行程序，从而避免了这种开销。成本分析和其中的CRS属于第二种方法。在确定性语言中，给定初始状态s0，有一个唯一的STS对应于执行。然而，在可能有非确定性选择的语言中，初始状态可能会导致几个可能的STS。 事实上，这是大多数现实编程语言的情况，因为它们提供了随机数生成和/或访问环境变量（如日期/时间）的构造。为了适应真正的非确定性编程语言，从现在开始，我们考虑给定初始状态s0，有一组不同的执行，以及它们相应的STS，可以从s0构建。我们将s0的所有可能STS的集合称为Execution（s0）。在确定性执行中，Executions（s0）是一个单例。3成本分析图1提供了成本分析的统一视图，其主要组成部分它合并以计算不同编程范例的CRS。在双框架内，我们表明，分析接收作为输入的程序和选定的成本模型，并作为输出的CRS产量。分析器可以有一组预定义的成本模型，在某些情况下，用户可以定义自己的成本模型[17]。我们现在更详细地描述主要组件。基于规则的表示。 在图的左上方，我们看到传入的程序通常被转换为基于规则的中间表示。这一步的主要目的是检测程序中的循环并表示它们借助于递归规则，以便于随后的CRS生成阶段。这一步可以很容易地从程序的控制流图（简称CFG）中通过将规则与每个基本块相关联来完成。 当成本分析 在低级语言上（参见，例如，[2]），具有基于规则的形式使得可以将字节码的非结构化控制流表示为过程形式（例如， goto语句被转换为递归）。 成本分析声明性语言的一部分不需要这种转换，因为它们本身就在递归形式36E. Albert等人/理论计算机科学电子笔记248（2009）31尺寸分析。在不同的程序点上获得状态之间的大小关系对于建立成本关系是必不可少的。这些大小描述了当程序循环时数据如何变化。为此目的，大小度量的概念至关重要。通常，可以使用各种度量来确定数据的大小。例如，在符号语言中（参见，例如，[13]），术语深度，术语大小和列表长度被用作大小度量。在面向对象语言中，使用了两种大小度量对于整数类型的值，我们可以将其实际值作为其大小。对于引用的值，它们的路径长度[20]可以用作它们的大小。引用的路径长度被定义为从它可到达的最长引用路径的长度。存在广泛的大小分析，用于计算不同编程语言的有用大小近似值。语言依赖分析。编程语言的计算性质可能需要一些额外的静态分析，以便生成有用和可靠的CRS。这是逻辑建模中的情况，其中需要额外的信息，例如确定性和非故障，以便获得准确和正确地近似对应成本的CRS，因为这样的分析提供了关于执行树的形状的有价值的信息（参见，例如，[12]）。类似的分析需要在延迟求值的函数式编程的成本分析中进行。这些问题通常不会在命令式语言中出现无用的变量在理想情况下，成本分析人员对获得CRS感兴趣，其中只有程序变量和参数，它是成本的一部分，出现在方程中的参数。可能对程序成本有影响的程序变量是那些可能直接或间接影响条件语句的变量（即，它们可以选择程序的控制流），以及那些可能被编码在转换标签中的（如上面第2无用变量的消除可以通过应用公知的切片技术来完成（参见，例如，[3]）。接口。为了分析现实的程序，必须有一个模块化的设计，允许在分析过程中处理外部方法。通过外部方法，我们指的是分析器无法访问的代码，包括用不同语言编写的本机库（因此不可分析），尚未实现的方法等。成本分析器可以通过存储外部方法所需信息的接口来支持模块化设计。按照模块化分析的惯例，从接口学习的信息在分析过程中的使用方式与分析器本身推断的信息非常相似。CRS。 一旦前面的阶段有了相应的信息，分析器就可以为输入程序和选定的成本模型建立CRS。本质上，程序的递归表示决定了CRS的结构CRS的参数表示相应程序变量的大小。大小关系近似于（1）每个成本等式的适用性条件和（2）数据大小如何在等式上增加或减少。成本模型用于定义每个代码块的成本，E. Albert等人/理论计算机科学电子笔记248（2009）3137k1=4，k2 =26，k3 =26，k4 =29Mninst(1) mmerge（this，o）=k1{this≥1，o=0}(2)mmerge（this，o）=k3+merge（this，oJ）{this≥1，o≥1，o>oJ，oJ≥0}(3)mmerge（this，o）=k2{this≥1，o≥1}(4)mmerge（this，o）=k4+merge（thisJ，o）{this>thisJ，this≥2，thisJ≥1，o≥1}PrologJava（递归）merge（This，[ ]，R）：-！，R =这个。合并（[D|下一页]，[OD|ONEx1，R）：-D>OD，！，R =[OD |T]，合并（[D |Next]，ONext，T）。merge（[D]，O，R）：-！R =[D |O]。合并（[D|下一页]，O，R）：-R = [D |T]，merge（Next，O，T）.public class MyClass{int d;private MLRec next;public int findDuplicate（ int d，int p）{this.next = next;}public void run（）{if（o== null）return this;（1）melse if（d> d）return new MLRec（o.d，merge（o.next））;（2）melse if（next= null）return new MLRec（d，o）;（3）melse return new MLRec（d，next.merge（o））;（4）m}Haskellmerge this[]= thismerge（d：next）o=如果（d>od），则(od：merge（d：next）onext）else if（next==[ ]）then（d：o）else（d：merge next o）其中（od：onext）= o图二. 递归合并图3.第三章。递归合并的CRS结构（捕获不同的实现）成本等式包括。作为这个过程的结果，CRS是抽象程序的工具化版本，旨在根据感兴趣的成本模型4实例证明CRS的独立性通过一个简单的例子，我们说明了成本分析的上述组成部分，并激发了CRS作为成本分析的语言独立的目标语言的概念。我们考虑图中的三个实现2的merge方法，合并两个排序列表。 在右边，Java中的实现合并了列表o接收作为输入参数的对象this，并在新列表中输出结果。在左边，我们展示了两个实现，一个是Prolog，一个是Haskell。 在这两种情况下，要合并的列表都显示为显式输入参数。这三种实现都有相同的前提条件，即第一个参数（在Java版本中是这样）是非空的。图3中描绘的CRS对图2中所示的合并的三个实现中的任何一个的成本分析的可能输出进行建模，因为它们具有类似的操作行为。特别地，所示的CRS是通过使用[2]的分析器从与Java版本相关联的字节码自动推断的。1取决于编程语言和所使用的成本模型，38E. Albert等人/理论计算机科学电子笔记248（2009）311为了便于阅读，CRS是在通过执行部分评估来简化它之后呈现的，这通过它们的定义来替换调用。E. Albert等人/理论计算机科学电子笔记248（2009）3139k1，.，k4取不同的值。我们在图的底部显示的值对应于M ninst成本模型（见第二节）。（见上文第2段）。本节的目的是说明从三个实现生成CRS所涉及的主要步骤第一个需要注意的要点是，正如第3节所解释的，CRS应该与程序的结构相匹配，这样当程序包含循环结构时，它的CRS就有递归。从声明性实现中，可以直接看到每个程序规则（或子句）都导致一个相关的成本等式。在命令式程序中，这一步需要经过某种形式的中间的、基于规则的表示，它使得程序结构和成本方程之间的对应关系是明确的 图4描述了合并的Java代码的CFG。 一个规则 (or等式）。当量(1)当列表o为空时，m捕获跟踪merge1-merge3当量(3)m捕获跟踪merge1-merge2-merge4-merge6的成本，这在列表this只有一个元素时发生。 当量(2)m捕获跟踪merge1-merge2-merge5的成本，其对应于第一个递归调用。最后，Eq。(4)m捕获对应于第二递归调用的跟踪merge1-merge2-merge4-merge7第二个要点是，程序中的数据结构在CRS中被例如，在递归调用Eq. (2)m，则可以确保O的大小已经减小（O>OJ），但我们不知道减小了多少。这是因为[2]中使用的基于指针的数据结构的大小分析是基于路径长度分析[14]，其中大小关系仅使用>和≥。逻辑和函数编程中更精确的大小分析可以推断出精确的关系，即，oJ=o−1。尺寸关系还包含适用性条件（即，如果有的话，通过提供仅选择LHS中的变量（的子集）的约束来为不同的方程（其中，我们有例如o=0，它要求列表o为空。第三个要点是条件d>o。d不出现在等式（2）的大小关系中。 d≤ 0。d在（3）m和（4）m中）。 这是因为这个条件在我们的CRS中是不可观察的，因为列表this和o已经被抽象到它们的长度，因此this中的值也是如此。d和o。D未知在这三种不同的语言中确实如此最后的结论是，不管程序是用什么语言编写的，成本分析都会产生一个形式相同的成本关系系统。这一观察促使我们对CRS的概念、评估机制、主要特性和挑战进行形式化描述，这是本文剩余部分的主题。5成本关系系统本部分正式提出了成本关系系统的概念。 我们使用x，y，z（可能已订阅）来表示变量，v，w表示Z的整数值，a，b表示N的自然数，q表示Q的有理数。我们用x表示40E. Albert等人/理论计算机科学电子笔记248（2009）31next=nulld > o.d合并3合并7是的合并1合并2否是没有合并4合并5return MLRec（o.d，merge（o.next））;合并6否是见图4。 方法合并的控制流程图变量序列x1，... .，xn，对于某些n> 0。类似地，v表示整数值的序列。为了简单起见，我们有时将这些序列解释为集合。给定一个序列x，我们说x的赋值是一个整数值序列v（actionuasignmentisdenoted[x/v]）。给定一个整数A，A[x/v]是将变量x i在A中的每次出现替换为vi的结果。此外，我们使用vars（A）来表示A中出现的变量集。线性表达式的形式为q0+ q1x1+···+qnxn。线性约束的形式为l1op l2，其中l1和l2是线性表达式，op∈ {=，≤，<，>，≥}。使用一组线性约束来表示相应约束的合取。尺寸关系是线性约束的集合我们现在定义成本表达式的概念，它在语法上表征CRS包含的表达式类型。定义5.1[成本表达式]成本表达式exp是以下形式的符号表达式：exp：：= q|XQ|exp-opexp-op|出口|loga（exp）|最大值（S）|min（S）其中op∈ {+，−，/，n}且S是代价表达式的非空集。成本表达式是CRS的基本要素它们被用来表示重新-我们正在积累的源;它们也用于表示CRS的边界由于CRS可用于捕获任何复杂性类，因此成本表达式必须涵盖多项式、对数和指数表达式，并且我们必须能够限制其解（通过使用函数max和min）。我们现在给出CRS概念的定义5.2成本关系系统S是一组成本方程，其形式如下：其中k≥0，i=1i1. 所有变量x、vars（exp）和yi都是不同的变量，2. exp是成本表达式，3. 这是一个与VARABLEXYVARS（ExP）相关的关系ki=1是的。图3中描绘的CRS包含仅具有一个递归调用的简单成本等式。此外，所有表达式exp都是常量，因为我们给步骤的成本赋予了相同的常量值“1”。显然，并非所有成本模型都是如此。例如，如果我们测量堆消耗，则创建integers的开销为4×n堆单元，其中n是数组的长度，4是表示整数所需的字节数例5.3让我们举例说明非常量表达式的使用。我们包括return MLRec（d）;return MLRec（d，next.merge（o））o=null返回此;E. Albert等人/理论计算机科学电子笔记248（2009）3141insertSort（l）=4+loop（l，0）{l≥0}loop（l，acu）=2{l =0，acu≥0}loop（l，acu）=26+merge（1，acu）+循环（lJ，acuJ）{l>lJ，lJ≥0，acu≥0，acuJ>acu}static MLRec insertSort（MLRecl）{Rec acu=null;（l！空值）{LRec node= new MLRec（l.d，null）; cu=node.merge（acu）;int n=l.next;}rn acu;}下面的方法insertSort使用前面的方法merge对输入列表进行排序。 CRS显示在右侧。 我们可以在（3）中观察到对合并成本的调用，其中第一个参数总是一个元素的列表。此外，尺寸关系似乎附加到描述规则头部以及头部和身体之间变量关系的方程。正如预期的那样，列表l的大小在循环中减小。我们可以安全地假设合并成本的上限（见定义8.1）：merge（l1，l2）= 26+29（l1+l2）。在这种情况下，等式（3）s采用以下形式：loop（l，acu）=52+29（1+acu）+loop（lJ，acuJ）。在这里我们可以看到非-常数成本表达式，特别是，它们必须涵盖复杂性CRS可以绑定到的类。Q6CRS与递归关系系统CRS具有几个重要的特征，这些特征是通过自动程序分析获得的结果，并且在传统的递归关系系统（RRS）中不存在：非确定性关系。 与RRS相反，相同关系的成本方程不需要相互排斥。允许这样做的原因是因为成本分析需要使用大小抽象。不可避免的是，抽象的使用引入了精度损失：当使用参数的大小而不是它们的实际值时，一些使原始程序的执行具有确定性的守卫可能无法观察到。在我们的例子中，这发生在守卫d>o上。d在方程（2）m和（4）m之间，因为它讨论了列表中元素的具体值，这些值显然是不可观察的，因为列表已经被抽象到它们的长度。不精确的大小关系。CRS可以具有包含不等式约束的大小关系。这是必不可少的，以处理成本关系自动获得的分析具有复杂的数据结构，其中规模分析可能会失去精度的现实计划。例如，分析可能能够推断出给定的数据结构从一次迭代到另一次迭代在大小上严格地减小，但它可能无法提供精确的减小。在我们的例子中，(2)m，（4）m，（3）s，其中我们只知道o>oJ，this>thisJ，l>lJ。多个论点。成本关系可以有几个参数，这些参数在每次迭代中可能增加或减少。 重要的是，给定关系的执行次数可以取决于它的几个参数，或者是几个参数的组合。为42E. Albert等人/理论计算机科学电子笔记248（2009）31(1)M 合并（1，0）4(2)S 循环（0，2(1)M 合并（1，0）4(3)S 循环（1，26(3)M 合并（1，1）26(2)S 循环（0，2(1)S insertSort（2）4(3)S循环26(1)S insertSort（2）4(3)S 循环26图五. insertSort的两个求值树（2）例如，函数merge被执行min（this，o）次。相比之下，大多数RRS求解器假设函数执行的次数仅取决于一个参数（通常是递减的变量）。由于上面的前两点，CRS不需要定义函数，而是定义关系，在这个意义上，给定输入值v，可能存在C（v）的多个结果。这就提出了问题：在运行时评估CRS是否可行，即，运行抽象程序的插装是否有意义现有的CAS（Maple、Mathematica等）足以解决CRS，因为它已被假定通常由成本分析界？下一节将讨论这些问题以及CRS带来的挑战7CRS的评价我们现在为CRS提供了一个正式的语义。这个语义是根据调用和应答来定义的。调用的形式是C（v），其中C是成本关系，v是整数值。调用C（v）在S中通过用适用方程的rhs的适当实例化重复地替换对关系的调用来评估，直到成本表达式（即，免费电话（call-free）。这个计算表达式由一系列代价表达式的和组成请注意，CRS具有潜在的不确定性，这意味着可能存在不同的评估呼叫的方式，从而导致对呼叫的不同应答。获得答案的过程可以使用定义为（可能嵌套）形式节点（呼叫，本地成本，孩子）的项的树以图形方式表示。例7.1图5描述了调用insertSort（2）的两个求值树。我们可以观察到树中的每个节点都包含一个调用（中间的框）和它的本地成本（右边的框），它通过箭头链接到它的孩子。在图中，为了清楚起见，每个调用都用数字（左框）注释，该数字指示用于评估相应调用的方程。最左边的树是最小成本的评估树，其产生36个成本单元，最右边的树是最大成本的评估树，其产生88个成本单元。Q定义7.2[求值树]给定CRSS和调用C（v），求值树S中的C（v），记为Tree（C（v），S），是节点（C（v），e，t1，...，tk），其中：(1) 存在一个重新命名的分离方程<$C（x）= exp +<$ kD（y），<$k∈ S s. t.吉吉是i=0iiE. Albert等人/理论计算机科学电子笔记248（2009）3143s在Z中是稳定的，其中reJ=[x/v]，且d(2) 存在分别用于VAR（exp），Y i的赋值W，Vi，S. T。 J [vars（exp）/w，yi/vi]在Z中是可定义的，并且d(3) e=exp[v arrs（exp）/w]，ti是一个等价的Tree（Di（vi），S），其中hi=0， . . . ，k.在步骤1中，我们寻找一个方程E，它可用于求解C（v）。 注意 可能有几个方程适用。在步骤2中，我们寻找E的rhs中的变量的赋值，这些赋值与与E相关联的大小关系兼容。这是另一个非确定性步骤，因为可能存在（无限多个）满足所有大小关系的不同分配。最后，在步骤3中，我们将赋值应用于表达式exp，并递归地评估呼叫。例7.3在图3的CRS中，只要公式（4）m适用，公式（2）m也适用，因为≥2意味着≥1。还要注意，在递归调用loop中，我们可以选择任何值lJ，acuJ，使得lJ< l，acuJ>acu。图5中最右边的树对应于最大实际成本，其中我们在递归调用中指定lJ=l−1和acuJ=acu+1 这就是现实生活中程序的执行。 在最右边的树中，我们指定lJ=l−2和acuJ=acu+1在循环的递归调用中，这导致最小的近似，然而，它并不对应于任何实际执行。这是静态分析计算的安全近似的一个侧面：它允许获得正确的信息，但有时可能不精确。有趣的是，我们可以计算出无限多的求值树，因为实例化步骤2可以给出无限多的求值树。对变量acuJ的赋值的数量，满足条件acuJ>acu。Q由于对于给定的调用可以获得多个求值树，因此我们使用标记Trees（C（v），S）来指代S中C（v）的所有求值树的集合。 然后，我们可以定义答案（C（v），S）={Sum（t）|t∈Trees（C（v），S）}，其中Sum（t）遍历t中的所有节点并计算其中的代价表达式之和。以下定义给出了正确CRS的概念。定义7.4 [正确的CRS]设m是一个有n个输入参数的方法，M是一个成本模型。一个CRS S对m和Mi是正确的，对于任何v∈Zn和相应的初始状态s0，我们有Cost（t，M）∈answers（Cm（v），S）对于任何t∈Executions（s0）。直觉上，CRS是正确的，如果它安全地近似实际执行成本，在这个意义上，这样的成本必须是方程的一个可能的解决方案。在一个给定的成本分析框架中，CRS的正确性通常取决于该框架中使用的特定规模分析8解决CRS：现有工具在上一节中，我们已经看到，由于CRS的递归性质，直接评估对CRS中定义的关系的调用需要在递归调用之后执行迭代计算。由于经常有多个44E. Albert等人/理论计算机科学电子笔记248（2009）31（可能是无限的）可能的调用评估，试图以这种方式获得解决方案（或上限）是不切实际的。此外，通过查看相关的CRS，特别是当涉及多个关系时，很难立即收集有关计划成本的信息。因此，CRS具有相当有限的适用性，除非封闭形式（即，非递归）的解或它们的界。需要注意的一点是，为给定目标执行程序的实际成本必然是CRS的解决方案原则上，这使得CRS成为计算成本上限和下限的有效工具。我们首先回顾关系的上界定义8.1[上界]设P，≤ P是偏序集，S是P的子集。值a∈P是Si的上界，s∈S我们有s≤a。另外，设C是Zn×R上的关系. 函数U：Zn→R是Ci∈Zn的上界，我们有U（v）是解（C（v），S）的上界.大 多数 现有 的分 析器 尝试 使用 计算 机 代数 系统 （CAS ） 来解 决RRS ， 如Mathematica，Maple，Maxima等。本质上，成本分析器使用它们的方式有两种：1）直接尝试将它们应用于解决CRS（如果它们具有RRS的形式）或2）将CRS转换为RRS。根据我们在[2]中使用分析仪的经验，在CRS上直接应用CAS不是一个现实的选择。主要的问题是，CAS只承认一种形式的RRS，而这种RRS并不包括将其与RRS区分开来的CRS的基本特征，正如第6节所指出的那样。即使对于我们简单的运行示例，也会发生这种情况;不存在我们可以直接使用的RRS求解器。这并不是说现有的CAS不强大。事实上，从代数的角度来看，如果我们忽略CRS所具有的附加特征，则成本关系将被视为一类简单的递归方程。事实上，CAS求解的递归方程可以呈现出更复杂的结构。例如，它们支持具有函数调用系数的方程，这些函数调用可以是多项式。然而，CRS中的方程并不真正需要这种能力，因为从程序的成本分析中生成的方程通常不是如此复杂的形式，因为它们的结构是从程序的结构中获得的。另一方面，现有的CAS不足以攻击CRSs中不存在于RRS中的一些特征。第二种方法是通过将CRS转换为RRS然后使用CAS来获得闭合形式的上界这需要，除其他事项外，消除不确定性，同时保留最坏情况的解决方案。为此，我们需要从CRS中删除方程，有时也需要用精确的尺寸关系代替不精确的尺寸关系。这个转换在我们的例子中很容易完成，因为我们可以采用最昂贵的递归情况（4）m和最昂贵的基本情况（3）m。然而，这两种转换都不能在所有情况下安全地进行特别地，当最大成本可能是不同等式之间的交织的结果时，这是不可能的。例如，如果我们对获得上限解感兴趣，那么在某些情况下，如果我们删除其中的任何方程，E. Albert等人/理论计算机科学电子笔记248（2009）3145CRS为了获得确定性，我们不再获得最坏的情况下，得到的封闭形式不能保证对应于一个正确的上限。因此，尽管这种方法可以应用于简单的情况，但也不是一个合理的替代方案。通过自动成本分析计算CRS输出的解决方案或上/下限的CRS求解器必须能够：(i) 当给定关系执行的（最大）次数可以是其几个参数的组合时，限制成本关系的迭代次数(ii) 用一般的方法处理不等式。以前的系统要么不能处理它们，要么它们只允许将变量与常数项相关的不等式，而不是变量之间的不等式（例如，这一点（J）。(iii) 提供一个通用的和合理的方法来计算非确定性方程的最大值（或最小值）。这通常是复杂的，因为最大（或最小）成本可能是不同方程之间交织的结果我们只知道三个工具，旨在解决或限制CRS。最早的系统之一是CAS [13]。但它仅限于相当简单的CRS，特别是它不能处理上面的前两个功能。在这个方向上的另一个相关工作是PURRS [7]，它是第一个以全自动的方式为广泛的递归类提供非渐近上界和下界的系统。不幸的是，它要求CRS是确定性的（上面的第3项），并且不处理不等式（第2项）。 最近，PUBS系统[5]已经被（可查阅http：//www.cliplab.org/Systems/PUBS）。这是朝这个方向迈出的重要一步，因为原则上它能够处理这三个项目以上 我们相信，最近开发的自动求解工具将是成本分析的实际应用的重要性9讨论和相关工作我们提出了成本的一般概念和成本分析的统一观点，其中包括最先进的资源使用分析仪的主要组成部分。在这种情况下，我们已经激发和形式化的概念，CRSs作为一种独立于语言的手段，以目标的分析输出。在成本分析方面，有一个重要的问题仍然不清楚，这是一个贡献。论文主要阐述了CRS与RRS的区别。事实上，随着CAS（SuchasMathematicaR，MAXIMA，MAPLE等）的发展，最近的成本分析[8，15]试图使用它们。本文阐明了CRS与RRS的区别。这种困难的重要后果是，现有的CAS没有涵盖CRS的区别方面，并且需要开发能够直接处理它们的实用求解器，正如我们所做的那样[5]第一次尝试解决这个问题。最后，请注意，给定CRS的解或上/下限，46E. Albert等人/理论计算机科学电子笔记248（2009）31作为近似，CRS在以下领域带来了非常有趣的应用• 资源绑定证书[11，6，9]。它建议使用涉及成本要求的安全特性，即，不受信任的代码遵守资源消耗的特定界限。CRS允许表达任意的资源界限证书。基于类型系统的方法通常限于多项式边界[11，6]。此应用程序的一个示例是移动代码，其中代码消费者接收要执行的代码。代码的接收器可能想要推断成本信息，以便拒绝在计算资源方面（在时间和/或空间上）具有太大成本要求的代码。• 性能验证和确认。 这是成本分析的一个直接应用，其中分析者试图验证或伪造程序员编写的关于程序效率的断言。CRS的作用是必不可少的，以推断的性能，无论是作为一个精确的解决方案或上限。• 控制粒度[13]。具有多核处理器的并行计算机目前正成为主流。在并行系统中，可以使用关于不同过程的成本的知识来指导并行进程的划分、分配引用[1] A. Adachi，T. KASAI，和DE。 莫里雅。一个新的规则可以让你的分析更加准确。 INJ。 Becv'ar，编辑，MFCS，计算机科学讲义第74卷，第201-207页。斯普林格，1979年。[2] E. Albert，P. Arenas，S. Genaim，G. Puebla和D. 扎纳迪尼 Java字节码的成本分析 Rocco De Nicola，编辑，第16届欧洲编程研讨会，ESOPSpringer，2007年3月。[