一种内存消耗分析的半自动技术及其在ML类程序中的应用

可在www.sciencedirect.com在线获取理论计算机科学电子笔记330（2016）27-46www.elsevier.com/locate/entcs一种功能命令语言的内存消耗分析J'er'emieSalvucci1和EmmanuelChailloux2Sorb onneUniversit'es，UPMC Univers. Paris06，UMR 7606，LIP6，4 Place Jussieu，F-75005 Paris，France摘要资源受限的嵌入式系统无处不在，使它们成为关键组件。程序员必须对他们的运行时行为提供强有力的保证，以使他们可靠。其中，在运行时给出活动内存的上限是强制性的，以防止堆溢出溢出的发生。本文提出了一种半自动的技术来推断显式区域管理的ML类程序的空间复杂性。它旨在结合现有的形式主义，以获得一个一致的框架中的命令式和纯函数式程序保留字：ML，区域，静态分析，内存分析。1引言在受约束的环境中部署软件需要对其运行时行为的强有力的保证在内存受限的嵌入式系统中，动态分配通常被禁止，以保持执行时间分析可行，并避免堆溢出。我们引入了一种编程语言和一个资源消耗分析，使能动态分配，同时提供了一个上限的活内存在编译时。本文提出了一种混合了纯函数式和命令式特征以及显式区域机制的语言。为了检索程序内存交互的信息，我们依赖于一个静态类型检查系统和通过区域相关原语的手动内存管理。类型系统的目标是确保在编译时没有与内存相关的错误。到1jeremie. lip6.fr2emmanuel. lip6.frhttp://dx.doi.org/10.1016/j.entcs.2016.12.0131571-0661/© 2016由Elsevier B. V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。28J. Salvucci，E.Chailloux/Electronic Notes in Theoretical Computer Science 330（2016）27要执行此操作，程序员必须通过第3节中描述的一组受限原语手动管理内存。输出系统有助于概括术语，并在函数级别区分纯函数式和命令式风格。分析依赖于类型系统的正确性，只考虑与内存有关的无错误程序。它结合了几个现有的资源消耗分析，取决于推断的风格的选举制度。例如，一个不分配内存的函数不需要分析，而一个分配内存并执行副作用的函数需要小心处理。在纯函数上，我们应用了适应区域机制的自动摊销分析[7]。在命令式函数上，区域或空间信息用于边对象，我们使用程序员提供的迭代空间上的不变量作为注释。这两种分析都返回一个符号表达式，该表达式表征了计算中涉及的每个区域的分析函数这些符号表达式的组成与仔细处理的副作用给出了程序的内存消耗。分配内存和回收内存是正交操作。分配内存不需要有关内存图的当前状态的信息。然而，回收内存需要堆的全局视图来区分可达值和不可达值。在这项工作中，我们使用区域在编译时收集足够的信息，以防止过度悲观的上限考虑区域释放的程序员在一个健全的方式。本文的主要目标是引入一个框架，结合各种内存消耗分析，这取决于在功能级使用的编程风格，以提供一个上限的活内存在编译时考虑回收内存。在其余部分中，第2节介绍了相关工作。我们在第3节中描述了该语言及其作为分析基础的类型识别系统。然后，我们展示了如何处理纯粹的功能和命令的功能在第4节，第5节如上所述，第6节组成他们在一个一致的框架。然后，我们将在第7节中展示它是如何工作的。最后，我们总结了目前的局限性和进一步的改进讨论。2相关作品资源消耗分析始于70年代后期，METRIC [14]针对纯Lisp子集编写的程序的最佳，最差和平均执行时间。基于递归关系，它可以适用于内存消耗分析。与时间相反，记忆是可以回收的。因此，新的方法已经出现了从纯功能和命令的社区，以获得上界的生活记忆。大小类型[9]已经应用于HUME [13]的核心部分，HUME是一种具有急切求值机制的纯函数式语言。它推断线性空间的复杂性，并提供了一个上限分配的内存，而无需用户干预。自动摊销分析[6]，基于TarjanJ. Salvucci，E.Chailloux/Electronic Notes in Theoretical Computer Science 330（2016）2729几个项目。其中，RAML [7]是一种纯ML语言，RAJA [8]是Java语言的子集。它能够在没有任何用户注释的情况下，考虑最新版本中的一些副作用[5]来递归关系在面向Java平台的COSTA [1]项目依靠一个强大的求解器，它能够推断多项式，对数和指数界的活内存感谢一个基于作用域的数据管理机制。抽象解释[3]已应用于Safe [10]。一种纯一阶语言，配备了隐式区域机制来管理内存。该技术不局限于特定的复杂性类别。不幸的是，它没有考虑边效应或高阶函数。迭代空间上的不变量已经在针对Java语言的JConvent [2]项目它通过一个逃逸机制来考虑边效应它还依赖于外部工具或程序员提供的不变量来提取程序空间复杂度。多亏了转义机制，它可以提供一个活内存的上限。在下文中，我们在以前的工作的基础上，在编译时获得活内存的上限。我们开发了一种语言，配备了类型和输出系统和基于区域的显式记忆机制。该系统允许我们混合自动摊销分析和迭代空间上的不变量，这取决于在函数级采用的编程风格。编译时存储有关堆状态的信息的区域。然后，我们可以跟踪副作用，并考虑回收内存，以防止不准确的边界。3语言分析在现代高级语言中，内存管理通常由垃圾收集器执行。主要由动力学准则支配，预测其行为是一个困难的问题。例如，我们需要知道它何时被触发，以及将回收多少内存。为了解决这个问题，我们开发了一种静态语言，它配备了一种特殊的内存管理机制：regions [12]。一个区域表示一组数据，其寿命相似。最初开发的目的是将词法作用域带回到堆分配的值，它们避免了由于堆栈规则而导致的内存泄漏。 关于线性区域的工作[4]表明，使其更通用，而不涉及这样的堆栈规程。能力可以被视为对区域进行操作的许可，并作为相关区域内的数据对于其余计算仍然是必要的证明。这是一种编译时机制，允许我们在资源消耗分析期间考虑回收内存（参见第6节）。30J. Salvucci，E.Chailloux/Electronic Notes in Theoretical Computer Science 330（2016）273.1语法从程序员的角度来看，区域可以被看作是通过使用四个原语来管理数据库的一种方式：newrgn、@、aliasrgn和freergn。它们分别允许程序员分配新的区域，指定值时，暂时移除线性约束（请参阅键入规则）并安全地释放先前分配的区域。这些操作的正确性由类型系统在编译时通过使用功能来确保。能力可以被视为执行某些操作的权限。图1中的语法显示，每个表达式的计算结果都变成了堆分配的值，并用@进行注释，以指定在运行时分配的区域eρ 与区域分配值相关的每个操作都需要相关区域的相关能力。类型系统检查是否拥有正确的能力。 如果不是，这将被视为禁止的操作并引发类型错误。语言语法如图1所示。规则e用相应表达式的性质来注释。因此，eρ表示一个表达式，它的计算应该产生一个区域处理程序，ec，et和ef分别表示条件表达式的条件，结果和替代两种类型的转让，累积和非累积，将在第6节中讨论。表达式描述⟨e⟩::= ()|b|⟨n⟩|x|fun x → ⟨e⟩ @ ⟨e ρ⟩|e0|如果你可以，那么你就可以，否则你就可以。|let ⟨x ⟩ = ⟨e a⟩ in ⟨e b⟩|let rec ⟨f ⟩ ⟨x ⟩ = ⟨e b⟩ @ ⟨e ρ⟩ in⟨e⟩|（e a，e b）@ e ρ|Π i⟨e⟩|Nil @⟨e ρ⟩|Cons ⟨e h⟩ ⟨e t⟩ @ ⟨e ρ⟩|ref ⟨e⟩ @ ⟨e ρ⟩|e|⟨e⟩ += ⟨e⟩|！⟨e ⟩|newrgn()|aliasrgn ⟨e ρ⟩在伊斯坦堡|freergn⟨e ρ⟩单位，布尔，整数变量函数函数应用条件变量绑定递归绑定（仅函数）对构造对投影列表新表头引用赋值取消引用共享区域处理程序的新区域原语自由区域基元Fig. 1. 表达式3.2型式检验系统这种类型系统的目标是双重的：收集有关程序内存行为的信息，以防止错误的内存管理，并提供J. Salvucci，E.Chailloux/Electronic Notes in Theoretical Computer Science 330（2016）2731类型描述τ s |bool |int|ατCinC out|(⟨τa⟩−−−φ−−→⟨τb⟩,ρ)|(⟨τ a⟩ × ⟨τ b⟩,ρ)|(list ⟨τ ⟩,ρ)|(ref ⟨τ ⟩,ρ)|hndρσ ρ|我的天 ⟨ σ ρ ⟩σ|好吧 ⟨ σ ⟩singleton，booleans，integers的类型类型变量闭包类型对类型列表类型引用类型区域处理程序的类型区域类型方案类型方案图二. 类型堆在编译时可用。 类型判断具有以下形状C;Γe：τ; ΓJ;CJ;φ其中C是一组能力，Γ是一个类型化环境，φ是一组效果。 它读作如下：事件系统跟踪三种事件：alloc、read和write（见图3）。它们主要用于let泛化和资源消耗分析。检查描述读取{r}写入{r}分配{r}读取在区域r更新在区域r在区域r中分配新值图三.跟踪事件在语言中，有两种变量。那些绑定到堆栈值和那些绑定到区域分配的值。最新的是处理区域变量的规则，RVAR。为了确保正确性，为线性和非线性区域处理程序添加了两个特定规则，LRHVAR和RHVAR。如你所见，这个表达式的类型（见图2）包含一个区域名r。这个名字在环境C中被限定为一个约束q。这个限定符可以取两个不同的值：1或+。Linearity，1，确保您不共享区域处理程序，而+允许您削弱线性约束。此规则检查32J. Salvucci，E.Chailloux/Electronic Notes in Theoretical Computer Science 330（2016）27►►−→xφFx−φ−→FF对区域r中的值的访问是合理的。对于区域分配值，我们有不同的规则。由于线性约束，我们需要将区域处理程序与其他值区分开来。原语实例化的作用是用新的类型变量替换类型参数。因此，我们认为，hnd r=instantiate（σ）C=CJ，r1C; Γ，x：σx：hnd r; Γ;C;{read r}（LRHVAR）对能力r的线性限制只允许一次使用假设x：σ。hnd r=instantiate（σ）C=CJ，r+C; Γ，x：σx：hnd r; Γ，x：hnd r;C;{read r}（RHVAR）当线性限制减弱时，其使用次数不受限制。（τ，r）=instantiate（σ）C=CJ，rqC; Γ，x：σx：hnd r; Γ，x：（τ，r）;C;{read r}（RVAR）在前面的规则中，q意味着线性约束键入一个函数需要计划未来的调用。例如，如果捕获了绑定到区域值的一些自由变量，则必须在每个调用站点呈现相关的能力集。为了执行此验证，箭头类型分别用Cin和Cout来扩展所需的功能集，以评估函数体和评估终止后的新功能集。谓词unrestricted检查是否没有捕获与线性功能关联的区域处理程序。此外，我们需要传播由e，φe的求值所执行的结果。要做到这一点，我们添加一个潜在的影响到箭头类型。C;Γeρ：hnd r; ΓJ;CJ;φρ Cin;ΓJ，x：τx e：τ; ΓJ;Cout;φeCJ=CJJ，rq无限制（Cin，ΓJ）C; r=fun x→e @eρ：τC在|C位出道eτ; ΓJ;CJ;φρ{alloc r}（FUN）应用规则APP紧跟在函数规则之后在每个调用站点，我们通过检查C是否包含C来检查操作是否正确，C包含了评估函数体的相关功能这里≤可以被看作是一个子类型关系：Cv必须至少允许Cin可以执行的操作。因此，我们有r1≤r+，因为线性允许您分配和释放区域3。这种关系延伸到能力的集合。C;Γ-羟色胺：τC在|C位出道eτ;Γ ;C;φCf;Γfev：τx; Γv;Cv;φv Cv≤C，C;Γef ev：τ; Γv;Cv\（Cin\Cout）<$（Cout\Cin）;φf<$φv<$φe3 这个关系也可以读作{alloc，free}≤ {alloc}（A页）FJ. Salvucci，E.Chailloux/Electronic Notes in Theoretical Computer Science 330（2016）2733要在系统中引入功能，必须使用原语newrgn。它允许在区域中分配，读取，写入值。我们可以看到，该能力具有线性性质。在创造的时候，我们知道它没有被分享。这是收回一个地区的重要标准r∈/CC; r=1;有时需要多次使用区域处理程序。 例如当你需要传递几个区域处理程序作为函数的参数。当您使用一个函数将列表复制到两个不同的区域时，就是这种要执行此操作，aliasrgn可以提供帮助。离开这个原语的作用域可以恢复我们之前拥有的线性属性。C，r1;Γρeρ：hnd r; Γρ;Cρ，r1;φρCρ，r+; Γρe：τ; ΓJ;CJ，r+;φeC，r1; r在e：τ; rJ;CJ，r1;φρ中的平均∪φe（ALIAS）分析中最有趣的规则是FREE。在这里，线性是重要的部分，它确保区域处理程序不被共享。因此，可以以合理的方式释放相应的区域。C;Γeρ：hnd r; ΓJ;CJ，r1;φρC;Γjfreergn eρ：unit; ΓJ;CJ;φρ（FREE）我们有一组规则，提供有关程序内存行为的信息，并保证良好类型的程序不会因为内存管理而崩溃。此外，区域在编译时为我们提供了堆的抽象视图。在第6节中，我们将看到这个视图如何有助于进行资源消耗分析。3.3成本模型要执行资源消耗分析，我们需要根据内存使用情况对运行时环境进行建模。用我们的语言编写的程序可以通过创建五种不同的值来分配内存：闭包、对、列表、引用和区域处理程序。因此，我们引入了五个常量来表示一个对、一个列表节点、一个空列表、一个引用和一个区域处理程序的分配内存量。对于闭包，我们引入了一个特殊的操作符，因为使用的内存量与自由变量的数量成正比我们假设编译方案不会引入额外的堆内存分配。这使我们能够操纵将根据目标系统实例化的符号表达式。每个内存量都是一个内存字的倍数（见图4），而内存字本身取决于软件运行的平台。闭包的成本用Ccls（n）表示，其中n是闭包的大小34J. Salvucci，E.Chailloux/Electronic Notes in Theoretical Computer Science 330（2016）27值恒定大小（字）对Ccpl2列表节点Ccons2空列表C零0参考C参考1区域处理程序Chnd1见图4。 内存模型环境该分析依赖于此模型来预测实时内存的数量。3.4分析此分析的目的是在编译时提供活动内存的上限，以防止堆溢出内存流。该分析综合了若干现有的资源消耗分析。它返回函数调用所涉及的通过区域大小和区域机制，我们可以考虑回收内存。为了分析一个程序，我们将纯函数式风格的函数与命令式风格的函数区分开来要做到这一点，我们依靠语言考试系统。在这种语言中，副作用通过引用更新发生。因此，如果函数类型在区域r上标记有写效应，则该函数被认为是不纯的，并且使用基于迭代空间上的不变量的分析来分析。然而，如果函数只执行分配或读取，那么它被视为纯函数，并且可以通过自动摊销分析进行分析。如果在不逃逸的局部区域上执行侧射，则从从调用者的角度来看，这个函数是纯函数。这是我们在第6节中依赖的属性。在接下来的部分中，我们将描述每种分析如何与纯编程风格和命令式编程风格一起工作，然后我们将展示如何组合这些分析。4纯函数基于Tarjan该分析的目标是考虑这些操作之间的交互的一系列操作的成本。一个著名的例子是函数队列上的一系列操作的复杂性。函数队列q被实现为一对列表（见图5）。当我们在q中推一个元素时，我们将它添加到第一个组件的前面。当我们去掉q的一个元素时，考虑两种情况。首先，第二个组件是非空的，我们删除头部并返回它。其次，第二个组件是空的，J. Salvucci，E.Chailloux/Electronic Notes in Theoretical Computer Science 330（2016）2735ΣΣ这意味着q为空或到目前为止只执行了推送，我们在第二个组件中反转第一个组件。示例中使用的选项类型与错误处理有关。类型a选项= 没有一 | Some 的’a'a列表*'alistletpush x（xs，ys）=（x：：xs，ys）令rec取q=将 q与|（[]，[]）->无| (xs,y::ys’)->Some(y,(xs,ys’))| （xs，[]）-> take（[]，List. 版本xs）图五、在OCaml中作为配对列表的数组push：a→a queue→a queuetake：a queue→（a×a queue）选项正如我们所看到的，函数take的最坏情况执行时间与第一个组件的长度是线性的，因为调用了reverse。因此，将n个元素推入并将它们取回将是一个二次操作序列。出现这种情况是因为我们没有考虑队列的状态潜在的方法引入了信用的概念来解决这个问题。它由以下等式中的函数Φ表示，其中C（P）是程序复杂度，并且ci和ci分别表示第i个操作的有效成本和平均成本。nC（P）=cii=1吉吉 =ci + Φ（Di）−Φ（Di−1）nC（P）=（ci）+ Φ（n）−Φ（0）i=1见图6。 电位法在我们的例子中，函数Φ是队列第一个部分长度的两倍当我们将一个元素添加到队列中时，我们将付出队列的前一个状态和当前状态之间大小差异的两倍 当我们开始取出元素在队列中，对反转的调用已经被累积的信用分摊。因此，该序列的最坏情况执行时间可以减少到线性复杂度。分析的关键是Φ函数。 自动化分析需要来推断这个功能。要做到这一点，有必要增加一些限制。在本文中，我们只对线性复杂性感兴趣然后，函数Φ是函数参数的线性组合。为了找到这个函数，我们提取一组不等式来最小化。在下文中，势方法仅应用于存储器消耗。36J. Salvucci，E.Chailloux/Electronic Notes in Theoretical Computer Science 330（2016）27≥≥≥资源判断具有以下形状，并且可以被解读为n+ Φ（r）个存储器单元在e的评估之前可用，则防止堆在超流上在评估结束时，留下nJ+ Φ（τ）个存储器单元Γ，ne：τ，nJ类型用势c、d和k标注。为了可读性，我们删除了区域信息，但假设它们在需要时仍然可用τCτs|bool|int|α|⟨τa⟩−→d⟨τb⟩|(⟨τ a⟩ × ⟨τ b⟩,k)|(list ⟨τ ⟩,k)|(ref ⟨τ ⟩,k)|hnd,k见图7。 自动摊销分析该分析直接改编自早期的自动摊销分析。主要的区别是在每个区域的基础上计算的复杂性，以考虑回收的内存。它被表示为一组语法指导的规则，描述每个语言结构的内存消耗相关的约束。每种类型都用一个潜在的注释来修饰。例如，List α k表示列表类型，其中每个元素都有一个潜在的k。因此，列表势是k×length（l）。为了考虑区域的大小，我们需要使摊销分析适应区域机制。我们不考虑每一次分配，而是只计算在特定区域进行的分配。类型规则应用于特定区域r。当表达式包含注释时，只有当它在区域r中时，才计算相应的已分配内存量。当一个函数涉及多个区域时，对每个区域执行一次分析。因此，我们得到的空间复杂度涉及到每个区域的计算。n mr（AA-B OOL）Γ，nb：Bool，mn mr（AA-SVAR）Γ，nx：τs，mrn mr（AA-1NT）Γ，ni：Int，mΓ（x）=（τ，r）n≥m（AA-RVAR）Γ，n<$x：（τ，r），m原始值不需要任何开销，因为它们是在堆栈上分配的。因此，它们各自的规则传播已知的约束。rΓ（ρ）=hndrΓ，x：τx，c∈：τ，dn≥m（AA-FUN）Γ，nfun x→ e@ρ：（τx，c）→（τ，d），m如果闭包是在当前分析的区域r中创建的，那么我们需要将闭包大小视为分配的内存量J. Salvucci，E.Chailloux/Electronic Notes in Theoretical Computer Science 330（2016）2737≥≥分析是组合的，我们不能轻易地计算一个函数被应用的次数。这迫使我们添加以下限制：函数闭包中的potential contains必须为null。因此，内存消耗只能通过函数参数来参数化。r，nef：（τx，nf）→（τ，mf），mJr，mJev：τx，mrmJ−nf+mf≥mΓ，n efev：τ，m(AA-APP）功能应用需要足够的积累潜力来执行。Γ，nec：Bool，mJrr r，mjet：τ，mr，mjef：τ，m（AA-COND）r，nifec then et elseef：τ，m条件表达式传播表达式ec、et和ef生成的约束。它们与区域分配内存无关。为了组合，两个分支返回相同类型和潜在的值。对于≥关系，这将只计算分配的最大内存量rr r，nea：τa，mJr [x：τa]，mjeb：τ，m（AA-LET）令x=ea in eb：τ，mlet表达式的规则类似于条件表达式。它只将约束传播到子表达式。r，nea：τa，mJr，mJeb：τb，mJ JrΓ（ρ）=hnd r mJJ≥Ccpl+mΓ，n<$（ea，eb）@ρ：τa×τb，m(AA-P空气）对也被分配在区域。因此，如果在分析区域进行分配，那么我们必须积累足够的信用来创造这个价值。这由该约束mJJ≥Ccpl+m表示。Γ，ne：τa×τb，mn mr（AA-PROJ）Γ， nie：τi，mΓ，neh：a，mJn mr（AA-N）无：列表a，mRr，mJet：列出a k，mJJΓ（ρ）=hndrmJJ≥Ccons+k+m(AA-C（续）Γ，n<$Cons eh et @ρ：List a，m没有参数的数据构造函数表示为整数。因此，各区域不参与其评价。然而，Cons有两个参数，38J. Salvucci，E.Chailloux/Electronic Notes in Theoretical Computer Science 330（2016）27≥分配到一个区域。约束mJJ≥Ccons+k+m表征了这一点。Γ，ne：列出a k，mJΓ，mjenil：τ，mr，x：a，xs：List a k，mJ+k列econs：τ，m(AA-M（ATCH）r，n匹配e，|Nil→ e nil| Cons x xs → econs：τ，m模式匹配规则至关重要。根据所采用的分支，可以对数据结构大小做出不同的假设。例如，如果nil分支被执行，那么我们知道列表是空的。但是如果取了cons分支，那么我们知道列表中有一个元素具有它的潜力。此规则与分配地点相结合可驱动分析。nCrgn+m(AA-NEW）Γ，nnewrgn（）：τ，m分配一个新的区域会引入一个新的处理程序来对这个区域执行操作。这个处理程序被分配在它自己的区域中，并且需要Crgn内存字。当我们分享一个价值观时，我们需要相应地分享潜力。 为了仔细地跟踪这个过程，我们需要下面的结构规则，它基本上确保了势能不会被重复。r，x：τ x，y：τ y，n e：τ e，m份额（τ|τ x，τ y）（AA-S兔）Γ，z：τ，ne[z/x][z/y]：τe，m有了这个规则，可用的潜力量不能重复，而是在不同的变量之间共享。例如，Listak0意味着每个列表元素都有k0个信用。如果这个列表在变量x：Listak1和y：Listak2之间共享，那么我们生成类似于k0=k1+k2的约束。例如在这里，我们正在寻找函数duplicate的计算所涉及的区域的大小（见图9）。这个函数复制两次作为参数传递的列表。重复：（List a r，hnd rc，hnd r1，hnd r2）→（List a r1×List a r2，rc）见图8。 重复类型从这种类型（图8），我们可以看到，在一般情况下，配对列表可以分布在三个不同的区域，rc，r1和r2。J. Salvucci，E.Chailloux/Electronic Notes in Theoretical Computer Science 330（2016）27391►letrecduplicate xsr r1 r2=matchxswith| Nil->(Nil@r1,Nil@r2)@r| Cons(x,xs’)->let（ys， zs）=在（Cons（x，ys）@r1，Cons（x，zs）@r2）@ r中复制xs见图9。 功能复制复制克隆xs两次。我们可以看到，列表结构最多可以位于两个不同的区域中，并且对也可以位于自己的区域中。首先，对象分析用read{r}和alloc{r1，r 2，rc}对象标记此函数。因此，采用自动摊销分析。根据前面的说明，势函数的形式为a×|XS|其中a是每个列表元素的势，|XS|表示函数duplicate的list xs参数的大小。分析从程序中提取出一个约束系统，并试图将其最小化。Γ，n1<$（Nil，Nil）：Listak1×Listak2，m1Γ3，n3重复xs：List a k1×List a k2，m3Γ4，n4<$（Cons x ys，Cons x zs）：List a k3×List a k4，m4r，nlet（ys，zs）=（Cons xys，Cons x zs）中的重复xsr，n0将xs与|无→（无，无）| Cons x xs → let（ys，zs）=重复的xsin（Cons x ys，Cons x zs）这个函数可以在不同的区域分配内存（取决于它是如何被调用的）。我们感兴趣的是更一般的情况。区域r，r1和r2的大小是多少？为此，我们将分析应用于每个区域。因此，我们将得到三个不同的关系集来最小化。与区域r1有关的约束：n1≥m1r4= r，x：a，ys：List a k3，zs：List a k4n4≥size（a×List a k3）+k3+m4k3=k1，k4=k2123240J. Salvucci，E.Chailloux/Electronic Notes in Theoretical Computer Science 330（2016）27r =重复：列表a q0，c→列表a q1×列表a q2，d xs：列表a k0n3−c+d≥m3k0=q0，k1=q1，k2=q2当我们解决这组不等式时，我们得到q0= 2，q1 = 0和q2= 0（假设列表节点在运行时系统中需要两个字的内存）。因此，我们可以得出结论，区域r1增长2 ×|XS|.然后，我们将相同的方法应用于rc和r2。最后，我们得到了三个符号表达式表征每个区域的大小进行分配。5命令函数用命令式风格编写的程序通过使用的参考。为了考虑它们，我们需要使用不同的方法：迭代空间上的不变量。我们依赖于最近在针对Java程序的字节码级别的JConclusion项目[2]中所做的工作分析我们将这种分析应用于用我们的语言编写的程序。我们仍然依赖于用户提供不变量。它们可以用所有经典的算术和逻辑运算符来表示。这些可以由她直接提供或通过使用外部工具获得。它们是用with语法编写的，如有趣X y-> x + y与X y见图10。 带有语法与最初的工作相反，这里我们不关心逃逸记忆的概念，因为它已经通过使用区域来处理。在自动摊销分析中，我们寻找计算中涉及的不同区域的大小。为了执行此操作，不变量表征迭代次数。这里，不变量是线性关系，但用户也可以提供其他类线性不变量的优势在于我们试图推断它们。例如如果我们采用上一个示例的命令式版本，我们得到我们感兴趣的不变量描述了所涉及的数据结构的大小关系（见图12）。在r1和r2中分配的内存量从它们中提取。 它们与列表xs的长度有关。 期望的不变量在图12中。函数length表示列表结构到整数域的投影。由于副作用是通过引用执行的，因此我们还需要跟踪通过引用可用的内存量这里我们注意到3J. Salvucci，E.Chailloux/Electronic Notes in Theoretical Computer Science 330（2016）2741letduplicate xs rc r1 r2=let r=newrgn（）inletys=refNil@rinletzs=refNil@rinletrecloop es=匹配es与| 无->（）| Cons(e,es’)->ys += Cons （ e ， ！ ys ）@r1; zs += Cons （ e ， ！zs）@r2;loop esinloopxs;（！ys，！zs）@ rc;见图11。 功能复制区域不变R1长度（xs）=长度（es）+长度（！ys）R2长度（xs）=长度（es）+长度（！zs）RcCcpl见图12。重复不变量赋值是累积的，这意味着数据被添加到通过引用可访问的先前数据。因此，为了确定从它们可访问的内存量，我们依赖于相同的不变量。最后，我们解引用ys和zs，因此我们通过这些引用传播可访问的内存量。从这些，我们得到的符号表达式表征分配在不同区域的内存量。从外部来看，这个功能被视为纯粹的。区域量R1Ccons长度（xs）R2Ccons长度（xs）RcCcpl图十三. 容量的内存6分析的组成以前的分析关注的是空间复杂性，但一个程序混合了纯函数和命令的功能，涉及组合。 先前分析提供的结果这种缺乏阻碍了尺寸关系的传播，从而无法进行合理的分析。要跟踪副作用，必须以一定的精度管理参考。例如，如果一个引用被更新，那么我们需要传播关于被解引用的值的新的大小信息来进行分析。不幸的是，空间复杂性与所涉及的数据结构的大小没有直接关系的42J. Salvucci，E.Chailloux/Electronic Notes in Theoretical Computer Science 330（2016）27append函数在第一个参数方面是线性的，但返回的列表长度是两个参数长度之和。参考资料需要小心处理。例如，引用更新可能意味着大小改变。这个新的大小必须传播到程序的其余部分。为了做到这一点，我们用一个唯一的标识符来注释每个引用。引用使用它所在的区域和引用的数据所在的区域进行注释。为了跟踪效应，我们用更新的引用的标签来细化写效应。如果程序员采用精细粒度的区域机制，则可以从空间复杂度中导出数据结构大小。函数append很好地说明了这一原则。它的类型表明两个列表可以位于两个不同的区域，并且结果列表位于与第二个参数相同的区域。基本情况和输出分配器2的组合需要将数据添加到第二个列表。 因此，我们可以推断， 是作为参数传递的列表的总和当无法自动提取大小关系时，程序员必须手动为它们提供与命令式分析一样的语法以运行分析。注释可以通过使用经典的算术运算符和大小运算符来提供。这个大小运算符是一种计算数据结构的节点数的方法。绑定到整数的变量可以直接用来引用整数本身。为了进行合成，我们假设整个程序可用。组成如下的控制流程图的程序。它被表达为一组规则，其形状是C;σ;φe：σJ;φJ其中，σ和φ分别表示分配的区域的大小和量通过当前作用域中可见的每个引用可访问的内存，即语言的表达式C;σ;φn：σ;φ（CSP-INT）C;σ;φb：σ;φ（CSP-B OOL）与前面的分析一样，基元值不分配在区域中。因此，σ和φ都没有被修改。C;σ;φx：σ;φ（CSP-SVAR）C;σ;φx：σ;φ（CSP-RVAR）使用变量并不影响区域。σJ=update（σ，Ccls（fv（e）\{x}）+1，ρ）（CSP-FUN）C;σ;φ= x→e@ρ：σJ;φ通过前面的分析，我们已经知道了程序所使用的函数的空间复杂度这里我们唯一关心的是闭包本身的大小。一个字表示代码指针，其余的表示闭包环境。这里，函数update将Ccls（fv（e）\ {x}）+ 1个存储器字添加到由ρ表示的区域。J. Salvucci，E.Chailloux/Electronic Notes in Theoretical Computer Science 330（2016）2743►►►►►►►►C;σ;φ ea：σa;φaC;σa;φa eb：σb;φbσJ;φJ=instantiate（C（ea），size（eb））C;σ;φe aeb：σJ;φJ（CSP-APP）组合实际上发生在调用点，函数instantiate。这是合并符号表达式和传播副作用C;σ;φc cc：σc;φcC;σ;φ et：σt;φtC;σ;φ ef：σf;φfσJ;φJ=max（σt，σf），max（φt，φf）C;σ;φifec then et elseef：σJ;φJ（CSP-COND）条件表达式引入了运算符max的使用。为了保证分析的正确性，我们需要考虑最坏的情况。在这里，它意味着在一个区域中分配的最大内存量和从引用可访问的最大内存量C;σ;φea：σa;φa σa;φaeb：σJ;φJ（CSP-LET）令x=ea in eb：σJ;φJC;σ;φeh：σh;φh（CSP-NII）无：σ;φC;σh;φh et：σt;φtσJ=update（σ，Ccons，ρ）（CSP-CONS）C;σ;φCons eh et@ρ：σJ;φtC;σ;φe：σe;φeC;σe;φeenil：σnil;φnilC;σe;φeecons：σcons;φconsσJ;φJ=max（σnil，σcons），max（φnil，φcons）（CSP-匹配）C; σ; φ与e匹配，|Nil→ e nil| Cons x xs → econsC;σ;φ e：σe;φeφJ=add（φe，l，size（e））：σJ;φJC;σ;φrefl e：σJ;φJ（CSP-REF）当创建引用时，我们需要相应的内存量关于引用的有趣的事情出现在赋值的时候。我们必须更新相应引用可访问的内存量。这就是函数update对φ的作用。 此更新取决于分配的性质。如果是累积的，那么我们在已经可用的44J. Salvucci，E.Chailloux/Electronic Notes in Theoretical Computer Science 330（2016）27数量上增加一些内存单词。如果是非累积的，那么我们引入一个max操作符来保持可访问内存的最大量。J. Salvucci，E.Chailloux/Electronic Notes in Theoretical Computer Science 330（2016）2745JC;σ;φef：σr;φrC;σr;φrev：σv;φvφ=update（φv，label（er），size（ev））C;σ;φer：=ev：σJ;φJ（CSP-A SIGN）要分配一个新的区域，您至少需要有存储区域处理程序所需的内存量。σJ=update（σ，Crgn，ρ）C;σ;φnewrgn（）：σJ;φ（CSP-NEW）记录（σ）σJ=free（σ，ρ）φJ=clean（φ，ρ）C;σ;φ自由能ρ：σJ;φJ（CSP-FREE）类型系统检查对应于ρ的区域可以以安全的方式回收。因此，我们可以忽略这个区域的大小来计算活内存的上限当我们释放内存时，存在一个局部最大值。我们需要保存区域大小的总和来跟踪最大的活动内存量。在分析结束时，我们取每个局部最大值之间的最大值。我们不需要考虑在执行结束时可用的内存量，因为类型规则会检查没有区域是未声明的。7例如以下示例显示如何执行分析。主要的函数是rev append，它通过反转第一个列表使其成为尾递归来连接两个列表。这个函数至少可以用两种不同的风格编写：纯函数式和命令式。这个程序构建两个区域r和rr，并分别在r和rr中分配两个列表xs和ys。然后，它通过