资源受限函数式程序设计语言的类型推理与内存分配成本评估

理论计算机科学电子笔记151（2006）27-45www.elsevier.com/locate/entcs资源受限函数式程序设计语言斯蒂芬·吉尔摩1爱丁堡大学计算机科学基础实验室，爱丁堡EH9 3JZ，苏格兰Olha Shkaravska2Ludwig-Maximilians-UniversitaütMünchen，Lehr-undForschungseinheitTheorretischeInformatik，Oettingenstraße67，D-80538München，BundesreektikDeutschland摘要我们解决的问题，在实践中应用面向对象的虚拟机，其中包括调用本机方法编码的低级语言，没有垃圾收集支持资源受限的函数式编程语言。我们考虑的应用程序的功能语言与一个高层次的类型系统，其中包括在这样的执行平台上的类型的堆空间消耗的措施。我们补充的语法类型推理过程的函数式语言与一个单独的分析，估计所产生的调用垃圾收集无知的功能的内存泄漏的成本关键词：资源受限函数式编程语言，本地方法调用，面向对象虚拟机1介绍Camelot是一种资源受限的函数式编程语言， 结构化的Java字节码，运行在未修改的Java虚拟机上。Camelot函数回收内存位置，以减少执行的对象分配数量，从而减少垃圾收集的成本。评估Camelot函数的对象分配成本计算的语法类型推理过程，检查的Damas-Milner风格的功能的抽象结构表达。一个类型被分配给一个函数，该函数既包括1电子邮件地址：stg@inf.ed.ac.uk2电子邮件地址：shkarav@informatik.uni-muenchen.de1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.03.01028S. Gilmore，O.Shkaravska/理论计算机科学电子笔记151（2006）27通常的表面类型指定函数参数和结果的类型，以及成本表达式指定根据输入数据结构的大小分配的对象的数量。Camelot还提供了一个外部函数接口，允许应用程序开发人员调用Java方法。Java本身也有Java本地接口（JNI），它允许Java方法调用没有等价字节码表示的函数。这些是典型的C例程，用于操作原始内存、访问外围设备或分配非Java对象（如操作系统资源）。在某些情况下，这些可能是来自专有源的库函数，仅作为编译后的图像提供，没有相应的程序源代码。在这种情况下，即使在库代码中检测到空间泄漏，如果没有源代码，也不可能修复。你只能提交一个bug报告，等待维护人员在下一个版本中修复这个问题实际上，Camelot程序需要调用这样的本地方法来执行诸如构建和显示用户界面组件之类的任务 类型推断算法，保证资源消耗界限的应用程序编写完全在卡米洛特是不适用于这种情况下，因为不是所有的程序文本可用于检查和查询，并不是所有的程序文本是在卡米洛特语言在任何情况下。在本文中，我们提出了一个完整的基于资源的分析，可应用于（不纯）Camelot应用程序调用Java方法调用C函数。本机方法的调用会影响Camelot应用程序对内存堆分配的推断，因为调用的本机方法本身可能会分配内存。 这个内存分配在JVM的垃圾收集器无法访问的地址空间中。如果这些本机方法本身不释放它们分配的所有内存，那么这种效应将在我们的应用程序中表现为空间泄漏空间泄漏在短期应用中不是一个非常重要的问题， 它们在长时间运行的应用程序中非常重要，例如服务器端代码，它打算运行数周或数月而不会失败。随着越来越多的空间在长时间运行的应用程序中泄漏，新内存的分配变得毫无意义。 在短期内，这会导致性能下降 从长远来看，应用程序会因内存不足而失败。因此，我们的分析最适用于服务器端代码，但在服务器端也是使用本机方法的正确位置。本机方法不是Java字节码意义上的在线可移植代码。为Unix平台编译的本机方法不会在Windows下运行，反之亦然。可移植性是要在客户端机器上运行的代码的一个重要问题，因为不同的客户端将具有不同的操作系统和硬件，但不可移植性在服务器端不是同一个问题。通常情况下，在服务器上运行的Java应用程序将完全通过使用“提前”优化本地代码编译器（如BulletTrain，SpecialJ或GCJ）编译为本地代码。因为我们在这里描述的分析是专门为本地方法量身定制的，所以它是由代码生产者作为软件开发和调优的一部分应用的，而不是由S. Gilmore，O.Shkaravska/理论计算机科学电子笔记151（2006）2729代码消费者作为代码验证过程的一部分我们提出了一个基于资源的分析，预测资源消耗作为时间的函数。 分析的主要结果是量化本地方法相对于整个应用程序的空间泄漏的严重性。这种分析为不纯的服务器端Camelot应用程序构成了一个软类型系统。分析并不拒绝任何程序，而是对其空间泄漏的严重程度进行分类。 即使是存在严重空间泄漏问题的应用程序，可以在足够大的服务器上使用足够长的时间，对服务器的定期维护可能会导致它在应用程序没有泄漏足够的空间以使其成为真正关注的时间段内被关闭。在分析中必须将来源不可用的C函数视为不透明（“黑盒”）的情况下，基于资源的分析将必然依赖于使用量化近似，因为模型使用的概率和平均持续时间是正式的。这导致了一个随机过程的定义，用于表示研究中的不纯Camelot应用程序本文结构：在下面的部分中，我们将概述Camelot，一种扩展的严格一阶函数式编程语言。我们详细介绍，特别是这些功能的Camelot语言提供了重用堆分配的内存。在第3节中，我们给出了纯Camelot程序的堆使用分析的概述。我们讨论了这两个在高层次的函数语言中的堆空间消耗的界限，然后在低层次的字节码，我们的高级程序编译的Camelot编译器验证。在此之后，我们继续在第4节提出一个新的分析，显示如何不纯Camelot程序调用C例程可以分析其空间消耗行为。我们描述了用于计算分析结果的工具。结论见第5节。2卡米洛特Camelot编译器以Java虚拟机为目标，并为重用内存提供语言支持。JVM不提供释放内存的指令，而是将其委托给垃圾收集器，这是一个分代收集器，有三代，实现了停止并复制和标记清除收集。Camelot运行时通过将未使用的地址添加到未使用的内存的空闲列表中来处理它们。在程序引起的下一次分配中，从空闲列表的头部检索存储，而不是由JVM新指令分配。当空闲列表变为空时，所需的存储空间由new分配。这种存储机制适用于Camelot，但不适用于Java，因为Camelot使用由编译器生成的类型的统一表示，允许数据类型交换存储单元。这种统一的表示被称为钻石类型[4，5]，由Camelot运行时中的Diamond类实现的30S. Gilmore，O.Shkaravska/理论计算机科学电子笔记151（2006）27Camelot语言的类型系统将类型分配给函数，这些函数记录它们消耗的参数数量及其类型;结果的类型;以及消耗或释放的钻石数量2.1函数式和命令式编程可以使用类型安全的地址重用的一个例子是列表更新函数。 与通常的非破坏性列表处理一样，一个函数依次对列表中的每个元素进行映射，在该函数下构建元素的镜像列表。与map等函数的通常实现相反，破坏性版本通过将每个cons单元格的内容与函数下元素的图像进行映射来就地应用函数，它遍历列表。下面的简单函数递增整数列表中的每个整数。Camelot的具体语法类似于Caml的具体语法。在地址不被操纵的情况下，如这里，Camelot函数也可以由Caml编译下面使用的构造函数当在模式匹配的上下文中用在箭头的左边时，它将把一个非空列表分解成它的头和尾。 当用在箭头的右手边时在表达式的上下文中，它将构造一个cons-cell来将新元素添加到列表的前面让 rec incListlst =匹配第一个[] −>[]| h：：t−>（h + 1）：：incList t以上是列表处理函数的非破坏性版本，它分配与列表中的元素一样多的cons-cell在下面的版本（“destIncList“）中，因此，此版本不分配任何存储。下面使用的构造函数当在模式匹配的上下文中在箭头的左手侧使用时，它将获得cons-cell存储的地址（类似于C的address-of操作符，但没有缺乏类型安全或指针相关内存故障的问题&当在表达式的上下文中用于箭头的右侧时，它将在给定地址处存储cons-cell（从而将存储在那里的分配让rec destIncListlst =匹配第一个[] −>[]| （h：：t）@a −>（（h + 1）：：destIncList t）@a在此函数的高阶版本（破坏性映射）中，如果函数参数不分配内存，S. Gilmore，O.Shkaravska/理论计算机科学电子笔记151（2006）2731存储，则破坏性映射函数的应用也不会。以这种方式选择性地使用就地更新可以用于实现森林砍伐，这是一种消除不必要的中间数据结构的程序转换，这些中间数据结构是在计算过程中构建的2.2线性作为一个在Camelot中不可类型化的函数的例子，我们可以考虑下面的一个。这个函数试图创建一个列表的修改后的副本，与原始列表交错。在实现这个函数的过程中，一个（故意的）错误是试图将cons单元格存储在列表的前面，而将cons单元格存储在second中 在同一地点，D。让 rec incListCopy lst =匹配第一个[] −>[]|（h：：t）@d −>让 tail =（（h + 1）：：t）@din（h：：tail）@d（错误：d使用了两次！ ）Camelot编译器将此函数设置为错误，并显示以下诊断错误消息。文件“incListCopy.cmlt”，第4-5行，字符18-80：！..................令tail =（（h +1）：：t）@d！in（h：：tail）@d....！<>类型的变量d非线性使用上面的destIncList函数演示了Camelot中的存储重用。作为存储器重新分配的编程控制的示例，考虑下面所示的破坏性求和函数。对一个整数列表的元素求和--或者更一般地说，将一个函数折叠到一个列表上--有时是对列表执行的最后一个操作，从列表中的各个值得到一个累加的结果。 如果如果是这种情况，则此时可以回收列表占用的存储，在遍历列表时这样做是很方便的let recdestSumList lst =匹配第一个[] −>0| (h:: t)@−> h + destSumList t将对象的位置与一个标记模式（符号）进行匹配表明不需要这个地址（因为它没有绑定到名称），因此可以释放它。destSumList函数在遍历列表时释放列表在高阶版本中，例如破坏性折叠，我们将具有内存回收能力，函数作为参数传入，也可以释放列表元素占用的存储空间，如果这些元素是其他占用存储空间的对象，例如列表或树。32S. Gilmore，O.Shkaravska/理论计算机科学电子笔记151（2006）272.3面向对象特性Camelot类包含可以调用与任何类无关的函数的方法。在Camelot的对象子语言和函数子语言之间的接口处，有必要指定函数的形式参数的类型。因此，在下面的（人为的）示例中，有必要指定id函数的参数类型（一个Camelot类的例子，它的方法调用了一个在类。类调用示例=方法myName（）：string = id端letid（s：string）= s像往常一样，在函数式子语言中，类型推断过程几乎消除了程序员提供类型信息的所有需要2.4执行Camelot编译器以与大多数函数式编程语言编译器非常不同的操作模式运行，因为它专注于对空间消耗进行可预测的分析，并且如果不知道优化总是保证改善基于类型的分析的空间使用，则故意不应用优化。 Camelot编译器也被构造为以一种倾向于增加我们对其正确性的信心的方式，转换成一种叫做Grail的Java字节码的结构化方言。Grail是结构化的字节码，因为它是A范式（函数和原语仅适用于值）。Camelot编译器可从www.example.com免费下载http://groups.inf.ed.ac.uk/mrg/camelot/。3分析为了解释不纯Camelot应用程序的分析背景，我们首先 对纯Camelot应用程序（不调用其他语言编写的Camelot [5]的现有推理过程跟踪堆分配，以报告Camelot函数调用分配的堆内存量。 这个成本表示为输入参数大小的函数。 成本可能 如果当前分配的内存被调用释放并在Camelot运行时返回到托管空闲列表，其他类型的记忆使用没有记录。具体而言，堆栈分配不被分析跟踪。因此，Camelot函数可能会失败，原因是它们递归得太深，以至于它们覆盖了Java运行时堆栈。这在原则上是可能的--堆空间分析中没有任何东西阻止S. Gilmore，O.Shkaravska/理论计算机科学电子笔记151（2006）2733·►►这在实践中也会发生，需要开发人员重写代码以防止此错误。3.1Camelot函数Camelot运行时提供了一系列未使用的堆单元（“菱形”）。 当 那么就需要一颗• 除非自由空间是空的，否则它是从自由空间中取出的• 否则执行JVM新建（分配）。解除分配意味着将“钻石”归还给自由党。推理过程旨在解决以下任务：为了找到，如果它们存在，line是一个函数和一个值的大小，函数δ−（·）和δ+（），使得如果frequencies至少包含δ−（x1，. . .，x m）“钻石”，f（x1，. . .，x m）以值v终止，则在求值期间不分配新的堆单元，并且在求值之后将至少有δ+（v）“菱形”在Fredom。推理规则是为记型系统设计的例如，类型L（A，k）的值是类型A的元素的列表，使得每个元素在freecycle中有k个堆单元，其起到“信用”的作用。判断Γ，ne：A，nJ意味着在标记的类型化上下文Γ中有签名并且有n个额外的“diamonds”可用的情况下，项e具有标记的类型A，剩下n j个未使用的“diamonds”。 为了简单起见，我们将省略下标。符号在任务中提到的线性边界函数δ−，δ+中扮演着系数的角色。更详细地考虑打字判断的含义。例如，对于一个表达式e和它的自由变量x，其类型为L（L（int）），我们得到以下类型：x：L（L（int，2），4），6 e：L（int，3），1。 这意味着如果x被评估为[l1，. . . ，l m]，并且e的评估以结果l终止，并且frequencies具有至少6+l i= l，.， m（4+2 |L i|）= 6+4 m+2 m i=1，.， M|L i|“钻石”，那么经过评价后至少会有1 +3 |L|“钻石”在自由女神像（|·|表 示 列表的长度）。作为带注释的推理规则的一个示例，考虑用于破坏性模式匹配的规则：Γ，n∈1：A，nJΓ，x h：A，x t：L（A，k），n+ 1 +k<$e2：A，nJr，x：L（A，k），n无->e1| (x h::x t)@->e2：A，nJ34S. Gilmore，O.Shkaravska/理论计算机科学电子笔记151（2006）27►−前件中的1+k之和表明，为了评估e2，人们可能需要额外的1+k一个额外的堆单元是在破坏性模式匹配时通过释放提供的。 k个堆单元肯定是在自由空间中， 仅仅因为这是匹配细胞的必要“信用”。将上面的规则与非破坏性匹配的规则进行比较：Γ，n∈1：A，nJΓ，x h：A，x t：L（A，k），n+k<$e2：A，nJr，x：L（A，k），n无->e1|（x h：：x t）-> e 2：A，nJ这里，可以提供由匹配单元的信用保证的仅k个额外的“钻石”。整个打字系统都很可靠。表示的操作语义，其中关系m，E，h e~v，hJ，mJ意味着e与环境E和堆h的评估在存在大小为m的随机数时终止，其中一个值v，修改后的堆hJ，而自由度有mJ个 这里，通常情况下，环境（堆栈）E：V ar~ V al是从变量到值的有限部分映射，堆h，hJ：Loc~ V al是从位置集到值的有限部分映射。使用标注类型系统，可以获得给定Camelot的标注签名 功能， 像“ 不到位，复制功能。第一个是用变量而不是num来增加类型派生为给定的函数生成一个有符号的派生树。 然后一个人收集 并求解由规则的边条件引起的数值线性约束。假设由变量值占据的堆区域的良性共享，约束系统的解包含线性堆边界的期望系数，函数-它们是它的签名中的符号被称为良性共享的语义条件意味着，如果在程序评估中的某个点，堆单元被破坏性模式匹配释放，则该单元不能从连续中出现的变量访问。这个条件是在语言的操作语义层面上制定的。证明给定Camelot程序的已编译Grail图像的谓词（回想一下，Grail是Camelot 编译成）我们必须静态地近似这个条件。 到目前为止，这基本上是通过线性使用Grail变量来完成的。我们正在考虑不同的可能性，使良性共享的近似限制较少。有一些方法可用，例如，参见关于使用方面的论文[1]或分层共享的工作[7]。一般来说，该方法不需要在标注的操作语义中为数字子化人们把它看作是S. Gilmore，O.Shkaravska/理论计算机科学电子笔记151（2006）2735（Ⅲ）（Ⅲ）可用的免费单位数。假设有一个垃圾收集器，而不是维护一个自由空间。然后，给定一个函数程序f，如果存在的话，我们找到线性界δ−（ ·），δ+（ · ） ， 使 得 如 果f （ x1 ， ...， xm ） 终 止 于 值 v ， 并 且 如 果 至少存 在 δ-（x1，. . . ，x m）可用的空闲单元，然后在占用N个堆单元的情况下开始评估，如果我们每次都运行垃圾收集器，当占用单元的数量达到N+δ−（x1，. . .，xm），则在评估期间，占用单元的数量将永远不会超过N+δ-（x1，. . .，x m）。3.2堆边界我们需要证明，对于所考虑的卡米洛特计划的圣杯图像，同样的函数δ−和δ+我们为圣杯计划U，n，ΓA，m，其定义基本上对应于高级类型判断Γ，n∈e：A，m的含义，其中U包含e的自由变量集。为了获得自动的，语法驱动的，证明这样的谓词，我们应用派生的规则，反映了高层次的标记类型规则。Grail规则被证明是先验的，适用于Grail加上frequencies管理函数make和free的任何语法结构。比如说，r（x）=L（int，k）Diamond.Free（x）：U，0，ΓL（int，k），1人们可以立即看到我们方法的技术局限性。如果必须证明一个圣杯方法m1，调用另一个方法，比如m2，那么最终m2的指定应该以上面的精确形式出现在指定表中。这意味着：• 或者m2是Camelot函数的图像并且m2的指定是可导出的，• 或者外部提供规格为了估计我们的方法的可靠性，我们建议应用统计方法。人们可以单独考虑不纯Camelot应用程序的“纯”子程序，然后• 评估（统计学上的）来自本机调用的可能的• 并评估原生呼叫的概率在本文中，我们集中在前一个任务。4分析不纯的Camelot应用程序回想一下，Camelot程序编译为Java字节码，可以在未修改的JVM上执行。卡米洛特程序的编译版本36S. Gilmore，O.Shkaravska/理论计算机科学电子笔记151（2006）27Java平台的API，而Java语言反过来又有一个外部函数接口，用于调用用C编写的本地方法（JNI）。我们给出了一个这样的相互作用的例子，从堆消耗的角度来看，这会导致致命的后果。考虑一个Camelot程序，该程序具有一个Java方法调用，调用的方法allocate适用于outOfMemory类的对象实例。下面的程序引入了这样一个对象实例（名称为c），并在名为allocLoop的递归函数中调用allocate方法。（ACamelot program which repeatedly calls a Java method）valmain：string array −>unitvalallocLoop：unit −>unitlet recallocLoop（）=让 c =new outOfMemory（）in（. a Java class（）let= c#allocate（）in（）. native method call（）allocLoop（.此函数的尾调用（）letmain s = allocLoop（）下面给出了Java类outOfMemory的实现/Camelot程序使用的Java类/public classoutOfMemory{//public voidrun（）;/在类加载时间执行的数据块的状态/静态{/n使用编译后的alllocate（）方法的C实现加载共享对象库/系统loadLibrary（}}C函数allocate每次被调用时都会分配一些内存。显然，这一进程不可能永远持续下去下面的C程序包含从上面给出的Java类调用所/C函数编译为一个可供Javaclas使用的共享库/#include jni.h>#include#include stdio.h>JNIEXPORTvoid JNICALLS. Gilmore，O.Shkaravska/理论计算机科学电子笔记151（2006）2737Java outOfMemory allocate（JNIEnv内存分配，jobject对象）{printf（“正在分配内存...”）;/如果返回空指针，则可能会失败/if（（voidsets）malloc（102400）== NULL）{printf（“失败！"}否则{printf（}返回;}在一个典型的Linux平台上，这个程序会非常迅速地分配内存，填满可用的实际内存。然后调用Kernel Swap Daemon（kswapd）将内存页交换到交换文件中。 很快，交换文件就会填满，程序可能会被操作系统杀死（从而释放它所占用的所有内存），或者可能只是挂起，要求程序 被用户或要重启的机器杀死当没有剩余的内存需要分配时，尝试分配内存的效果最终取决于malloc函数的定义。malloc函数是在C语言规范中定义的，用于标准库在无法分配所需内存时返回空指针在C程序中，任何对malloc的调用都必须准备好处理作为结果返回的空指针这是Camelot应用程序的形式，我们试图通过随机建模进行分析（Camelot调用Java，调用C），因为它不适合Hofmann和Jost [5]的精确空间推断4.1分析详情我们对不纯Camelot应用程序的统计分析是通过首先遍历程序以获得其控制流程图来进行的。在此过程中，与应用程序逻辑相关的许多信息可以被抽象掉。算术表达式求值和其他不引起堆分配事件的计算部分，或者调用本地方法或调用纯Camelot函数可以被删除，以便制定一个明显更简单的程序，其余的分析是基于这个程序的。在这一点上，程序中的大部分数据依赖性被删除，并被控制流行为的统计近似值所取代。因此，一个决定性的条件表达式可以被替换为替代方案之间的概率选择，并且条件表达式中的测试中包含的条件表达式本身可以被删除，如果它的评估直接或间接地在堆上分配没有存储，并且没有调用本地方法。由模式匹配评估引起的多路分支可以类似地处理以给出化合物38S. Gilmore，O.Shkaravska/理论计算机科学电子笔记151（2006）27−→概率选择在Camelot程序中调用本机函数的地方，我们插入一个可能的故障点，表示致命的内存不足错误，该错误会突然终止程序的执行。这些事件的相对频率也需要估计。如果我们可以使用Dmalloc、Valgrind等工具确定本机代码例程没有空间泄漏，则可以消除其中一些潜在的故障点 或其他[9]。为了反映在这一点上已经应用于程序的强简化，我们选择将其渲染为不同的形式语言，Ramsey和Pfeedere：：= x|v| λx.e|e1e2|设x=eJin e|选择p e1e2| e. |e. 1 |e. 2|Le1|Re2|casee e le r随机lambda演算的显著特征是在备选方案之间的概率选择（选择p e1e2以概率p评估为e1，以概率（1p）评估为e2其余的结构更熟悉，包括值的左标签和右标签，以区分异常（或错误）结果和良好值。case构造测试这样的标签，并将子表达式el和er分别应用于携带的值。我们使用通常的数据类型（如布尔和整数），并构建-在succ、pred和cond等函数中，此外，我们使用sizeof等函数来返回类型的机器表示的大小。 为了便于阅读，我们将succ（x）写成x+1，并将三位条件函数cond bexp exp1exp2的应用写成如果 bexpthenexp1elseexp2 。 同 样 为 了 可 读 性 ， 我 们 有 时 会 写 letx=e1inlety=e2ine3asletx=e1;lety=e2;e3。在确定不会产生歧义的情况下，我们将省略这种句法形式中的分号。 我们也将添加多余的括号，如果他们似乎需要澄清复杂的复合表达式，其中包括多个子表达式。4.2例如考虑一个类型为List unit的Camelot函数，如果输入列表的长度为偶数，则该函数调用静态Java方法fnative。我们假设fnative的主体包含一个C函数的本机调用，可能存在内存泄漏。let recevenOddLength lst =匹配第一个[]->fnative（）| h：：t->matcht with[] −>（）| hh：：tt −>（evenOddLength tt）S. Gilmore，O.Shkaravska/理论计算机科学电子笔记151（2006）2739≡−假设我们已经得到了，比如说实验上的，列表长度为偶数的概率p。 我们可以将一个列表抽象到它的长度，并得到一个非常简单的随机λ-项，表示Camelot函数的主体choosep memleak（）我们插入了一个潜在的内存泄漏点，而不是Java方法调用，假设我们不能保证本机调用不包含内存泄漏。我们想把随机λ-演算中的一项映射到马尔可夫链上，马尔可夫链的状态反过来也是项。链的跃迁用对（α，r）标记，α表示动作，r表示速率。速率是比转移概率更一般的概念，在某种意义上，两个分支转移的两个速率之和不一定等于1。例如，考虑随机λ -演算中的函数f（lst），其主体由上面的项表示：echoose p memleak（）。 在这个简单的例子中，函数体不包含lst作为自由变量。在列表x上调用此函数的转换图将具有以下形式f（x）（f，r））e[lst：=x]memleak（（），r2）v（）比率与概率成比例：ri=kpi，对于某个正k，其中p1=p，p2= 1-p。比率r等于r1+r2=k。4.3二示例考虑 表示Camelot 函数 的随 机lambda 演算 项， 其 以概 率pc将调 用 Java方法javaMethod，并且以概率1pc将调用另一个Camelot函数camelotFn。当分配完成时，我们跟踪可用程序内存m的结果在一个case表达式中检验.如果所有的内存分配都成功了，那么函数将递归执行其他函数或方法调用，否则应用程序将退出并出现内存不足错误。字母循环 = λm。让步骤=choose（pc）（javaMethodm）（camelotFnm）如果步骤循环退出已经使用Hofmann-Jost类型系统确定了Camelot函数不分配存储器，则我们可以使用表示当前存储器级别（当前存储器级别）的保留的随机lambda演算项对此进行建模。40S. Gilmore，O.Shkaravska/理论计算机科学电子笔记151（2006）27值标记有L标记，表示成功）。设camelotFn = λm。Lm检查Java方法，我们意识到这要么调用纯Java方法（编译为类型安全的，垃圾收集的字节码），bytecodeMethod，要么调用本机函数（编译为类型不安全的，内存不安全的本机代码），nativeFn。概率为pb，它是被调用的字节码方法让javaMethod = λm。choose（pb）（bytecodeMethodm）（nativeFnm）与Camelot函数一样，我们可能已经能够确定字节码方法不分配任何内存，在这种情况下，它太简单地保留了当前内存。设bytecodeMethod = λm。Lm由于其控制流，本机函数调用并不总是导致空间泄漏。有时内存在分配后会被释放;或者在某些调用中内存没有被分配。因此，另一个概率变量进入模型：该函数的该应用将导致空间泄漏的概率，pl。使得nativeFn=λm。choose（pl）（leakSpac em）（noSpaceLeakm）没有空间泄漏的结果与我们看到的其他结果类似在空间泄漏的情况下，返回失败结果或成功结果，这取决于是否有足够的内存可用于满足当前分配请求。通过alloc t表示当前请求的分配类型。令leakSpace = λm。ifm>sizeof（alloct）那么L（m−sizeof（alloct））否则R（m）为了利用程序的这种表示，有必要用计算中事件的相对频率及其持续时间的估计来播种随机lambda演算模型。在进行程序分析时，需要尽可能准确地估计这些量。理想的情况是从成本模型中导出这些数据值，Grail语言[2]，但是我们的技术目前还不是很先进，所以我们从我们的软件实现的工具和测量中幸运的是，现代JVM（如SUN这概括和扩展了Java虚拟机平台编程器架构和Java虚拟机配置接口，以提供对Java虚拟机管理的编程访问，并促进在运行时对Java字节码的插装。S. Gilmore，O.Shkaravska/理论计算机科学电子笔记151（2006）2741在随机lambda演算实现中建立了程序的抽象表示，并通过仪器，测量或其他手段获得了事件发生频率的估计，我们现在能够进行分析。4.4分析过程我们首先从我们的随机lambda演算项推导出约简序列。在任何确定性lambda演算中，这样一个推导序列中的分支可以通过选择一种归约策略来去除，该归约策略确定了下一个要被归约的整体的单个子项，并且连续性保证了将获得相同的最终结果。在随机lambda演算中，源于概率选择的分支不能被移除，因此来自给定随机lambda演算项的约简路径通常是树。这个树在叶子上有致命的内存不足事件（lambda演算表示），我们感兴趣的是从根到这些叶子之一的路径的持续时间。现在，我们已经制定了一个随机过程分析过程的问题。我们希望计算这个活动的时间分位数，所以我们转向随机过程分析工具。我们已经使用DNAmaca分析仪[6]和PRISM [8]用于该模型。在马尔可夫模型中，有两种分析值得一提，因为它们将对模型的不同见解结合起来。第一个是稳态分析，从长远来看，当任何初始预热期已经过去时，它会观察模型的行为。 第二个是瞬态分析，它着眼于行为模型在某个时刻（可能接近其生命周期的开始）的 并且仍然在系统初始配置的任何影响的范围内。我们在这里进行后一种分析。我们的分析工具的结果可以呈现为概率分布函数（PDF）或累积密度函数（CDF）。 前者的含义是被测事件在这一瞬间发生的概率在时间上（因此，当时间趋于无穷大时，PDF的值趋于零，因为事件变得更有可能已经发生）。后者的含义是测量事件发生的累积概率随时间的增加而变化（因此，CDF的值随着时间的增加而趋于1，因为事件变得更有可能已经发生）。 所呈现的图表图1和图2显示了4.3节中给出的上述随机lambda演算模型的结果。由于这是对计算机应用程序的实时分析，询问是否可以简单地通过重复运行应用程序来获得相同的信息。答案是，这种信息可以通过实验以这种方式获得，但计算时间的成本将非常昂贵。为了根据实验数据绘制上图，需要重新运行应用程序并积累足够的故障点观察结果，以便可以有意义地计算以下情况发生的次数百分比：42S. Gilmore，O.Shkaravska/理论计算机科学电子笔记151（2006）27随机lambda演算模型的CDF图10.90.80.70.60.50.40.30.20.1002040 60 80 100 120天数图1.一、由于累积空间泄漏而导致的系统故障概率的累积密度图这些失败发生了。即使我们满意地认为只有100次运行的应用程序足以让我们为长期运行的程序（如本文中考虑的程序）计算统计上有效的结果，这也意味着一系列实验的运行时间将以数十年的计算时间来衡量，这是不可行的。通过对底层连续时间随机过程的瞬态分析进行的实时分析给我们带来了好处，我们可以从短运行时间（基于每个函数）推广到长运行时间（从系统初始化到系统故障）。4.5结果比较和讨论图1和图2显示了系统故障的概率如何随着时间的推移而增加。因此，所有的曲线图都显示了累积概率从零增加到一。为了绘制这些图，我们保持函数调用时间的持续时间不变，只改变调用各种函数的概率在图1中变化的概率是pc，即调用Java方法的概率。空间泄漏只发生在Camelot应用程序中，因为Java方法是这样调用的。 由于进行这些呼叫的概率降低，因此由于存储器耗尽而导致的系统故障的可能性也降低。我们在这个图中保持pb和pl常数（0.5）。在图2中，我们展示了被调用的自然方法泄漏空间的概率“p_c=0.1”“p_c=0.25”“p_c=0.5”“p_c=0.75”“p_c=0.9”由于空间泄漏导致S. Gilmore，O.Shkaravska/理论计算机科学电子笔记151（2006）2743随机lambda演算模型的CDF图10.90.80.70.60.50.40.30.20.1002040 60 80 100 120天数图二. 由于累积空间泄漏导致系统故障概率的累积密度图，随时间变化。p= 0时的值。即使在t = 115时，1也低于0.0015。0.如果我们没有进行我们所做的定量分析，这个值的变化对坠毁可能性的影响比我们所预期的要明显结论是，降低泄漏的概率对应用程序的寿命有显著影响，将泄漏的影响降低到可以容忍的程度，因为周期性系统重置将在任何情况下清除所有泄漏的内存。在这幅图中，我们保持pb和pc不变（0.5）。5结论我们已经讨论了Camelot编程语言，这是一种创新的高级函数编程语言，它在其类型系统中表示资源消耗信息。为了使原则性编程语言有用，它还必须对实践做出让步[3]。Camelot编程语言允许用户调用Java方法，这些方法又可以调用低级语言（如C）中的本机函数我们在这里花了一些时间来讨论如何与高级语言分析进行互操作这里讨论的问题是潜在的内存泄漏（在调用本机方法时有一定概率发生）将如何影响整个系统。质量问题，最终结果是肯定的：内存泄漏最终会导致系统“p_l=0.1”“p_l=0.25”“p_l=0.5”“p_l=0.75”“p_l=0.9”由于空间泄漏导致44S. Gilmore，O.Shkaravska/理论计算机科学电子笔记151（2006）27失败但是，我们在这里感兴趣的是定量分析：“内存泄漏多久会导致系统故障？” 对这些问题的回答可以- 不能通过实验确定，因为确定这些的实验过程（重复重新运行长时间运行的应用程序）的成本太高。这里需要进行形式分析，这在这里很有用我们已经考虑了程序的某些部分（用Camelot编程语言编写）可以接受检查和查询，但其他部分（C应用程序的预编译库映像）则不可以。因此，我们进行的分析必须不可避免地利用近似，因为C函数的完全可测性是未知的。我们使用外部对函数行为的观察，这些观察可以从时间和空间精确的轮廓仪的轮廓信息中获得。这些都可用于现代JVM，并且还详细说明了本机方法调用的成本。我们的分析关键取决于这些近似的准确性。我们使用的近似是相反的函数堆空间分析的纯子集的卡米洛特语言由于霍夫曼和约斯特，这是一个精确的分析，不使用近似。种子与随机过程表示的不纯Camelot appli-阳离子通过随机lambda演算中间形式获得，transformation到一个连续时间马尔可夫链，变换通过均匀化，瞬态解和累积密度函数计算是完全自动的，可以执行低计算成本，指出这种方法的潜在有用性的系统比这里考虑的更大我们考虑的例子是一个相对简单的例子，控制流程简单。然而，我们用来分析这个例子的方法具有更大的普遍性。映