Safe：一种基于区域的堆的一阶渴望函数式语言的编译和验证

理论计算机科学电子笔记246（2009）167-182www.elsevier.com/locate/entcs一种具有显式释放的我的朋友2RicardoPensoula1，3 ClaraSegura1，3DepartamentodeSistemasInform′ticosyComputacio′nUniversidadComplutense de Madrid摘要Safe是一种一阶渴望语言，具有堆区域和不寻常的设施，如程序员控制的销毁和数据结构的复制。 这些区域是堆中不相交的部分，编译器可以在其中分配数据结构。多亏了区域，运行时垃圾收集器是不需要的。 该语言及其相关的类型系统，保证销毁设施和区域管理在一种安全的方法，以前已经提出过。本文从Safe的高级大步操作语义出发，经过一系列半形式化的步骤，将其编译为命令式语言和命令式抽象机。一旦机器的内存需求是已知的，我们丰富的语义与内存消耗注释，并证明丰富的语义是正确的翻译和抽象的机器。所有步骤都是以这样一种方式导出的，即很容易理解翻译并正式确定其正确性。保留字：函数式语言，基于区域的堆，抽象机，代码生成。1引言Safe是一种一阶渴望函数式语言，具有程序员控制的数据结构销毁和复制功能。它还提供了地区，即编译器分配数据结构的堆的不相交部分。这些区域的分配和释放与功能应用程序相关联。安全语言及其共享分析发表在[11]中。我们还定义了一个类型系统和一个类型推理算法[10，9]，保证销毁设施和区域管理以安全的方式进行1由马德里地区政府以赠款S-0505/TIC/0407（PROMESAS）提供部分支助。2 电子邮件：montenegro@fdi.ucm.es。由MEC FPU资助AP 2006 -02154支持的工作。3 电子邮件：ricardo@sip.ucm.es，csegura@sip.ucm.es1571-0661 © 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.07.021168M. 黑山等/理论计算机科学电子笔记246（2009）167显然，语言是不纯的细胞和区域破坏，如果不加限制地使用，是一个（非常危险的）副作用。但是如果我们只考虑那些被这种类型系统接受的程序，那么这种语言是纯的，副作用是自由的。在本文中，我们推导出一个命令式机器从一个高层次的大步操作语义，并给出了功能，翻译安全程序的命令式代码的机器。派生是通过跨小步操作语义和中间抽象机的增量精化来实现一旦机器的内存需求是已知的，我们丰富的语义与内存消耗注释，并证明翻译和抽象的机器是正确的丰富的语义。我们还实现了进一步的代码生成阶段，从这里介绍的最后Safe是Proof CarryingCode项目的一部分，其目的是将此字节码与正式证书一起生成。在我们的例子中，证书将证明代码的执行没有悬挂指针。在第2节中，我们简要介绍了语言。第3节和第4节描述了一个大步操作语义和一个等效的小步操作语义。第5节描述了一个称为SAFE-M2的抽象机器，其中使用了一个延续堆栈。第六节介绍了命令式机器SVM，第七节介绍了从安全到命令式代码的转换方案。给出了一个详细的例子，证明了有效的尾递归.在第8节中，我们提供了丰富的大步骤语义，并证明其资源注释反映了翻译后的程序所做的真实消费。最后，在第9节中，我们回顾了一些相关的工作，并得出结论。2安全总结Safe是一种一阶多态函数式语言，其语法类似于（一阶）Haskell或ML，并具有一些管理内存的功能。内存模型基于构建数据结构的堆区域。然而，在编写程序的全安全中，区域是隐式的。这些都是在完全安全的情况下被脱糖为核心安全的[8]。由于本文中提出的语义是在核心安全级别定义的，因此我们对其进行了详细描述区域的分配和释放与函数调用绑定：工作区域在进入调用时分配，在退出调用时释放。在函数内部，数据结构可能会被构建，但它们也可以通过使用破坏性模式匹配被破坏，表示为！或者一个案子表达式，该表达式释放与最外层构造函数对应的单元格。使用递归，整个数据结构的递归部分可以被释放。我们说它是被谴责的。作为一个例子，我们在Full-Safe中展示了一个append函数，它破坏了第一个列表concatD[]！YS= yconcatD（x：xs）！ YS= x： concatD xs ys因此，追加需要恒定的堆空间，而通常的版本M. 黑山等/理论计算机科学电子笔记246（2009）167169需要线性堆空间。第一个列表丢失的事实反映在函数的类型中：concatD：：[a]！->[a]->[a].不属于函数结果的数据结构作为一个例子，我们展示了树排序算法的破坏性版本treesortD：： [Int]！-> [Int]treesortD xs= inorder（mkTreeDxs）首先，使用原始列表xs通过应用函数mkTreeD（定义如下）来构建搜索树。然后遍历这棵树以产生排序列表。树不是函数结果的一部分，因此它将在工作区域中构建，并在treesortD函数返回时死亡（在Core-Safe中，区域是显式的，这将是显而易见的）。原始列表被销毁，并且在遍历中使用了破坏性追加函数，从而消耗了常量堆空间函数mkTreeD在二叉搜索树中插入列表的每个元素。mkTreeD：：[Int]！-> BSTreeInt mkTreeD []！ =空mkTreeD（x：xs）！=insertD x（mkTreeD xs）函数insertD是二叉搜索树中插入的破坏性版本。然后mkTreeD正好消耗列表在堆中占用的空间。在最坏的情况下，这个函数的非破坏性版本将消耗平方堆空间。insertD：： Int ->BSTree Int！-> BSTreeInt insertD x Empty！=节点空x空insertD x（节点lty rt）！| x == y =节点lt！yrt！| X > y=节点lt！y（insertDxrt）| X< y= Node（insertDxlt）y rt！请注意，在第一个守卫中，刚刚被摧毁的细胞必须重新建造。当一个数据结构被宣告无效时，它的递归子结构可能随后被销毁，或者它们可能作为函数结果的一部分被重用。我们用a！表示后者，如函数insertD所示。这是出于安全原因：一个被谴责的数据结构不能作为函数的结果返回，因为它可能包含悬挂指针。重用将一个被谴责的数据结构变成一个安全的数据结构。原来的参考资料已无法访问。因此，在这个例子中，lt和rt是不合格的，它们必须被重用，才能成为结果的一部分数据结构也可以被复制，表示为附加@到变量。只有结构的递归部分被复制，而元素与旧的共享。当我们需要基于破坏性函数的非破坏性版本时，这很有用。例如，我们可以定义treesort xs=treesortD（xs@）。在图1中，我们展示了Core-Safe的语法。 程序prog是一个序列，可能是递归的多态数据和函数定义，后跟使用它们的主表达式e，其值是程序结果。缩写xin代表x1···xn。破坏性模式匹配脱糖成案！表达式。构造式只允许在let绑定中使用，原子在函数应用程序中使用，case/case！判别、复制和重用。 区域是明确的，结构体应用程序和复制表达式。函数定义具有额外的区域参数rjl，其中可以构建数据结构。 在右手边170M. 黑山等/理论计算机科学电子笔记246（2009）167我Ij我ijkmksprog→datan;decm;edata→dataT αn@ρm=C不nk@ρl{recursive，polymorphic data type}dec→fxin@rjl=e{rrsive，polymorphicfunction}e→ a{atom：literal cor variablex}| x@r{copy}| x！{reuse}| fain@rjl{functionapplication}| 设x1=在e{非递归，单态}中| case x of altn{read-only case}| case! altn的x{destructivecase}alt→Cxin→ebe→Cain@r{构造函数应用程序}| eFig. 1. 核心安全语言定义可以仅使用Rj及其工作区域self的函数类型包括区域参数类型。多态代数数据类型通过数据声明来定义。在区域推断之后，Alge-XML类型声明具有额外的类型变量，指示该类型的构造值被分配的区域。区域推断还向构造函数添加区域参数，强制限制递归子结构必须与其父结构位于同一区域。例如，在区域推断之后，树表示如下：data BSTree a @rho = Empty@rho| Node（BSTree a@rho）a（BSTree a@rho）@ rho当使用嵌套类型时，可能有几个区域参数：数据结构的不同组件可能位于不同的区域。在这种情况下，最后一个区域变量是分配这种类型的构造值的最外面的区域。在下面的示例中数据T a b@rho1 rho 2 = C1（[a]@rho1）@rho2 |C2b@rho2rho2是分配类型T的构造值的位置，而rho1是分配C1值函数splitD是具有多个输出区域的函数的示例。为了节省空间，我们在这里展示了一个带有显式区域的半脱糖版本。注意，结果元组及其组件可能位于不同的区域：splitD：：Int-> [a]！@ rho2 -> rho1 -> rho2 -> rho3 ->（[a]@rho1，[a]@rho2）@rho3splitD 0 zs！@r1 r2 r3=（[]@r1，zs！）@ R3splitDn []！@r1 r2 r3 =（[]@r1，[]@r2）@r3splitD n（y：ys）！@r1r2 r3 =（（y：ys1）@r1，ys2）@r3其中（ys 1，ys 2）=splitD（n-1） ys@r1r2 r33大步语义学在图2中，我们展示了核心语言表达式的大步操作语义。我们用v，vi，。。来表示值，即堆指针或基本常数，并且p，pi，q，. 来表示堆指针。我们用a，ai，。。表示原子，即程序变量或基本常数。前者用x，xi，.表示。最后，我们使用r，ri，. 来表示区域变量。形式为E h，k，ehJ，kJ，v的判断意味着表达式e是-M. 黑山等/理论计算机科学电子笔记246（2009）167171我Eh，k， c h，k，c[Lit]E[x<$→v]h，k，x h，k，v [变量1]j≤k（hJ，pJ）=copy（h，p，j）E[x<$→p，r<$→j]h，k，x@rhJ，k，pJ[变量2]新鲜（q）[变量3]E[x<$→p]h[p<$→w]，k，x！h[q<$→w]，k，q（f xn@rm=e）∈nJmJJij[xi→E（ai），rj→E（rj） ，self <$→k+1]h，k+1， eh， k+1， vnJmJ J[应用程序]Eh，k，fai@rj拉克什|kJ， k， vEh，k，e1hJ，kJ，v1E[x1<$→v1]hJ，kJ，e2hJJ，kJJ，v[Let1]设x1=e1在e2中，HJJ，KJJ，vj≤kfresh（p）E<$[x1<$$> →p]<$ h [p<$→（j，C vin）]，k，e2<$hJ，kJ，vE[r<$→j，a<$→vn]∈h，k，设x=Can@rine∈hJ，kJ，v[设2]我我1 我2C=CrE[xri<$→vinr]h，k，erhJ，kJ，vE[x<$→p]<$h[p<$→（j，C vnr）]，k，Cxni的情况x→em<$hJ，kJ，v[情况]我我伊日C=CrE[xri<$→vinr]h，k，erhJ，kJ，vE[x <$→ p] h[p <$→（j，C vinr）]，k，case！x=Cixijni→emhJ，kJ，v[Case！]图二. 安全表达式的操作语义在运行时环境E和堆h下，可简化为规范形式v，堆h具有k+ 1个区域，范围从0到k，并且产生具有kJ+ 1个区域的最终堆hJ将程序变量映射到值和区域变量到实际区域标识符。我们采用这样的约定：对于所有的E，如果c是常数，则E（c）=c。堆h是一个从新变量p（我们称之为堆指针）到构造单元w（形式为（j，Cvin））的有限映射，这意味着单元驻留在区域j中。我们称区域（w）=j。实际的区域标识符j是自然数。出现在函数体中的形式区域要么是对应于形式参数的区域变量r，要么是常量self。背离他人作者，通过h[p<$→w]，我们表示堆h，其中绑定[p<$→w]被突出显示。相反，我们用h[p<$→w]表示堆h与绑定[p<$→w]的不交并。由h|k我们表示通过从h中删除那些存在于大于k的区域中的绑定而获得的堆，并且由dom（h）表示集合{p |[p<$→ w] ∈ h}。程序的语义是环境声明中主表达式的语义，它是包含所有函数和数据声明的集合规则Lit和Var1只是说基本值和堆指针是范式。 规则变量2执行复制表达式，将p指向的数据结构复制到（可能不同的）区域j中。运行时系统函数副本跟随结构递归位置中的指针从p开始并在区域j中创建所有递归单元的副本。我们的运行时系统中提供了一些受限类型信息，以便可以实现此函数。非递归位置的指针在新单元格中保持相同。这意味着两种数据结构可以共享某些子部分。172M. 黑山等/理论计算机科学电子笔记246（2009）167在规则Var3中，堆中的绑定[p<$→w]被删除，并添加到单元格w的新绑定[q<$→w此操作可能会在活堆中创建悬空指针，因为某些单元格可能包含p的自由出现。规则应用程序显示何时分配新区域。注意，函数体是在一个有k+2个区域的堆中执行的。形式标识符self绑定到新创建的区域k+ 1，以便函数体可以在该区域中创建DS或将该区域作为参数传递给其他函数调用。在从函数返回之前，删除在区域kJ+1中创建的所有单元格此操作是另一个可能的悬空指针的来源。规则Let1，Let2和Case是用于一种渴望语言的常见规则，而规则Case！表示破坏性模式匹配中发生的情况：判别变量的绑定从堆中消失。此操作是可能的悬挂指针的最后一个来源。在下文中，我们可以随意地将可导出的判断写为Eh，k，ehJ，k，v，因为：命题3.1如果Eh，k，ehJ，kJ，v是可导的，则k = kJ。证据 直截了当，通过归纳就推导出了深度。Q命题3.2如果e0是安全程序的主表达式，并且[self›→0]{}，0，e0hf，0，vf是可导的，则在每个判断中，E（self）= k的导数E h，k，ehJ，k，v成立。证据这个性质在初始判断时为真，并且在每一个归纳规则中都保持不变。 唯一相关的情况是规则App。Q4小步语义在图3中，我们展示了小步语义规则。有两种判断。第一类，E，h，k0，k，e−→hJ，k0，v，当表达式e在一步中被求值为一个值时应用。这些对应于文字、变量、复制表达式和重用表达式。另一类，E，h，k0，k，e −→ EJ，hJ，k0，kJ，eJ，涵盖了其余的情况：函数应用，let，case和case！ 表情在配置中，k表示h中可用的最高区域，就像在大步语义中一样。下面我们解释一下k0的含义。注意，let表达式用自然数δ和环境E标记。在规则App中，可用区域的数量增加1，因为新的本地区域被分配并被分配编号k+ 1。此外，环境E被丢弃，因为在函数体中只有参数和self区域在作用域中然而，由于let表达式，在函数应用之后可以继续然后，我们需要恢复丢弃的环境和原始的k值。环境保持在绑定中，数字δ用于在计算绑定表达式时记住新创建的区域，以便以后可以恢复原始的kδ和E的初始值为分别为0和0，我们可以假设在文本中注释了规则Let4bM. 黑山等/理论计算机科学电子笔记246（2009）167173011k≥k0[Lit]E，h，k0，k，c −→ h |k0，k0，ck≥k0[Var]E[x <$→ v]，h，k0，k，x −→ h |k，k0，v1k≥k0k≥j（hJ，q）=copy（h，p，j）E[x<$→p，r<$→j]，h，k，k，x@r−→hJ，k，q[变量2]0 0k≥k0新鲜（q）[变量]E[x→p]，h[p→w]，k0，k，x！−→h[q<$→w]，k0，q 3（f xin@rjm=e）∈E，h，k，k，fan@rJmnJm[应用程序]0ij−→[xi→E（ai），rj→E（rj）j≤k新鲜（p），self<$→k+ 1]，h，k0，k+1，eE[r<$→j，a<$→vn]，h，k，k，令x[Let3]=<$C an@rine−→E<$[x<$$> →p]，h[p<$→（j，C vn）]，k，k，e我我010i1i0E，h，k，k，e1−→hJ，k，v1E，h，k，k，令x=e，在e−→E[x›→v]，hJ，k，k，e[设4a]0 1011 1 0E，h，k，k，e1−→EJ，hJ，k，k+η，eJ[让4b]E，h，k0，k，令x1=Ee1ine−→EJ，hJ，k0，k+η，令x1=EeJine0η1EJJ<$E，h，k，k+δ，e1−→hJ，k，v1E，h，k，k+δ，设x=EJJe在e−→EJJ<$[x›→v]，hJ，k，k，e[设4c]0 1δ11 1 0EJJ/=E，h，k，k+δ，e1−→EJ，hJ，k，k+η，eJ[Let4d]E，h，k，k+δ，设x=EJJe在e−→EJ，hJ，k，k+η中，设x=EJJeJine0 1δ1 0 1η1C=Cr[Case]E[x<$→p]，h[p<$→（j，C bnr）]，k，k，Cxni→em−→En[x<$→vnr]，h，k，k，e的情况xi0i i j i ri i0rC=Cr[Case！]E<$[x <$→ v nr]，h <$[p <$→（j，C bnr）]，k，k，case！ x of C x ni → em −→ E <$[x <$→ v nr] h，k，k，e里伊i0i伊日ri i0r图三. 安全表达式的小步操作语义第一次保存环境，并且规则Let4d在计算绑定表达式期间根据需要更新信息。 在绑定表达式的求值成功的情况下，规则Let3、Let4a或Let4c将被应用以继续主表达式的求值。在计算绑定表达式期间创建的那些新区域不能包含计算结果，因为在函数应用之后，局部区域被释放。区域k0表示当机器停止减少表达式时可用的最高区域。初始k=k0= 0。规则App递增k，而规则Lit、Var1、Var2和Var3丢弃所有局部区域回到k0。这种小步语义等价于先前定义的大步语义：对于任何k和k0≤k，Δ，k，e<$Θ，k，v当且仅当Δ，k0，k，e−→<$ Θ，k0，k，v。5抽象机SAFE-M2我们的下一个改进是引入一个抽象机器，称为SAFE-M2，因为之前有一个名为SAFE-M1的机器现在被放弃了。机器的配置是一个7元组（h，k0，k，e，E，S，N），其中h是堆，k0，k是在小步语义中使用的区域编号，e是控制表达式，E是运行时环境，S是堆栈，N是给出每个定义的安全函数的代码的函数。在图4中，我们174M. 黑山等/理论计算机科学电子笔记246（2009）167展示了抽象机器M. 黑山等/理论计算机科学电子笔记246（2009）167175Jn初始/最终配置条件标签（h，k0，K，c，E，S，S）（h |k0，k0，k0，c，E，S，n）k > k0[Lit1]（h，K，K，C1，E1，（k0，x1，e，E）：S，n）n（h，k0，K，e、E[x1<$→ c1]，S，S）[Lit2]n（h[p<$→（j，Cbi）]，k0，k，x，E[x<$→p]，S，S）k > k0[缺点1]（h|k0，k0，k0，x，E，S，S）n（h[p<$→（j，Cbi）]，k，k，x，E1[x<$→p]，（k0，x1，e，E）：S，n）[Cons2]n（h，k0，K，e、E [x1<$→p]，S，S）n（h[p<$→（l，Cbi）]，k0，k，x@r，E[x<$→p，r<$→j]，S，n）（h，q）=copy（h，p，j）[Copy]n（hJ，k0，K，y，E<$[y <$→q]，S，n）j≤k，fresh（y）（h[p›→w]，k0，K，x！、E [x <$→p]，S，n）新鲜（q），新鲜（y）[重复使用]n（h[q<$→w]，k0，k，y，En[y<$→q]，S， n）（h，k0，k，fain@sjm，E，S，n）（fxin@rjm=e）∈n[App]n mn（h，k0，k+1，e，[xi→E（ai），rj→E（sj），self→k+1]，S，n）（h，k0，K，设x1= Cain @ sine，E，S，n）E（s）≤ k[设3]n（h[p›→（E（s），C E（ai））]，k0，K，e、E[x1<$→p]，S， n）新鲜（p）（h，k0，K，设x1= e1，E，S，E）[Let 4]n（h，K，K，E1，E，（k0，x1，e，E）：S，n）（h[p<$→（j，Cbi）]，k0，k，casexofCixijnin→ei，E[x<$→p]，S， n）C=Cr [情况1]（h，k0，k，er，E→bjn]、S，S）ni（h[p <$→（j，Cbi）]，k0，k，case！xofCixijnn（h，k0，k，er，En[xrj<$→bj]，S，n）→ei，E[x<$→p]，S， n）C=Cr[情况2]见图4。抽象机SAFE-M2安全M2。唯一的新元素w.r.t.小步长语义是栈S。它由形式为（k0，x1，e，E）的连续框架组成，对应于一个字母的待定表达式e，其辅助表达式e1正在评估中。 区域k0是应该返回e的范式的地方，x1是e中的let绑定变量free，E是应该在其中计算e对应于Let4组的归纳语义规则，抽象机器规则Let4将延续推到堆栈，并继续进行辅助表达式e1的求值。当在规则Lit1和Cons1中达到e1的标准形式时，继续被弹出并且机器继续主表达式的求值。我们用a，ai，。。表示程序变量或基本常量。请注意，当达到正常形式时，当前环境在规则Lit2和Cons2中被丢弃，并且必须从堆栈中弹出延续。此外，当输入函数体并且形式参数成为作用域中唯一的变量时，它在规则App中被丢弃。在第7节中，这将产生一个重要的结果，即尾递归被转换为只需要一个常量堆栈空间还请注意，在规则Let4中，当前环境保存在堆栈中，但176M. 黑山等/理论计算机科学电子笔记246（2009）167R不从对照中丢弃。第7节中给出的翻译的一个重要方面是，它设法避免了这种隐含的环境复制当前的环境在规则Let3、Case1和Case2中扩展了新的绑定，只要let绑定或case绑定的变量在continuation表达式的作用域中成为自由变量。 此外，它在规则复制和重用中扩展了一个新的程序变量y。这仅仅是一个伪像，因为在控制表达式中必须引用新的数据结构。最后，在规则Lit2和Cons2中，continuation中保存的环境E必须用let引入的新绑定进行扩展。6命令式抽象机SVM我们首先介绍我们的命令式机器，然后，在SEC。机器SVM（安全虚拟机）的配置由六个组件（is，h，k0，k，S，cs）组成，其中is是当前指令序列，cs是代码存储器，其中保存从程序片段编译产生的指令序列。现在，我们将使用p，q，... 来表示由cs求解的代码指针，并且b，bi，. 表示堆指针或存储在堆栈中的任何其他项（常量，区域编号或延续）。在图5中，我们显示SVM指令在配置转换方面的语义。通过Cm，我们表示数据构造器，它是其数据定义中的第r总共有m个数据构造器。通过S！j我们表示堆栈S的从顶部开始计数并从0开始的第j个元素（即S！0是top元素）。指令DECREGION从堆中删除当前区域k和区域k0之间的所有区域（如果有的话），不包括后者。它将在达到正常形式时使用。指令POPCONT从堆栈中弹出一个continuation，如果没有continuation，则停止执行。请注意，b（通常是一个值）被留在堆栈中，以便可以通过continuation访问它。指令PUSHCONT推送延续。它将被用于一封信的翻译。指令COPY和REUSE只是模仿抽象机M2的相应动作Copy和Reuse。指令CALL跳转到新的指令序列并创建新的区域。指令PRIMOP操作位于堆栈中的两个基本值，并将它们替换为操作的结果指令MATCH根据匹配闭包的构造函数执行向量跳转。由pj指向的序列的向量对应于一组情况替代的汇编。指令匹配！另外破坏匹配的细胞。指令BUILDENV接收键Ki的列表，并在堆栈顶部创建一部分增强：如果键K是自然数j，则项S！j被复制并推送到堆栈上;如果是基本常数c，则直接推送到堆栈上;如果是标识符自身，则将当前区域编号k推送到堆栈上。指令BUILDCLS分配新的内存并构造堆值。作为BUILDENV，它接收一个键列表并使用相同的约定。它M. 黑山等/理论计算机科学电子笔记246（2009）167177我0RR初始/最终配置条件（DECREGION：是，h、k0，k，S，cs）k≥ k0（是，H|k0，k0，k0，S，cs）（[POPCONT]，h，k，k，b：（k0，p）：S，cs[p<$→is]）（是，h、k0，K，b：S，cs）（PUSHCONTp：is，h、k0，K，S，cs [p <$→ isJ]）（是，h、K，K，（k0，p）：S，cs）（COPY：is，h[b> →（l，C vin）]，k0，k，b：j：S，cs）（hJ，bJ）=copy（h，b，j）（是，hJ，k0，k，bJ：S，cs）j≤ k（REUSE：is，h[b<$→w]，k0，k，b：S，cs）fresh（bJ）（是，h[bJ<$→w]，k0，K，bJ：S，cs）（[CALLp]，h、k0，K，S，cs[p›→is]）（是，h、k0，k + 1，S，cs）（PRIMOP：是，h、k0，k，c1：c2：S，cs）c = c1<$c2（是，h、k0，K，c：S，cs）（[MATCHlpjm]，h[S！l<$→（j，Cmvin）]， k，k，S，cs[pj<$→isjm]）n（is r，h，k0，k，bir10的：S，cs）（[MATCH！ lpjm]，h[S！l<$→（j，Cmvin）]，k0，k，S，cs[pj<$→isjm]）n（is r，h，k0，k，biR：S，cs）（BUILDENVKn：is，h、K，K，S，cs）n（是，h、k0，K，第k项（Ki） ：S，cs）（1）（BUILDCLSCmKnK：是，h、K，k，S，cs）项目（K）≤k，新鲜（b）ri0kn（是，H[b<$→（k项（K），Cmk项（Ki）） ）]，k0，K，b：S，cs）（1）（幻灯片m n：是，h、K，K，bm：bJn：S，cs）M（is，h，k0，k，bi⎧0ii：S，cs）（1）Itemk（K）d=ef快！J若K=j∈ N⎨如果K=c⎪如果K=self，则为图五. 抽象机SVM还接收值的构造函数Cm。最后，指令SLIDE删除堆栈的某些部分。它将用于删除不再需要的环境7翻译成命令式代码这种转换的主要新思想是将M2机器的运行时环境分为两个环境：一个是将程序变量映射到自然数的编译时环境ρ，另一个是将堆栈顶部的操作集映射到实际堆指针、基本常量或区域号的实际运行时环境。⎪⎪178M. 黑山等/理论计算机科学电子笔记246（2009）167ρ环境将变量映射到其运行时值所在的堆栈中的位置。随着堆栈的动态增长，第一个想法是从环境的底部到顶部为变量这样如果环境占据堆栈的顶部m个位置，ρ[x<$→1]，则S！（m−1）将包含对应于x的运行时值。第二个想法是在将continuation推入堆栈时重用当前环境。在M2规则Let4中，压入堆栈的环境E与评估辅助表达式e1这样做的目的是共享环境而不是复制环境，并且只推送continuation中剩余的参数，即对（k0，e）（实际上不需要变量x1因此，整个环境ρ将由一系列较小的环境[δ1，. ，δn]，除了第一个δ1，每个都有一个延续。每个单独的块i由一个三元组（δi，li，ni）组成，实际环境δi将变量映射到范围（1.mi），其长度li= mi+ ni，以及指示符ni，其值对于除了第一个块之外的所有块都是2，第一个块的值是ni= 0。我们假设一个continuation在堆栈中需要两个单词，而其余的项目需要一个单词。函数中定义的变量x的栈顶的操作集德国国防军块k，记为ρ x，计算如下：ρ x=i=1li-δkx。只有顶层环境可以使用新绑定进行扩展。在编译时环境中有三种操作：(i)（（δ，m，0）：ρ）+{xi <$→jindef}=（δi{xi→m+jin，m+ n，0）：ρ.（ii）（（δ，m，0）：ρ）++d=ef（{}，0，0）：（δ，m +2，2）：ρ.（iii）topDepth（（δ，m，0）：ρ）d=efm. 你知道我的意思。第一个使用n个新绑定扩展顶层环境，而第二个使用2-indicator关闭顶层环境，然后打开一个新环境。使用这些约定，在图6中，我们展示了转换函数trE，它采用核心安全表达式并给出SVM指令列表和代码存储。其中，NormalFormρ是一个编译宏，定义如下：def=SLIDE 1（topDepth ρ）;DECREGION;POPCONT请注意，在函数应用程序中，主体的转换应该在代码存储中找到。这通过突出显示地址p来表示。7.1高效尾递归：一个例子我们在这里展示一个详细的例子，factorial函数的尾部递归版本：ifact n r= case nof0 →r→令rJ=rnin（令nJ=n−1 inifactnJrJ）;ifact3 1标准形式ρM. 黑山等/理论计算机科学电子笔记246（2009）167179nntrEc ρ=BUILDENV[c];标准形式ρtrEx ρ= int n[n];标准形式ρtrE（x@r）ρ=int n[n，n];副本;标准形式ρtrE（x！）ρ=int n[n];重复使用;标准形式ρtrE（a1<$a2）ρ=buildDENV[ρ a1，ρ a2];PRIMOP;标准形式ρtrE（fain@sjm）ρ= BUILDENV[ρain，ρsjm];SLIDE（n+m）（topDepth ρ）;CALLp其中（f xin@rjm=e）∈cs[p<$→trEe [（{rj <$→m−j+ 1m，xi<$→n−i+m+1n}，n+m，0）]]trE（letx=Cman@sine）ρ=BUILD CLSCmn1liL[（pi）]（p s）;trEe（ρ+{x1<$→1}）trE（letx1=e1ine）ρ=PUSHCONTp;cs<$[p<$→trEe（ρ+{x1<$→1}）]trEe1ρ++n ntrE（alt i的情况x）ρ=MATCH（ρ x）pics[pi<$→trA altiρ]n ntrE（case！ 所有i）ρ的x= 火柴！（ρ x）pi&cs[pi<$→trA altiρ]trA（C xin→e）ρ=trEe（ρ+{xi<$→n−i+ 1n}）见图6。 从标准化Safe到SVM指令的在图7中，我们展示了相应的命令式代码和执行ifact3 1的概要。 我们从上到下，从左到右显示了执行某些指令（写在堆栈上方）后堆栈通过SLIDE2 4指令可以直观地看到尾递归是如何有效地完成的，该指令丢弃了以前的（已经死亡的）环境。堆栈8资源感知语义一旦SVM的资源消耗是已知的，我们丰富的语义节。3，其中资源向量（δ，m，s）作为评估表达式e的边向量而获得。第一个分量是一个偏函数δ：N→Z，它给出了每个区域k的最终堆和初始堆中单元之间的有符号差。正差异意味着在该区域中已经产生了新的细胞。一负一，意味着一些细胞已经被破坏。 我们用dom（δ）表示其中，N是定义为δ的子集。 通过|δ|我们的意思是，n∈ dom（δ）δ（n）给定细胞的总平衡剩余的分量m和s分别给出堆中新单元的最小数量和栈中成功评估e所需的字的最小数量。当e是主表达式时，这些数字给出了安全程序的总内存需求在图8中，我们展示了丰富的规则。请注意，模拟compile的topDepth函数所需的附加参数td180M. 黑山等/理论计算机科学电子笔记246（2009）16713nRnRP5+ 1P5+ 1P5+ 1nBUILDENV[ Lit3，Lit1]P3载玻片2 0n呼叫ifact0n1n2ifact： MATCH0 [ P，P]r0rJrJrJ341 2P3：BUILDENV[Var1]幻灯片1和2DECREGIONPOPCONTP4：PUSHCONTP5BUILDENV[Var2，Var1]PRIMOP*n0的P4+ 1r0RP6nNJn1n2r1r2P3RP6P6n3jjr31 2滑动 1 0POPCONTP5：PUSHCONTP6BUILDENV[Var2，Lit1]PRIMOP-滑动 1 0POPCONTn0rJr0nJRJP4+ 4n0r10的RJJ J1 2J J1 2J J1 2n1n2r1r2P3+ 2RP6：BUILDENV[变量0，变量1]n00P6+ 2P6+ 2P6+ 2见图7。 ifact31的命令代码和执行时间环境。我们用[ ]表示函数λn。δ1+δ2的函数为：8>δ1（x） +δ2（x）ifx∈dom（δ1）dom（δ2）（δ1+δ2）（x）=>：δi（x）ifx∈dom（δi）−dom（δ3−i），i∈{1，2}否则，规则Var2中的函数大小给出了数据结构的递归脊柱的大小：Xsize（h[p<$→（j，C vin）]，p）=1+i∈RecPos（C）尺寸（h，vi）其中RecPos返回给定构造函数的递归参数位置。在规则App中，通过δ|k表示一个类似δ的函数，但对于大于K. 新堆栈字的计算max{n +l，s+n+l-td}考虑到考虑到需要前n+l个字来存储实际的参数，则丢弃长度为td的当前环境，然后计算函数体。在规则Let1中，一个continuation（2个单词）在计算e1之前被堆叠，这个a在计算e2之前在堆栈中留下一个值。因此，计算max{ 2+s1， 1+s2}。现在，我们证明，对抽象机器是健全的，完全尊重这个语义。首先，我们注意到语义和SVM机器规则都是语法驱动的，并且它们的计算是确定性的（直到新名称生成）。定义8.1我们说环境E和对（ρ，S）是等价的，记为E<$（ρ，S），如果domE−{self}= dom ρ，且<$x∈domρ。E（x）= S！（ρ x）。6nRnR311名P6331212个P6623113个P6616606131名P531232331161623060616331滑动2 4R呼叫ifactn12n21n30R13R26R36M. 黑山等/理论计算机科学电子笔记246（2009）167181JSSSSSEh，k，td，c h，k，c，（[]， 0， 1）[Lit]E[x<$→v]h，k，td，x h，k，v，（[]， 0， 1）[Var]j≤k（hJ，pJ）=copy（h，p，j）m=size（h，p）E[x<$→p，r<$→j]h，k，td，x@rhJ，k，pJ，（[j<$→m]，m， 2）[变量2]新鲜（q）E[x <$→ p] h[p <$→ w]，k，td，x！ h [q <$→ w]，k，q，（[]，0，1）[Var3]（fxn@rl=e） ∈nJlJi j[xi<$→E（ai），rj<$→E（rj），self<$→k+ 1]<$h，k+ 1，n +1，e<$h，k+ 1，v，（δ，m，s）L[应用程序]Eh，k，td，f ain@ rJhJ|k，k，v，（δ|k，m，max {n + l，s + n + l-td}）Eh，k，0，e1hJ，k，v1，（δ1，m1，s1）E<$[x1<$→v1]<$HJ，k，td+1，e2<$HJJ，k，v，（δ2，m2，s2）Eh，k，td，令x=e在大肠δhJJ，k，v，（δ[Let1]+ δ，max {m，|δ |+ m}，最大值{2+ s，1+ s}）1121211212j≤kfresh（p）E<$[x1<$$> →p]<$ h [p<$→（j，C vin）]，k，td+1，