理论计算机科学电子笔记132（2005）53-71www.elsevier.com/locate/entcs进入循环：翻译验证中的一些实际问题本杰明·戈德堡1，2勒诺·扎克1，2克拉克·巴雷特1，2纽约大学计算机科学系ACSys Group摘要翻译验证是一种确保翻译器生成的目标代码正确翻译源代码。翻译验证不是验证翻译器本身，而是验证每个翻译的正确性，生成一个正式的证明，证明它确实是正确的a正确。 近年来，翻译验证被应用于编译正确性的证明 特别是优化由作者及其同事开发的优化编译器的翻译验证工具Tcloud成功地处理了英特尔ORC编译器采用的许多优化。但是，TSTK在处理循环重新排序转换时受到一定的限制。 首先，在它所基于的理论中，不同类别的循环重排变换需要单独的证明规则。第二，Tibet在处理对同一代码块执行的优化组合方面存在困难。 最后，Tandem依赖于信息， 由编译器执行，指示已经执行了哪些优化（在当前ORC的情况下，幸运的是，该插装是编译器的一部分）。本文将对上述问题进行探讨。它提供了一个统一的证明规则，涵盖了英特尔ORC编译器执行的所有重新排序转换，描述了在存在优化组合的情况下进行转换验证的方法，并提供了用于确定发生了哪些优化的方法（而不是依赖编译器获取此信息）。保留字：翻译验证，形式化方法，循环优化，ORC，融合，分布。1 电子邮件：{goldberg，zuck，barrett}@ cs.nyu.edu2本研究部分由NSF资助CCR-0306538和CCR-0098299以及ONR资助N 00014 -99-1-0131支持。1571-0661 © 2005 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.01.03054B. Goldberg等理论计算机科学电子笔记132（2005）531介绍翻译验证（TV）是一种技术，用于确保翻译器（如编译器）发出的目标代码是源代码的正确翻译。由于验证整个编译器的困难，即确保它为每个可能的有效源程序生成正确的目标代码，翻译验证可以用于验证编译器的每次运行，比较实际的源代码和目标代码。在这一领域，这些作者和其他人已经做了大量的工作，开发了用于优化编译器的TV技术，这些编译器利用结构保持变换，即不会极大地改变程序结构的优化（例如死代码消除，循环不变代码运动，复制传播）[1，7，11]以及结构修改变换，如循环重新排序变换（例如交换，平铺），这会显著改变程序的结构[2，7，12]。在过去的一年里，在此之前，作者和他们的学生描述了一个原型工具，Tcloud，该工具是为在Intel Open研究分类器（ORC）执行大量的两个类别的转换[13，14]。尽管TMF能够在存在多个不同的结构保持和结构修改优化的情况下执行TV，但是它存在以下缺点：• TMF不使用单一的统一证明规则来验证循环重排转换，而是依赖于几个不同形式的证明规则，这取决于所应用的特定优化。具体来说，Tibet使用不同的证明规则来交换，平铺和倾斜，而不是融合和分布。从科学（和工程）的角度来看，一个单一的证明规则来处理所有的循环重新排序转换会更令人满意。• Tynchronous很难处理结构保持和结构修改优化的组合这是一个严重的缺点，因为通常只对代码执行一次转换，以实现后续的转换。• texture使用编译器生成的信息，指示执行了哪些循环优化。幸运的是，ORC在每次编译后都会生成一个包含这些信息的文件，因此不需要额外的编译器插装。尽管Tibetan从未依赖这些信息来证明汇编是正确的，它是由Tendon用来建议在特定部分上使用的证明方法的代码。B. Goldberg等理论计算机科学电子笔记132（2005）5355在本文中，我们描述了我们的方法来解决上述问题，目前正在实施。BrieViley表示，解决方案如下：• 我们已经推广了用于交换，平铺和倾斜的证明规则作为一个附带的好处，证明规则现在捕获了额外的循环转换，如剥离和软件流水线。• 当呈现有反映源代码S的一系列变换的目标代码T时，使得没有代码的中间版本（例如，在单独的变换之后）可用，T将基于它认为执行了什么变换来合成代码的一系列中间版本。也就是说，它将产生合成中间体版本I1、I2、. I n，它可能根本不是编译器创建的。然后，T将验证从S到I1的转换、对于每个j从Ij到Ij+1的转换以及从In到T的转换是正确的。• 为了避免Tcloud依赖于编译器产生的信息来确定实际执行了哪些优化，我们开发了一组语法，用于生成仅给定的此信息源代码和目标代码启发式以前被Necula [8]用于gcc中结构保持变换的TV。在本文中，我们描述了我们用于结构修改变换的TV的算法，特别是循环重排变换。本文的结构如下。第2节提供了必要的背景，以了解我们的电视工作，在个别结构修改转换的验证。第3节描述了我们用于循环优化（如交换和平铺）的证明规则如何被一般化，以包括更广泛的循环转换，包括融合，对齐，剥离和展开。第4节描述了ORC执行的优化组合的种类，以及我们使用创建代码的合成中间版本来验证此类组合第5节介绍了我们已经开发的算法，以便在没有编译器的任何建议的情况下确定已经执行了哪些最后，第6节结束。2背景本节是对我们以前在Tcloud上的工作的总结。 我们建议读者参考[13，14]以了解更多细节和示例。56B. Goldberg等理论计算机科学电子笔记132（2005）532.1变迁系统为了讨论程序的形式语义，我们引入了转换系统TS，一个转移系统S=V，O，Θ，ρ是一个状态机，它包括：一个状态变量集合V;一个可观测变量集合OV;一个初始条件Θ，系统的初始状态;以及一个转移关系ρ，将一个状态与它可能的后继状态联系起来。变量是类型化的，并且TS的状态是变量的类型一致的解释。对于状态s和变量x∈V，我们用s[x]表示s赋给x的值。转换关系指的是变量的未启动版本和启动版本，其中启动版本指的是变量在后继状态中的值，而变量的未启动版本指的是它们在转换前状态中的值。因此，例如，转换关系可以包括旧（转换前）状态下的值。我们假设每个转移系统都有一个描述程序位置计数器的变量π虽然可以为每个语句单独分配一个转换关系，但我们更喜欢使用广义转换关系，描述沿程序路径执行多个语句的效果。考虑以下基本块：B0：n-500Y-0W<-1IF！（n）GOTOB2B1：在与该块相关联的转换关系中有两个析取。第一个描述B 0到B1的路径，即π=B 0<$nJ= 500<$yJ = 0<$wJ =1<$nJ≥wJ<$πJ=B1，第二个描述B0到B2的路径，即π=B 0<$nJ= 500<$ yJ = 0<$wJ = 1<$nJ<<$πJ =B2。转移关系则是所有这样的广义转移关系的析取。可观察变量是我们关心的变量，我们将每个I/O设备视为变量，每个I/O操作（包括外部过程调用）都会将元素删除/追加到相应的变量。如果需要的话，我们还可以在可观察变量中包括一组选定过程的外部过程调用的历史。当比较两个系统时，我们将要求两个系统中的可观测变量匹配。B. Goldberg等理论计算机科学电子笔记132（2005）5357TS的计算是状态σ的最大（可能无限）序列：s0，s1，.。，从满足初始条件的状态开始，使得每两个连续的状态通过转移关系相关联。如果初始条件的可观测部分唯一地决定了计算的其余部分，则转移系统T被称为确定性的。我们限制我们的注意力，确定性的过渡系统和程序，生成这样的系统。因此，为了简化演示，我们在这里不考虑其行为可能取决于程序在整个计算过程中读取的附加输入的程序这是直接的理论和方法扩展到这样的中间输入驱动的程序。设PS=PS，OS，θS，ρS，和PT=PT，OT，θT，ρT，为两个TS如果两个系统之间存在一一对应，则称这两个PS和PT的观测量。 为了简化符号，我们用X∈ OS和x∈ OT表示这两个系统中相应的观测量。源状态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是，在终止的情况下，它们的最终状态是相容的。注意，细化是一个等价关系。我们用PT <$SS来表示PT是PS的正确翻译。我们区分结构保持优化，这承认一个目标程序中的控制和数据值到源程序中相应的控制和数据值的清晰映射，以及不允许这种清晰映射的结构修改优化。大多数高级优化是结构保持的，而大多数循环优化是结构修改的（值得注意的例子是倾斜，展开和剥离，实际上可以通过我们的结构修改和结构保持证明方法来处理。2.2结构保持优化设PS = PS，OS，θ S，ρS，PT = PT，OT，θ T，ρ T，PT是可比较的TS，其中PS 是源和PT 就是目标 为了证明PT是PS的正确翻译，对于PT的结构与PS的结构没有根本区别的情况，我们使用了一个证明规则Val，它是受计算归纳法（[3]）的启发，最初是为了证明单个程序的性质而引入的。规则Val（见[13]和[14]中的一个变量，它产生更简单的验证条件）提供了一个证明58B. Goldberg等理论计算机科学电子笔记132（2005）53可以证明一个程序改进另一个程序的方法。这是通过建立从目标到源位置的控制映射，从源变量到目标变量上的（可能受保护的）执行的数据抽象映射，以及证明这些抽象沿着目标程序的基本执行路径在Val中，假设每个TS具有切割点集合，即，的一组框包括所有初始和终端块，以及来自程序控制流程图中的每个周期的至少一个块简单路径是连接两个割点并且不包含作为中间节点的其他割点的路径对于每一条简单路径，我们可以（自动）构造出该路径的转换关系，通常，这种转换关系包含了使该路径能够被遍历的条件和该路径所引起的数据转换。RuleVal构造了一组验证条件，每个简单目标路径对应一个，其集合由源和目标之间转换正确性的归纳证明组成粗略地说，每个验证条件都声明，如果目标程序可以执行一个简单的路径，其中某些条件将源程序和目标程序相关联，则在简单路径的执行结束时，将源程序和目标程序相关联的条件仍然成立。这些条件包括控制映射、数据映射，可能还有在目标代码中保持不变的断言。与我们的方法有点相关的是比较检查的工作，其中在特定输入上比较未优化和优化版本的代码执行[4，5，6]。比较检查取决于在特定输入上找到源和目标之间的数据和控制映射，并且报告不匹配以检测优化错误。比较检查主要用于结构保持优化。2.3重排转换的翻译验证结构修改转换是那些不允许源程序和目标程序在每个切割点处的状态之间的自然映射的转换。 特别地，重新排序转换是一种结构修改转换，它仅仅改变代码的执行顺序，而不添加或删除任何语句的任何执行[2]。如果它保留了依赖关系的源和目标的相对执行顺序，则它保留了依赖关系，从而保留了程序的含义。重新排序转换涵盖了许多循环转换，包括循环体中语句的融合、B. Goldberg等理论计算机科学电子笔记132（2005）5359考虑图中的通用循环。1.一、对于i1=L1，H1，...对于im=Lm，Hm，B（i1，. ，i m）Fig. 1. 一般循环具体地，我们可以描述这样的操作：“对于i ∈ I，b ，d，B（i）”，其中i =（i1，. ，i m）是嵌套循环索引的列表，并且I是通过循环的不同迭代由i假定的值的集合。 集合I可以用一组线性不等式来描述。例如，对于图1的循环，一、I={（i1，.，i m）|L1≤i1≤H1<$···<$L m≤i m≤ H m}。这种关 系 是 由I的各种点被遍历的顺序。例如，对于图1的循环 1，这个顺序就是I上的词典顺序。通常，循环变换具有以下形式：forri∈IbyI doB（i）=ff frj∈Jby<$J doB（F（j））（1）在这样的变换中，我们可能会将循环索引的域从I更改为J，将循环索引的名称从i更改为j，并可能在循环体中引入额外的线性变换在[14]中，我们提出了图2中的规则置换。 关于细节、合理性和示例，请参见[14]。为了将规则置换应用于给定的情况，有必要确定F（和F−1），并验证规则置换的前提R1-R3。前提R1和R2确定F是双射，前提R3确定没有依赖性被转换破坏。F的标识可以由编译器提供给我们，一旦它决定了它选择应用哪个相关的循环优化。在英特尔的ORC编译器中优化器。Toggle收集这些信息，验证优化的代码确实遵循了所指示的优化，并构造验证条件。60B. Goldberg等理论计算机科学电子笔记132（2005）53R1 i∈I：j∈J：i=F（j）R2. <$j1/=j2∈J：R3. i1，i2∈I：F（j1）=/F（j2）i1i2F（i2）JF（i1）−1−1=B（i1）;B（i2）→B（i2）;B（i1）forri∈IbyI doB（i）对于rj∈Jby <$J doB（F（j））图二. 重排变换的排列规则置换选项。然后这些条件被传递给定理证明器CVC Lite[10]，它会自动检查它们。这里介绍的规则置换只处理重新排序整个循环体执行的转换。 一些优化，如软件流水线和融合/分布，似乎不属于这个证明规则的范围。下一节将展示如何使用规则置换来处理此类优化。3规则置换如上一节所述，规则置换仅涵盖从单个循环到单个循环的转换，并要求一个循环中的迭代与另一个循环中的迭代之间存在双射。考虑一个更一般的循环结构，由几个“简单”循环组成这样的循环结构可以被转换成另一循环结构。例如，在典型的循环融合变换中，有两个简单的循环（通常在相同的索引域上），它们被变换成单个简单循环，每个迭代由两个子体组成，每个子体来自每个原始迭代。其他转换，如剥离和软件流水线，也可以被视为这样的循环结构转换（我们在下面列出一些例子）。我们的论点是，经过一些预处理后，我们可以将这些类型的转换视为2.3小节中研究的重新排序转换的实例，并使用规则置换来验证它们。B. Goldberg等理论计算机科学电子笔记132（2005）5361t1Æ3.1从循环结构到简单循环形式上，循环结构包括：(i) asetI1， . . . ，在index-dom-mains中;(ii) 对于每个k=1， . . . ，n，总排序为k， overIk的元素;(iii) 对于每个k = 1，.，n，一个数m k和一个m k个物体的序列{Bk}mk这种循环结构的代码如图3所示。l l=1对于i∈I1，通过做B1（i）;. ;B1（一）11m1对于i∈I2，由做B2（i）;. ;B2 （一）...21平方米对于i∈Ik，由doBk（i）;. ;Bk（一）k1mk图三. 循环结构显然，任何形式的循环图。第2.3小节中的1对应于图中的单线3 .第三章。考虑一个典型的环路融合示例，其中输入由k=2、I1=I2和m1=m2=1的环路结构给出。融合的环于是是环结构，其中J=I1，m=2，B1（j）=B1，并且B2（j）=B1。我们也可以将循环结构称为以下形式的简单循环：forrii∈IIbyII doB（ii）通过定义：KII={l}×Il× {1，. ，m 1}B（11，i1，t1）= B11（i）l=1设（l1，i1，t1）≠II（l2，i2，t2），其中n（l1 i2且l1（0，i，1） l=1i≤p>：（k+1，i，1）l=k<$i>q（l，i，1）其他其中L（1）=p+1;L（k+1）=q+1;并且对于所有其它l，L（l）=1;和H（0）=p;H（k）=q;H（k+ 1）=Nk;并且对于每隔一个l，H（l）=Nl。两个II 而JJ J都是常规的X射线照相术，并且，再一次，规则置换的先决条件R3是平凡的 真。环路校准对于通用环路对准，分别考虑图4部分（g）和（h）中的源和目标。在这里，我们采取：KII=JJ={l}× {L l，.，H l}× {1}l=1K{l}× {f l（L l），.，f l（H l）}× {1}l=1F（l，i，1）=（l，f−1（i），1）F−1（l，i，1）=（l，f（i），1）B. Goldberg等理论计算机科学电子笔记132（2005）5365L其中fr（i）=i−Lr+ 1，f−1（i）=i+Lr−1，并且对于每个l/=r，fl（i）=Rf−1（i）= i.两个II 而JJ J都是常规的X射线照相术，并且，再一次，规则置换的先决条件R3是平凡的 真。4组合如上所述，真实的编译器可以应用若干优化来将源程序S转换成目标程序T。 在这种情况下，我们首先获得（或猜测）单个变换的序列，然后合成一系列代码的中间版本，S = I0，I1，.。 ，In= T。然后，我们必须验证从I j到I j+1的变换，对于每个j = 0，. ，n-1，并验证In确实是T。 在本节中，我们通过假设编译器给出了转换序列来说明这种方法。在下一节中，我们将讨论在没有给出变换序列的情况下如何处理的算法对于i=0到99，a[i+1]：= x +5对于i=0到99，a[i+1]：= a[i+1]+ a[i+2](a) 源S=I0a[1]：=x+ 5;对于i=1到99，a[i+1]：= x +5a[i]：= a[i]+ a[i+1]a[100]：= a[100] + a[101](b) 目标T=I3图五. 输入和输出考虑图中的源程序和目标程序5（这是ORC编译器执行的实际转换 源包含在I=[0.. 99.第99章和往常一样<假设现在应用的优化顺序是对齐，然后剥离，然后融合，如图6所示：I1对齐第二个循环;I2剥离第一个循环的第一次迭代和第二个循环的最后一次迭代;I3=T融合循环。为了显示每个阶段的正确性，我们使用规则置换，应用于循环结构，如第3节所述。例如，核聚变的最后（也是最困难的）阶段，相当于表明，n1> n2=n a[n1+1]：=x+5;a[n2]：=a[n2]+a[n2+1]a[n2]：=a[n2]+a[n2+1];a[n1+1]：=x+5;这可以很容易地建立。66B. Goldberg等理论计算机科学电子笔记132（2005）53对于i=0到99，a[i+1]：= x +5对于i=1至100 doa[i]：= a[i]+ a[i+1](a) I1（路线）a[1]：=x+ 5;对于i=1到99，a[i+1]：= x +5对于i=1到99，a[i]：= a[i]+ a[i+1]a[100]：= a[100] + a[101](b) I2（剥离）a[1]：=x+5;对于i=1到99，a[i+1]：= x +5a[i]：= a[i]+ a[i+1]a[100]：= a[100] + a[101];(c) I3（融合）见图6。 优化阶段通常，编译器执行一个或多个循环优化，以实现进一步的全局（结构保持）优化。例如，图6中的最后阶段I3可以通过执行标量替换、循环不变代码运动和复制传播来进一步优化，以获得图6中所示的代码。7 .第一次会议。y：= x +5;a[1]：= y;对于i=1到99，a[i+1]：= ya[i]：= a[i]+ ya[100]：= a[100] + a[101];见图7。 结构保持优化这可以通过使用第2节中讨论的RuleVal（用于结构保留优化）添加一个额外的验证阶段来处理。因此，总体方法包括三个步骤。首先，固定n个循环变换的候选序列。其次，合成中间表示I1到I n，并使用规则置换验证每个变换的正确性。最 后，I n和目标T的 等 价 性 为：使用RuleVal验证。5试探法在本节中，我们描述了在没有编译器提供的信息的情况下，我们用来尝试确定可能对源代码执行的循环优化序列以产生目标代码的技术。B. Goldberg等理论计算机科学电子笔记132（2005）5367由于我们仍处于设计逻辑学来推断发生的转变的早期阶段，我们做了以下简化（但并非不合理）的假设：• 我们知道从源代码中的每个循环结构到目标代码中的每个循环结构的映射-也就是说，对于源代码中的每个循环结构，我们知道目标代码中的哪个循环结构是由它产生的。引用的过程、条件分支、引用的变量等）。• 我们有一些关于编译器执行某些转换以启用其他转换的顺序的知识，因为大多数转换遵循公知的转换序列。5.1一般方法我们的一般方法是将编译与代码的中间版本的合成相结合，将下面的算法应用于源代码中的每个循环结构和目标代码中相应的循环结构输入：源循环结构S和目标循环结构T。输出：算法• I：=S• 同时！（I）do· Opt：=NextOpt（I，T）;NextOpt将中间循环结构和目标循环结构作为输入，并返回一个可能的下一个优化，可以执行该优化以使中间代码更接近目标代码，或者如果不存在则返回一个优化;显然，这是包含优化的部分。· 如果Opt=0，则返回· IJ：=Opt（I），创建由猜测的优化产生的新的中间形式。· 使用规则置换或规则值来建立IJI。 如果验证失败，以“失败”退出。end while• 使用“有效”退出当然，一个问题是上述循环的终止。由于我们正在生成可能实际上没有由编译器生成的代码的中间版本，因此可以想象，该过程可能是非终止的（例如，考虑重复应用循环融合，然后是循环分布但在68B. Goldberg等理论计算机科学电子笔记132（2005）53实践，这不会发生。我们利用我们对编译器通常执行的优化序列的了解来限制我们猜测编译器可能在每个步骤执行的可能优化。因此，例如，如果已经在循环结构的某个部分上执行了分发，则可以防止NextOpt最后，由于编译器通常在任何单个循环上执行短序列的优化，因此我们对我们愿意创建的中间版本的数量和循环的迭代次数虽然我们已经考虑使用回溯来尝试多个猜测优化序列，以达到编译器生成的循环结构的实际优化版本，但我们的第一组实验将在不使用回溯的情况下我们期望循环的未优化和实际优化版本的形式将为我们创建中间版本提供一个非常好的指导，而不需要回溯5.2选择下一个优化我们选择下一次优化的标准如下：(i) 循环的数量有变化吗(ii) 循环的嵌套深度是否改变了？(iii) 循环体的大小是否改变了（即，是否有更多的语句被添加到循环体中）？(iv) 循环迭代的边界是否改变了？(v) 循环索引变量的使用是否在使用的主体中发生了变化（例如，数组下标中的“i”是否(vi) 是否在循环中引入了非单位步长（例如“for i = 1 to N step k”）？这些标准很有用，因为不同的循环优化会显示标准的不同组合。 我们第一次尝试的启发式排序测试在上面指定的顺序，但我们希望通过实验来完善这种排序。我们的工具预计将识别的循环优化以及它们产生的更改如下所示。• 剥离会添加一个新循环，并更改新循环和原始循环的循环边界。• 对齐会导致循环边界发生变化并添加一个常量B. Goldberg等理论计算机科学电子笔记132（2005）5369循环体中的循环索引变量的每次出现• 展开会导致循环体的大小增加，并在迭代中出现非单位步骤。• 平铺会导致循环嵌套深度的增加，（新的）外部循环中的非单位步长，以及内部迭代的循环边界的变化。• 交换会导致数组下标中循环索引变量的顺序发生变化，并可能导致循环边界发生变化• 融合会导致环的数量减少，环体尺寸增加。• 分布会导致循环数量的增加和循环体大小的减小。在下一节中，我们将提供更多的细节，这些细节是由第4节中的示例激发的。5.3NextOpt启发式我们在第3节中描述的循环结构的广义表示的好处之一是，在这个框架中源循环和目标循环的表示有助于为发生的转换提供线索。我们没有为所有可能的转换（我们仍在研究）给出一个完整的NextOpt定义，而是通过描述NextOpt在图中的例子中的行为来激励我们的工作。五、图5中的源代码可以表示为广义循环结构哪里forrii∈IIbyII doB（ii），II=（{1}× {0. 99}× {1}）（{2}× {0. 99}× {1}）。图中的目标代码5可以表示为对于jj∈J J，通过<$JJ做B（jj），哪里JJ =（{1}× {0}× {1}）（{2}× {1. 99}× {2}）（{3}× {99}× {1}）。请注意，我们将循环体的一次出现识别为一次迭代70B. Goldberg等理论计算机科学电子笔记132（2005）53源代码的第一个循环体的实例，i= 0，目标代码的最后一行作为源代码的第二个循环体的实例，i= 99。通过这种表示，以及对源和目标循环体的粗略检查，可以很容易地看到以下内容(i) 在II中，每个三元组的最后一个元素是1，但在JJ中有最后一个元素是2的三元组。这表明在目标循环结构中的简单循环内，块的数量增加了，这是在融合或展开发生时发生的。(ii) 由于II和JJ中的中间元素的范围都不包含“阶”（例如{1，k+1，2k+1，. }），则不太可能发生展开。这也可以通过注意到目标中的简单循环的主体在尺寸上增加（即，内的区块数量循环）不是具有不同数组索引的彼此的副本。因此，展开不太可能产生这组块。(iii) II的第一个元素的范围是{1， 2}，而JJ的第一个元素的范围是{1， 2， 3}。这种情况表明目标循环结构中的简单循环的数量比源循环结构中的简单循环的数量增加，这种情况只能在剥离或分布时发生。(iv) 由于与II相比，分配将导致JJ的第三元素的范围减少-并且在这种情况下没有发生-因此分配不太(v) JJ中的中间元素的范围（即，循环索引变量的值的范围）是{0.100}，而II的中间元素的范围是{0. 99}。循环索引变量上限的增加或下限的减少表明可能发生了对齐（它也可能表明偏斜，但当偏斜发生时II和JJ之间的关系与我们在这里看到的基本不同一旦这些观察，我们就剩下一组优化- 即融合、剥离和对齐-它们被认为是在从源到目标的途中执行的第一优化的候选者。因为对齐和剥离被认为是支持融合的转换，而不是相反，所以NextOpt选择对齐或剥离作为构建下一个中间版本代码的优化是有意义的（这是我们在启发式中利用编译器知识的一个例子）。尽管英特尔ORC编译器实际上在此示例中执行了先对齐后剥离的操作，但在验证过程中，在对齐前剥离的启发式选择也是可行的。B. Goldberg等理论计算机科学电子笔记132（2005）5371J通过选择peeling，我们将构造代码的下一个中间版本IJ，如下所示：a[1]：= x +5对于i=1到99，做a[i+1]：= x +5对于i=0到98，a[i+1]：= a[i+2] + 11a[100]：= a[101] +11因此，II J的迭代速度由II={（1，0，1）}<$（{2}×{1. 99}×{1}）（{3}×{0. 98}×{1}）{（4，99，1）}J现在，比较II有了JJ，很明显，第二个llj。5.4执行情况我们正在将这些算法添加到Tencent工具中，因此还没有实验结果来表明我们的算法有多有效。一旦实现达到了它将在各种循环转换上工作的程度，我们将使用实现来评估我们的策略，并调整我们的策略，特别是在应用上述标准的顺序方面。6结论本文介绍了三个改进，我们的翻译验证方法优化编译器。首先，我们提出了一个通用的规则，以适应更广泛的循环变换。接下来，我们展示了如何通过合成代码的中间版本并单独验证每个优化来最后，我们描述了猜测优化序列的初步算法，只给出了源代码和目标代码。我们目前正在将所有这些改进集成到我们的Tandem工具中。在我们这样做的同时，我们计划改进我们的翻译，并继续使用真实的例子来增加翻译验证技术的能力和范围。确认一如既往，我们要感谢Amir Pnueli进行了许多有益的讨论。Ying Hu为我们提供了ORC优化的例子72B. Goldberg等理论计算机科学电子笔记132（2005）53超越了以前版本的Tencent的能力。引用[1] 阿霍河Sethi和J.D.厄尔曼制造原则、技术和工具。艾迪森·韦斯利1988年[2] 兰迪·艾伦和肯·肯尼迪为现代建筑优化散热器。摩根·考夫曼2002年。[3] R.W.弗洛伊德对节目的意义。应用数学研讨会论文集，19：19[4] C.哈拉米略河Gupta和M. L.所以你要小心点。捕获代码改进转换的效果。并行体系结构和编译技术国际会议论文集，第118-123页，1998年[5] C.哈拉米略河Gupta和M. L.所以你要小心点。比较检查：一种避免调试优化代码的方法。在ACMSIGSOFT Symposium on Foundations of Software Engineering ， 第 1687 卷Lect.Notes inComp.Sci. Springer-Verlag，第268-284页[6] C.哈拉米略河Gupta和M. L.所以你要小心点。通过比较检查优化和测试优化器。在COCV 2002会议录中，J.Knoop和W.齐默尔曼编辑，ENTCS，65（2），2002.[7] S. S.穆奇尼克高级封装设计实施。 摩根·考夫曼，1997年。[8] G. Necula优化编译器的翻译验证。在ACM SIGPLAN 2000年编程语言设计和实现原则会议中，第83-95页[9] A. Pnueli，M.Siegel和E.辛格曼翻译验证。在TACAS[10] A. 施通普角W. Barrett和D.L. 迪尔CVC：一个合作的有效性检查器。 在proc14 thIntl.计算机辅助验证会议（CAV'02），计算机科学讲义第2404卷。Springer-Verlag，第500-504页[11] 法医沃尔夫和MS Lam. 一种数据局部性优化算法。 在SIGPLAN '91 Symp.编程语言设计与实现，第33-44页，1991年。[12] M.沃尔夫并行计算的高性能并行计算器。Addison-Wesley出版公司，1995年。[13] Lenore Zuck，Amir Pnueli，Yi Fang，and Benjaming Goldberg. Voc：用于优化编译器的翻译验证器。Journal of Universal Computer Science，9（2），2003。[14] Lenore Zuck，Amir Pnueli，Benjaming Goldberg，Clark Barrett，Yi Fang，and Ying Hu.优化代码的翻译和运行时验证 发表在Journal of Formal Methods in System Design上。ENTCS，70（4），2002中的初步版本。
我的内容管理
展开
