179--理论计算机科学电子笔记70第4期（2002）网址：http://www.elsevier.nl/locate/entcs/volume70.html22页优化代码的翻译和运行时验证1，2Lenore Zuck3 Amir Pnueli4 Yi Fang3 Benjamin Goldberg3胡英3摘要本文提出了优化编译器的验证方法。该公司是积极的和针对体系结构的优化，试图从现代体系结构，特别是EPIC类微处理器获得最高的性能。翻译验证的方法不是验证编译器，而是在每次运行编译器后执行验证检查，产生一个正式的证明，证明所产生的目标代码是源代码的正确实现首先，我们调查的标准方法来验证的优化，保持循环结构的代码（虽然他们可能会移动代码进出循环，并从根本上修改个别语句），提出了一个基于模拟的通用技术验证这种优化，并描述了一个工具，VOC-64，实现这些技术。 对于更积极的优化，通常会改变代码的循环结构，例如循环分布和融合，循环平铺和循环交换，我们提出了一组置换规则，这些规则确定转换后的代码满足所考虑的转换有效性所需的所有隐含数据依赖性。我们描述了必要的扩展VOC-64，以验证这些结构修改优化。最后，本文讨论了投机循环优化的运行时验证的初步工作，其中包括使用运行时测试，以确保正确的循环优化，无论是编译器还是编译器验证技术可以保证的正确性。与编译器验证不同，运行时验证不仅有确定优化何时生成错误代码的任务，而且还有从优化中恢复而不中止程序或产生错误结果的任务。这种技术已被应用于几个循环优化，包括循环交换，循环平铺，和软件流水线，似乎是相当有前途的。1本研究部分由NSF资助CCR-0098299，ONR资助N 00014 -99-1-0131，以及John von Neumann Minerva Center for Verification of Reactive Systems。2 电邮地址：zuck，amir，yifang，goldberg @ cs.nyu.edu3纽约大学4魏茨曼科学2002年由ElsevierScienceB出版。 诉 操作访问根据C CB Y-NC-N D许可证进行。ZUCK等人1801介绍在工业界和学术界，人们越来越意识到正式证明系统安全关键部分的正确性的关键作用大多数验证方法都关注于对需求的规范进行验证，以及对规范进行高级代码验证然而，如果要证明高级规范在低级代码中正确实现，则需要验证执行transla-tions的编译器。由于目标架构的复杂性和可重构性，以及编译器中使用的复杂分析和优化算法，现代优化编译器的正确性具有挑战性。由于编译器的大小、随时间的演变以及可能的专有考虑，正式验证一个全边缘优化编译器是不可行的，就像验证任何其他大型程序一样翻译验证是一种新的方法，它为一般的翻译人员，特别是编译人员的使用翻译验证方法，而不是验证编译器本身，构建一个验证工具，在编译器每次运行后，正式确认生成的目标代码是源程序的正确翻译新系列微处理器架构的引入，例如以英特尔IA-64架构为代表的EPIC系列，使编译器的优化责任更加繁重。需要静态编译时依赖性分析和指令调度来利用指令级并行性，以便与其他体系结构竞争，例如超标量类机器，其中硬件在运行时确定因此，一个新的家庭的sophisticated优化已被开发，并纳入编译器针对EPIC架构。之前的工作（[PSS98a]）开发了一个翻译验证工具CVT，它成功地在大约10分钟内自动验证了大约10，000行源代码的CVT的成功关键取决于一些限制源和目标的简化假设对于具有单个外部循环的程序，并假设一组非常有限的优化。其他方法[Nec00，RM00]考虑了限制较少的语言的翻译验证，例如允许嵌套循环。他们还考虑了一系列更广泛的优化。然而，那里提出的方法仅限于结构保持优化，并且不能直接处理更积极的优化，例如循环分布和循环平铺，这些通常用于更高级的优化编译器中。我们的最终目标是为高级优化编译器的翻译验证开发一种方法，重点是EPIC目标编译器和此类编译器的积极优化特性ZUCK等人181我们的方法将处理一组广泛的优化，并可用于实现各种编译器的全自动认证，确保编译器在安全关键系统和编译成硅等领域具有极高的置信度，其中正确性是最重要的问题。[ZPFG02]描述了实现这一目标的初步步骤。在此基础上，我们提出了正确翻译的理论。我们区分结构保持优化，承认一个明确的映射在目标程序中的控制点在源程序中的相应控制点，结构修改优化，不承认这样的映射。针对结构保持优化，提出了结构保持转换的翻译验证的一般证明规则，并给出了在EPIC编译器（SGIPro-64）上实现该证明规则的一个工具（EST工作总结见第2节。一类更具挑战性的优化不能保证目标和源中的控制点之间的这种对应性这些优化的一个重要子类，也是本文其余部分的重点，是重新排序转换，它只改变语句的执行顺序，而不改变、删除和添加它们。属于这类的典型优化是循环分布和融合、循环平铺和循环交换。为了验证这些重新排序转换，我们在第3节中探索置换规则要求计算哪些是重新排序的语句，然后证明重新排序保留了可观察的语义。在某些情况下，不可能在编译期间确定所需的优化是否合法。这通常是因为有效检查语法不同的索引表达式是否引用同一数组位置的能力有限。对于这种情况，一种可能的补救方法是采用积极的优化，这种优化永远不会执行循环转换，但在运行时保持检查，以确保没有危险的别名发生。如果运行时检查检测到危及优化有效性的别名，则代码逃逸到原始循环的未优化版本，在那里它以较慢但保证正确的方式完成计算这种方法建立在置换条件理论的基础上，在第4节中介绍。因此，这里报告的工作涉及首先，“翻译验证”方法可以被视为优化编译器的运行时验证，因为在每次运行编译器时，我们都会然后，推测性优化方法对目标代码应用运行时监控和验证-不断检查所应用的转换的有效性，并在有效性受到损害时ZUCK等人1821.1相关工作本文的工作是[ZPFG02]中工作的推广[Nec00]中的工作首先，它将源程序从单循环程序扩展到具有任意嵌套循环结构的程序。另一个重要的特征是，该方法根本不需要编译器插装，并且应用各种算法来恢复和识别所执行的优化以及相关联的细化映射。[Nec00]中明显的主要限制是，正如报告中描述的单一证明方法所暗示的那样，它只能应用于结构保持优化。相比之下，我们的工作也可以应用于结构修改优化，如与积极的循环优化，这是现代架构的优化的主要组成部分。另一个相关的工作是[RM00]，它提出了一种类似的翻译验证方法，其中一个重要的贡献是能够处理源程序中的指针然而，那里提出的方法假设编译器的完整插装，这在这里或[Nec00]中没有假设更弱相关的是[Nec97]和[NL 98]中报道的作品，它们并不旨在建立翻译的完全正确性，而只是对某些“安全”属性感兴趣然而，那里描述的程序分析技术与精化映射和辅助不变量的自动生成非常相关2优化翻译器的翻译验证我们概述了验证优化算法的一般策略，并描述了结构保持优化的验证理论。更详细的描述见[ZPFG02]。最后，我们以SGI PRO-64编译器的全局优化工具来编译器接收用某种高级语言编写的源程序，将其翻译成中间表示（IR），然后对程序应用一系列优化-从经典的体系结构无关的全局优化开始，然后是体系结构相关的优化，通常，这些优化在几个通道中执行（在某些编译器中多达15个），其中每个通道应用某种类型的优化。为了证明目标代码是源代码的翻译，我们首先使用转换系统（TS）的形式主义给源语言和目标语言提供公共语义 目标代码T的概念是一个源代码S的正确实现，然后定义在细化方面它指出，T的每一次计算都对应于某个计算。ZUCK等人183∈不⟨ O⟩⟨ O ⟩ ⟨ O⟩S与相应变量的匹配值中间代码是一个三地址代码。它由一个三地址代码的图形表示法--图来图中的每个节点表示一个基本块，即完整执行且不包含分支的语句序列。图的边缘代表控制流程。2.1变迁系统为了呈现源代码和中间代码的形式语义，我们引入了转换系统，TS转换系统S=Vi， Θ，ρ是一个状态机，其中：• V是一组状态变量，• 一组可观测变量，• Θ是表征系统的初始状态的初始条件，以及• ρ是一种过渡关系，将一个状态与其可能的后继者联系起来。变量是类型化的，并且TS的状态是变量的类型一致的对于状态s和变量x V，我们用s[x]表示s赋予x的值。转移关系既指未启动的也指启动的变量的初始化版本，其中初始化版本指的是后继状态中变量的值，而变量的未初始化版本指的是它们在过渡前状态中的值因此，例如，过渡关系可以包括状态比它在旧（转换前）状态下的值大1可观察变量是我们关心的变量。当比较两个系统时，我们将要求两个系统中的可观测变量我们要求所有由程序打印其值的变量都被识别为可观察变量。如果需要的话，我们还可以在可观测量中包括TS的计算是状态的最大有限或无限序列σ：s0，s1，.，从满足初始条件的状态开始，使得每两个连续的状态通过转移关系相关联。如果初始条件的可观测部分唯一地决定了计算的其余部分，则过渡系统被称为确定性的我们限制我们的注意力，确定性的过渡系统和程序，生成这样的系统。因此，为了简化演示，我们在这里不考虑其行为可能取决于程序在整个计算过程中读取这是直接的理论和方法扩展到这样的中间输入驱动的程序。令PS= VS，S，ΘS，ρS P T = VT，T，ΘT，ρT 是两个TS，我们分别将其称为源TS和目标TS。这两个系统被称为ZUCK等人184∈ O可比较的，如果存在一个一对一的对应关系之间的观测PS和那些的PT。为了简化符号，我们用X∈ OS和xT表示两个系统中相应的观测量。源状态s被定义为与目标状态t兼容，如果s和t在它们的可观测部分上一致也就是说，对于每个x∈ OT，s[X] =t[x]。我们说PT是P S的一个正确的翻译（精化），如果它们是可比较的，并且对于每个σT：t0，t1，. PT和每个σS：s0，s1，.的计算。PS的计算使得s0与t0相容，则σT是终止的（有限的）i <$σS是，在终止的情况下，它们的最终状态是相容的。2.2结构保持变换设PS=PS，OS，θS，ρS，和PT=PT，OT，θT，ρT，是可比较的TSs，其中PS是源，PT是目标。 为了证明PT是PS的正确翻译，在PT的结构与PS的结构没有根本区别的情况下，我们引入了一个证明规则，V ALIDATE，它受到了计算归纳法的启发（[Flo 67]），最初在-为了证明单个程序的属性，RuleVALIDATE提供了一种证明方法，可以证明一个程序可以改进另一个程序。这是通过建立从目标到源位置的控制映射，从源到目标变量的数据抽象映射，并证明这些抽象是沿着目标程序的基本执行路径维护的证明规则如图所示1.一、其中，假设每个TS具有割点集CP。这是一组块，包括初始块和终止块，以及程序控制流程图简单路径是连接两个割点的路径，不包含其他割点作为中间节点。我们假设每两个割点之间最多有一条简单路径对于每个从Bi到Bj的简单路径，ρij描述了块Bi和Bj之间的过渡关系。通常，这样的转移关系包含了使该路径能够被遍历的条件，以及该路径所引起的数据变换。注意，当从Bi到Bj的路径经过不在割点集中的块时，ρij是压缩的转移关系，可以通过从Bi到Bj的路径上的中间转移关系的合成来计算。部分（2）中的不变量B1是每当执行访问块Bi时预期保持的程序注释。它们通常可以从优化编译器执行的数据流分析中直观地说，它们的作用是在基本块之间传递信息验证条件断言，在从Bi到Bj的每个（目标）转换处，如果在转换之前断言Bji和数据抽象保持并且转换发生，则在转换之后存在新的源[5]回想一下，我们假设跃迁所描述的路径是简单的。ZUCK等人185→∈∈ O不π(i) 建立控制抽象κ：CPTCPS，将目标的初始和终端块映射到源头(ii) 对于CPT中的每个基本块Bi，形成可以仅引用具体（目标）变量的不变的Bui(iii) 建立数据抽象α：（p1→V1=e1）···（pn→Vn=en）将目标状态变量上的表达式e i赋给某些非控制源状态变量ViVS，条件是（tar-get）布尔表达式pi。请注意，α可以为同一个变量包含多个子句。 要求对于每个可观测源变量VS（其目标对应物是v）和每个终端目标块B，α意味着在B处V=v。(iv) 对于每对基本块Bi和Bj，使得存在简单的P的控制图中从Bi到Bj的路，设Paths（κ（i），κ（j））B是连接b l oc k Bκ（i）到Bκ（j）的简单源路径的集合。我们形成验证条件C：不∧α ∧→VJ：（ρS）J，伊日皮季Sπjπ∈Paths（κ（i），κ（j））其中ρS是简单源路径π的跃迁关系。(v) 确定所有生成的验证条件的有效性Fig. 1. 证明规则验证变量，其反映源中的相应转换，以及数据抽象和断言Rlj在新状态中保持。因此，在蕴涵Cij的前件处，将Ciji用作一个假设。 作为回报，验证器还必须确定转换后的basej是否成立。因此，作为验证分类的一部分，我们确认所提出的断言确实是归纳的，并且无论何时访问相应的块都有效。[ZPFG02]包含了对该规则的讨论、合理性证明和应用实例在生成其有效性意味着目标T是源程序S的正确翻译的验证条件之后，只需要检查这些含义是否确实有效。只有当这种验证（以及前面的条件生成步骤）可以以全自动的方式完成时，这里所提倡的方法才有意义ZUCK等人18601无需用户干预。可使用为Sacres项目[PRSS 99]开发的CVT工具执行部分确认任务（概述见[PZP00]）。 对于其他部分，我们需要一些我们使用STeP系统（[MAB+94]）的算术能力。 我们目前正在探索其他可以提供类似功能的包装2.3图为歼-64SGI Pro-64（简称SGI）的中间语言是WHIRL。在每一轮优化之后，编译器输出ASCII格式的WHIRL代码，该代码可以被解析器读取并翻译回图形表示。工具的描述见[ZPFG02]。图2我们提出了一个程序和几个优化适用于了B0n-500Y-0W<-1B1B0n-500B0 y-0W<-1如果！（n>= w）GOTOL2 B1n-500Y-0W<-1WHILE（n>=w）B2B1L1：w-w+y*2+3L3：w-w+y*2+3y- y +1w<- w +y * 2+3y- y +1IF（n>= w）GOTO L3w<- y +1IF（n>= w）GOTO L1B2B2B3返回(a) 输入程序L2：返回(b) 循环反转返回(c) 恒定折叠B0Y-0W<-1B1B0Y-0W<-1.t1<-0B1L3：w-w+y*2+3y- y+1IF（w = 500）GOTOL3B2返回(d) 复制传播后，L3： w<-。t1+w+3y- y +1.t1<-.t1+ 2IF（w = 500）GOTOL3B2返回死代码消除(e) 强度降低后图二、优化阶段在附录A中，我们给出了ESTA-64为优化的每个阶段产生的验证条件在这里，我们使用（a）-（e）的注释因此，例如，Ccd指的是上面程序（d）的目标相对于源程序（c）从B0到B1的验证条件，而ye表示程序（e）的y变量变量π是表示程序的程序计数器的控制变量数据映射和断言是ZUCK等人187由下式给出αab：（πb∈{1， 2}→（na=nb）<$（wa=wb）<$（ya=yb））αbc：（πc∈ {1，2}→（nb=nc）（wb=wc）（yb=yc））αcd：（πd∈{1， 2}→（nc=500）<$（wc=wd）<$（yc=yd））αde：（πd∈{1， 2}→（wd=we）<$（yd=ye））<$3：（.t1 = 2·ye）3验证循环重新排序转换重排序转换是任何程序转换，它只是改变代码的执行顺序，而不添加或删除任何语句的执行[AK02]。如果它保留了依赖关系的源和目标的相对执行顺序，则它保留了该依赖关系，从而保留了程序的含义重新排序转换涵盖了许多循环转换，包括循环体中语句的融合、分布、交换、平铺、展开和重新排序。在本节中，我们将回顾重新排序循环转换，并提出3.1重新排序循环转换考虑图1中描述的形式的循环3.第三章。 我们表示为I ={i1，...， i N}的值的集合i =（i1，...，ik）。我们用
k然后出口与“失败”端出口关于“成功”为了理解为什么这个算法将检测是否违反规则（2），请注意，违反规则的唯一方式是当存在i，j使得（i<（j）（D（i）=U（j））（P（j） i，则违反了规则，算法失败退出。如果U（k）对于k的几个不同值可以产生相同的值，则在算法中使用max是必要的。该算法具有几个理想的性质，即(i) 循环索引变量k在序列P−1（1）. 上 迭 代 。 P-1（N），就像上面的转换循环(ii) D（k）和U（k）的计算与变换后的循环执行的计算相同总之，这些属性意味着满足它们的运行时算法可以被集成到变换的循环代码中，而无需a）改变变换的循环的顺序或添加附加循环，以及b）仅为了运行时测试的目的而必须计算D（i）或U（i）特别是，带有运行时测试的转换循环可能看起来像这样：对于i=P−1（1）. P−1（N）doZUCK等人194联系我们w =D（i）r =U（i）MARK[r] = max（ MARK[r]，i）如果MARK[w]>i，则n得到0patchup_codeA[w]=....=...A[r].端然而，该算法具有两个不期望的性质，即：(i) 它需要一个大小等于A的数组MARK，以及对MARK的2N次访问。(ii) 最糟糕的是，在违反规则的情况下，算法不会检测到违规，直到写入即将发生-直到读取已经在前一次这最后一个特征使得算法作为运行时验证的工具是无用的，因为它没有表现出可测试性属性。直观地说，问题是在前一次迭代中读取的不正确的值可能已经在随后的迭代中使用，从而使程序不正确。是否存在一种算法，它具有我们想要的属性，而没有上面列出的不需要的属性如果像上面的代码一样，我们要求将运行时测试集成到优化的循环中，并且仅在循环索引具有值j的迭代期间计算每个D（j），那么答案是要看到这一点，需要注意的是，为了满足可测试性属性，我们必须能够在每第i次迭代中回答以下问题：“有价值吗？P−1（i+1）， .. . ， P−1（N） suc h，j P−1（i）和ndD（j）=U（P−1（i））？”而不计算D（j）。对于任意函数D，这是不可能的。4.5限制D到目前为止，我们也就是说，我们允许D和U足够复杂，以防止静态分析。然而，在大多数循环中，并不是D和U都不能被分析。例如，以下形式的循环的变换对于i = 1到N，A[i]=. .对于i=P1到PN，=A[i]=.. .端...=...A[U（i）].端...=...A[U（i）].其中U（i）是任意复数，不是静态分析的候选者，满足可测试性特性6。转换后的代码的一个版本，6注意，在这种情况下，可测试性属性仅在我们将关注点限制为减少依赖，忽视反依赖。例如，允许我们忽略反依赖的约束是U（i）P（i）尽管这种测试功能看起来过于昂贵，但实际上并非如此编译器在创建了置换P之后，就可以为P所特有的测试生成有效的代码。例如，如果转换是循环反转，那么测试函数就是test（i，r）=（r i）如果转换是两个嵌套循环的循环交换，则测试函数为test（（i1，i2），（r1，r2））=（r1，r2）lex（i1，i2）（i2，i1）lex（r2，r1）=r1i1r2>i2<4.6示例动态环路交换在本节中，我们将展示如何从上面给出的通用交换测试的公式中自动导出特定循环交换示例的运行时测试假设变换为：对于i= 1到 N对于j= 1到Mk = 10-j=A[i，j]=A[i-1，j-k]+ C结束结束对于j= 1到Mk = 10-j对于i= 1到 NA[i，j]=A[i-1，j-k]+ C端端这种循环交换的好处是：1）k的计算可以从内部循环中移出; 2）在具有列优先数组的语言（如Fortran）中，转换后的循环具有更好的局部性。使用for循环交换中的一般验证测试的公式，插入测试如下：对于j= 1至M，k = 10-j对于i= 1到 N如果测试（（i，j），（i-1，j-k））转到转义码A[i，j]= A[i-1，j-k]+C结束结束其中，可以看出test（（i，j），（i 1，jk >）=（i1j）=（k0）.因此，在插入实际的测试并将其移动到外循环之后（因为测试在内循环中是不变的），我们得到：⇒ZUCK等人196对于j= 1至M，k = 10-jif（k 0）goto escape_codefori= 1 toNA[i，j]=A[i-1，j-k]+ C结束结束如果因为k为0，依赖关系即将被违反，则要跳转到的循环是执行剩余迭代的原始循环。原始循环的剩余迭代可以通过以下方式执行escape_code：对于ii= 1到 N对于jj =j到 Mk = 10- jjA[ii，jj]= A[ii-1，jj-k]+ Cend端其中j是与上面的转换循环中相同的变量，包含j在优化循环中采用的最后一个值。这个转义码并不难从问题的形式说明中推导出来，但是空间限制迫使我们把它留给读者。动态平铺在前面的示例中，我们能够生成原始循环的一个版本，一旦转换后的循环中的测试检测到即将发生的依赖违反，就可以执行该版本对于更复杂的循环优化，例如平铺，在进入变换循环之前基于运行时测试简单地调整变换循环可能更容易例如，考虑图1中的循环平铺变换六、fori= 1to Nforj =1to N对于ii= 1至N步骤B对于jj= 1至N步骤B对于i=ii至ii+B-1=forj=jjtoojj+B-1A[i，j]=A[i-1，j-k]+C结束结束A[i，j]=A[i-1，j-k]+C结束结束结束结束见图6。平铺变换其中k是一个变量，其值在编译时未知。如果没有运行时测试，这种转换就不一定正确。但在k≥B的条件下，它是正确的。如果需要一个固定的区块大小BZUCK等人197编译器可以生成代码以在进入平铺循环之前测试k的值，并且如果k为B，则跳转到原始循环。另一种选择是简单地在平铺循环之前添加赋值B = min（k，maxTileSize）4.7架构考虑添加运行时测试来验证编译器优化正变得越来越容易处理，这是由于新的处理器类别的出现，这些新的处理器类别表现出1）利用并行级并行（ILP）的能力和2）当将要违反依赖性时减少运行时测试和补偿代码的成本的硬件特征大多数现代处理器都有多个功能单元来利用指令级并行性，或者通过超标量机器上同时动态调度多个指令，或者通过VLIW/EPIC处理器上编译器指定的多操作指令事实上，这些机器的挑战是在程序中找到足够的ILP，以便在每个周期中充分利用所有功能单元因此，运行时验证所需的附加测试通常可以安排在指令调度中未使用的时隙在以英特尔IA-64体系结构为例的VLIW/EPIC类机器上可以找到一些有助于测试和补偿依赖性违规的硬件功能动态消歧功能，它提供了几个指令，测试别名，可用于实现低成本的运行时验证测试。一旦一个运行时测试已经确定，一个依赖违反即将发生，IA-64的预测功能可以用来禁用指令，以保持代码的正确性。有关最后一点的更多细节，如应用于软件流水线的运行时验证，请参见[GHCP 02]。5结论我们回顾了翻译验证方法，它的优点，用于结构保持转换的主要证明规则，并描述了一个为SGI Pro-64生成验证条件的工具，ST-64然后，我们转向导致代码结构发生重大变化的优化对于重排序变换，我们提出了特殊的置换循环，可以很容易地处理最常见的优化。对于transformations的有效性是很难的，甚至是不可能的，在编译时检查，我们提出了一个运行时的翻译验证，允许积极的优化，同时不断保证没有危险的别名发生。当检测到问题时，代码会逃逸到原始循环的未优化版本，在那里它以较慢但保证正确的方式完成计算ZUCK等人198引用[AK02]兰迪·艾伦和肯·肯尼迪。为现代建筑优化散热器。摩根·考夫曼2002年。[Flo67] R.W.弗洛伊德对节目的意义。应用数学研讨会论文集，19：19[GHCP02] B.戈德堡角Huneycutt，E. Chapman，and K.帕伦软件气泡：使用预 测 来 补 偿 软 件 管 道 中 的 别 名 。 并 行 架 构 和 编 译 技 术 国 际 会 议（PACT），2002年。[MAB+94] Z.甘露A.Anuchitanukul，N.Bjørner，A.布朗，E。张，M. 科隆湖 DeAlfaro，H. 一月的时候，H。Sipma和T.E. 乌里湾STeP：Stanford Temporal Prover。技术报告STAN-CS-TR- 94-1518，部门的Comp.科学， 斯坦福大学，斯坦福，加利福尼亚州，1994年。[Nec97] G.C.Necula 携带证明代码。在POPL[Nec00] G. Necula优化编译器的翻译验证。在2000 年 ACM SIGPLAN 会 议 程 序 设 计 语 言 设 计 和 实 现 原 则（PLDI），第83-95页G.C. Necula和P. Lee。一个认证编译器的设计与实现。在AC
我的内容管理
展开
