基于几何模型的循环和数据重用转换的程序优化技术及功能等价性检查方法

67网址：http://www.elsevier.nl/locate/entcs/volume65.html页面几何模型检查：循环和数据重用转换K.C. Shashidhara;b;1 Maurice Bruynoogheb;2Francky Catthoora;c;1 Gerda Janssensb;2a比利时Heverlee B-3001 Kapeldreef 75，IMEC vzw计算机科学部b鲁汶大学计算机科学系，Celestijnenlaan 200 A，B-3001 Heverlee，比利时c电气工程系，Katholieke Universiteit Leuven，Kasteelpark Arenberg 10，B-3001 Heverlee，比利时摘要通过应用源代码到源代码转换来优化程序是程序员中的一种普遍做法。特别是在基于方法的嵌入式系统设计框架中，初始程序需要进行一系列转换以优化计算和通信。 在并行化和自定义内存设计的背景下，这种转换被应用于程序中数组变量的循环结构和索引表达式，通常是手动而不是使用工具，导致检查其正确性的重要问题。应用的转换是语义保持的，如果转换后的程序从输入输出的角度来看在功能上等价于初始程序。在这项工作中，我们提出了一个自动技术的基础上几何程序建模正式检查下循环和数据重用转换的初始和转换程序的功能等价性。我们的技术还提供了非常有用的诊断来定位检测到的错误。1引言为消费市场设计嵌入式系统，特别是为多媒体信号处理应用设计嵌入式系统是一项复杂的任务。在性能、面积、功率和成本方面对设计的最优性的要求很高。通常，初始设计由简单的实现1 电子邮件：fkodambal，catth o o r g @im ec. 被2 电子邮件：fmaurice，gerda g @c s. 我的意思是，我的意思是，我的意思是。梭Bec 2002年由Elsevier Science B出版。诉 在CC BY-NC-ND许可下开放访问。68I：初始程序T：变换程序...for（i = 0; i 10; i++）...1'：int [i]= 0;for（i = 0; i 10; i++）对于（j = 0; j 4; j++）1：B[i][0] = 0;2'：int [0][j] = A[j];for（i = 0; i 10; i++）for（i = 9; i >= 0; i--）{对于（k = 0; k 8; k++）对于（j = 0; j 4; j++）2：B[i][k+1] = B[i][k] + A[i*4+k];3'：buf[10-i][j] = A[4*（10-i）+j];...对于（k = 0; k 4; k++）4'：B[9-i][k+1] = B[9-i][k] + buf[9-i][k];对于（k = 7; k > 3; k--）5'：B[9-i][12-k] = B[9-i][11-k] + buf[10-i][7-k];}...Fig. 1. 程序转换的一个例子高级编程语言中的规范。这种最初的设计，如果天真地实现，往往会导致一个不可接受的次优系统。这促使了有条理的设计框架的发展。设计探索和优化是在各种抽象级别上完成的，从而使软件在定制平台上的映射更加优化。一个重要的设计规则是，更高的抽象级别导致更大的优化收益。因此，通过应用源代码到源代码的转换，初始源代码可以作为系统探索例如，在并行化[3，25]和自定义内存设计[5]的上下文中，修改程序[2]的循环结构和/或引入缓存以降低数据传输成本的转换非常常见，因为它们已被证明是最有用的优化。这种全局转换的应用仍然不在当前优化编译器的范围内[10]。在实践中，设计人员手动应用复杂的转换，依赖于应用知识，经验和独创性的组合，并得到一些分析工具的支持。在上市时间的压力下，确保当今复杂规范的无错误实现是一个非常困难的问题，而且手工应用的转换进一步加剧了这个问题。因此，迫切需要用自动验证工具来补充/替代测试。此外，一般而言，有必要扩大验证和测试技术，以应对当前的挑战[7]。假设初始源代码是正确的，在这项工作中，我们解决的问题，自动检查的功能等价的转换程序与初始。换句话说，我们验证了转换不会引入任何细微的错误。图1示出了从输入-输出的观点来看在功能上等效的初始程序和转换程序的玩具示例，即，对于给定的输入A[]，分配给B[][]的值序列在两个程序中是相同的。由于程序的等价性检查问题通常是不可判定的[23]，因此自动化工具必须基于一个可判定的条件，该条件对于初始程序和转换后的程序之间的等价性是足够的。如果条件成立，69源到源变换初始程序变换程序O.K.不好。几何模型检查等价几何模型+ 错误诊断图二. 变换验证方案转换是安全的，确保等价性;否则，什么都不能得出结论。在后一种情况下，为了有用，自动化工具应该能够查明一个合理的小程序片段，这是证明等价性失败的根源。在上面解释的上下文中，将转换验证限制为检查初始程序和转换程序中的循环结构下的程序语句的计算的等价性是实际的。这些程序语句通常涉及索引变量（数组），转换循环结构通常也会导致索引表达式的转换。在变换后的程序的循环结构下进行计算时，应检查定义变量和操作变量的使用与初始程序的使用是否一一对应。在我们的方法中，这非常信息的寻址顺序和循环迭代器下的变量的索引的界限是从程序中提取，并表示为几何模型。一旦这些模型可用，就需要检查初始程序和转换程序的相应模型上的必要和充分等价条件图2将我们的方案简单地概括了一下。本文提出的技术适用于动态单赋值形式的顺序程序的循环和数据重用转换[9]。论文概要。第2节讨论了相关的工作，并与本文提出的工作进行了对比。第3节简要说明了我们在验证技术中使用的几何模型。第4节描述了本工作中的目标转换。第5节介绍了我们提出的技术来验证这些转换的正确性2相关工作通常建议的确保正确性的方法是仅允许应用预定的变换集合的先验方法，其被证明是语义保持的。如果这些转换是由一个正式的验证工具，转换后的程序是正确的建设[1，12，20，26]。70【变身工具验证】变身是否正确？设计者引导的程序转换工具源转换源程序程序手动转换编译器转换后的源程序是源程序的正确转换吗？【变身验证】目标代码是源代码的正确翻译吗？[翻译验证]编译器正确吗？[验证码]目标代码图三. 与相关工作但是，这种理论上优雅的方法存在一个明显的实际问题。定制的程序转换工具通常不适用于给定的上下文。即使工具可用，只允许预定的一组转换也是非常有限制的。 设计者希望在应用一个不在集合中的变换时，能够灵活地应用它，他们通常也缺乏将新的变换添加到现有集合中所需的形式证明的技能。在实践中，应用程序转换和编程本身一样是自然和手动的活动，因此不需要后验方法。形式验证的前沿技术，模型检验和定理证明，不适合我们正在解决的问题。模型检测是不合适的，因为我们正在处理的顺序数据占主导地位的程序，这是不服从表示为状态转换系统。在文献[4]中提出了一种用于验证非稳态系统时间特性的符号模型检验方法，这不是我们工作的重点。但是，我们确实使用类似的框架来解决我们的问题。定理证明是没有吸引力的设计师，因为经常引用的技能要求。此外，用于验证实现与行为规范[6，24]等的等效性的技术适用于检查算术和逻辑表达式，但不适用于源代码中索引变量的循环构造。通常提出的解决方案是完全展开循环，但这显然是不可行的，因为循环是嵌套的，并且在实际程序中边界相当大，特别是在嵌入式多媒体应用中。特别地，SFG-Tracing [6]提供了基于归纳的循环构造的等价性的证明，其中限制是保持排序。但是，自动化仅适用于非循环转换。相对较新的翻译验证工作[15，13，16]，其动机支持我们自己的动机，解决了一个非常相关的后验问题71我我我验证由编译器产生的目标代码是否是源程序的正确翻译，提供了对翻译器/编译器的验证的替代。在这种技术中，在可以检查的转换类和向验证器提供关于所应用的转换的足够信息所需的编译器扩展程度之间存在折衷。 与翻译相反，我们关注的是更模糊的源到源转换。更重要的是，这个问题是复杂的事实，通常转换是手工在有条不紊的系统级协同设计框架的上下文中，它是可取的，有第一个验证在源代码的水平，然后才开始编译和合成。 我们在这里的尝试是提供一个转换不经意验证的基础设施，这是翻译验证的补充。在图3中，粗体线描绘了我们正在解决的问题，并与其他相关问题进行了对比在程序集成的背景下，基于程序表示图和程序切片，提出了一种完全不同的目标，近似等价性检查方法但是，他们的方法局限于一个语言子集，省略了索引变量，因此不适合解决我们的问题。在之前的工作中，在Imec，已经证明了处理纯循环转换的方法的可行性[21]，并且已经提出了处理更大问题大小的启发式[8]。本文中提出的工作显著改进了模型，并扩展了处理数据重用转换的方法。3几何程序建模我们的方法的新颖性在于我们的技术所基于的几何模型。在过去，几何模型已经被广泛用于模拟和分析程序语句的执行，在并行编译器和常规数组合成域[9，17，18]。虽然模型本身非常简单，但它简明地表示了程序中有关数据和控制流的大部分必要信息。我们使用的公式，编码的整数变量，逻辑连接词和quantiers，也被称为Presburger公式的aerogne约束，象征性地表示域空间和它们之间的映射。[5]中详细解释了几何模型，但在这里，我们只打算给出介绍我们的技术所需的定义。对于给定的程序P，我们使用以下符号：变量read =PV oper;变量defed =PV def;变量read in statement i =PV oper;变量defed in statement i =PV def。通过对给定程序的静态分析，提取模型的以下元素：语句i的迭代域;PD iter：域中每个具有整数坐标的点只表示语句的一次执行722我M语句i中变量v的定义/操作域;PDdef，PDoper：2IDdef：= f[a1; a2] ja1=i ^a2=k+1^[i; k] 2IDitergi. 如果语句的执行由k个迭代器变量控制，则域将是k维线性有界格（LBL）[22]。例如：图1中初始程序I中语句2的迭代域如下：IDiter：=f[i; k] j 0我九零K7^[i; k] 2Z2gif-then-else构造（如果存在）通过其分支条件在域上引入额外i v i v中定义（或读取）的变量的定义（或操作数）域。语句i描述在语句的所有可能执行期间访问变量的哪些元素。在这些域中具有整数坐标的每个点对应于被写入（在定义域中）或被读取（在操作数域中）的变量的恰好一个元素。对于d维数组变量，定义域和操作域将是相同维的LBL.例如：I的语句2中B[][]的定义域和A[]的操作数域为：2B2IDoper：= f[a3] ja3=i4+k ^[i; k]2IDiter g2A2定义的变量v d和第k个操作数之间的依赖映射语句i中的变量vo;P Mvd（vo;k）：依赖关系映射是一个inte-描述哪些元素的完整信息的元组关系定义变量的大小取决于在语句的所有可能执行期间操作数变量的哪些元素。关系中的每个元组对应于定义变量和操作数变量的元素之间的一个依赖映射。例如：定义变量B[][]与I的语句2中的第二个操作数变量A[]之间的依赖映射为：我2B（A;2）：= f [a1; a2]！[a3] ja1=i^a2=k +1^a3=i4+k^[i; k] 2IDiterg依赖映射M：D def！从定义中可以明显看出，D运算是从整数定义域到整数运算域的部分函数，它既不是满射也不是内射。[5]的模型包括捕获数据流信息的其他定义，如依赖距离向量、方向向量等。但它们与等价性检查相关的程度仅在于它们提供有关索引变量元素之间DEF-USE排序的信息。这里要强调的一点是，上述模型可以从任何提供循环和索引变量的编程语言编写的程序中提取。这使得等价性检查独立于初始程序和转换后的程序所用的特定编程语言。此外，我们想补充的是，解释的符号保持简单，以保持清晰。仅仅是符号73如果在一个语句中定义了多个变量，则为successes假设。要遵循的转换验证技术要求转换仅更改循环结构和索引表达式，而不更改其他内容。考虑到正在解决的特定问题，这一要求是合理的。下面列举的假设使要求明确。在许多程序转换框架中，通常将程序rst转换为动态单赋值形式，其中每个变量（数组元素）仅写入一次[9]。这为应用优化转换提供了更多的自由。因此，我们要求程序是单赋值形式的，并且它们没有指针。我们假设在[5]中部分描述的预处理阶段已经正确地将源代码转换为所需的形式。索引表达式和给出迭代器边界的表达式都是只包含周围迭代器变量的简单函数。只有向量变量被验证。涉及标量的数据流，没有循环结构和索引变量，可以用第2节中提到的处理算术和逻辑表达式的其他技术来处理。如果源代码被组织成两层，则与其他技术的集成是直接的，其中，循环构造和索引变量被排序成一层，标量被排序成另一层。 这其实是很重要的以便于对前者进行手动转换，而将后者的优化留给编译器[5]。转换不会更改程序中的变量名及其类型。我们假设转换仅涉及（1）引入通过复制其他数组元素写入的缓冲数组（缓存），以及（2）重新组织循环结构，该循环结构保留应用于写入语句右侧的数据元素的函数，即，我们的分析只支持索引表达式的修改和由缓冲器我 们假设已经验证了数据ow是正确的，初始程序和转换后的程序，即，每个数组元素在被使用之前被定义。4优化转换4.1循环变换当目标是增加并行性和有效利用内存层次时，循环变换在程序优化中起着至关重要的作用。74真恶心。它们作为索引集上的矩阵操作已经得到了很好的研究。 最基本的循环变换是：排列/交换，倾斜，反转和紧密嵌套循环上的碰撞。通过连续应用这些本原类型的Auberne幺模变换，可以导出一大类普遍应用的循环变换[3]。循环分布/ ssion/splitting、合并/折叠/融合、条带挖掘/平铺、展开是不能从上述原语导出的其他重要循环变换。在实践中应用的大多数循环变换都属于上述类型之一。此外，其中一些转换只是为其他循环转换启用转换，本身不会导致任何优化。循环转换只改变了执行顺序，而整体计算基本上保持不变。如果程序是单赋值形式，并且DEF-USE顺序被保留，则变量的元素读写以及它们之间的依赖关系应该保持不变，以保持转换。如第3节中所解释的，几何模型捕获独立于所应用的特定循环变换的该信息，因此，使我们能够验证上述结构保持和结构修改循环变换的整个集合。图1中的示例示出了内部循环上的简单循环分布变换、外部循环和内部循环之一上的循环反转变换以及待解释的数据重用变换。尽管与用于严格优化的多媒体应用程序中的转换相比，在示例中应用的转换是微不足道的，但是它们说明了检查正确性所涉及的复杂性4.2数据重用转换有效地使用定制的存储器层次结构来利用数据访问中的时间局部性，对于在存储器系统中具有更少能量消耗的嵌入式系统的优化设计是非常重要的。硬件控制的缓存利用这一点，但在一个非常显着的能源成本。因此，对软件控制的高速缓存的兴趣越来越大。编译时引入的程序上的数据重用转换在系统级设计框架中实现了这一点[5]。数据重用转换涉及到引入一个buer变量来保存被多次访问的数据元素，如图4。布尔变量的引入通常还需要转换数组变量的循环结构和索引表达式。显然，这种转换是语义保持的。但是，在非平凡程序上应用这种转换时犯的错误可能会引入微妙的错误。图1中相当简单的初始程序和转换后的程序对demon-75初始转化图四、数据重用转换原理演示了转换。这里，buf[][]变量被引入来保存A[]1的重用元素。该示例显示了使用单个缓存的数据重用，但在实践中，通常需要多级重用，这使得手动检查语义是否得到保留变得非常困难。5转换验证技术转换验证技术是图2所示方案的一种实现。给定初始程序对和变换后的程序对（I; T），从两个程序中提取几何模型，并对模型中的各个域和映射进行必要和充分的等价条件检验如果一个条件不成立，则利用由于条件无效而生成的错误诊断来调试转换后的程序。定义了整环与映射的等价性。定义5.1域等价性：D = D0i（x2D）（）（x2D0）.映射等价性：M = M0i（（x！ y）2 M）（）（（x！ y）2M 0）。上述定义等于说当A B =和BA=时等价A= B成立，其中A和B都是整环或映射。使用Omegatest [17]等工具执行等价性检查必须以这种方式完成。在我们介绍这个技巧之前，我们定义了两个关于语句和语句集合等价的概念：定 义 5.2 假 设 s1： u[ ： ]=f （ u1[ ： ]; ： ;um[ ： ] ） 和 s2： v[ ： ]=g（v1[：]; ：;vm[： ]）be程序状态。如果u = v且f = g，则状态s1和s2是弱等价的（即，这些语句定义相同的数组并应用相同的函数）。它们是等价的，如果它们是弱等价的，并且对所有1im：u i= v i。1buf[][]变量与A[]具有相同数量的元素，这是因为单赋值形式的要求。完整转换脚本中的后续转换步骤将删除这些冗余[5，18]。76vvvMvvvv划分（ISdef）=fIR1;IR2 g，其中IR1=fi;k g且IR2=fjg。vI：InitiallProTg：raTmtransfor医疗项目{hijkL{buf[..] int n= nums [.];....v[..]= f（u1，buf，.，n）;....v[..]= g（u1，buf，..，um）;....v[..]= f（u1，u2，..，n）;....v[..]= f（u1，buf，.，n）;}....第一步：v[..]= f（u1，u2，..，n）;....j：v[..]= g（u1，u2，..，um）;....k：v[..]= f（u1，u2，..，n）;....}图五. 解释语句类的示例。 每个v[：：]都是v的不同元素，因为程序是单赋值形式的。定义5.3设P是一个程序，PS def是定义P中数组变量v的语句集。这个集合可以划分成语句类，每个类是等价语句的最大子集我们使用PR（如果需要的话，可以加上一个额外的上标）来表示P中变量v的语句类。例如，在图5中的初始程序I中，仅在语句i、j和k中定义v，上面定义的集合如下：v v v v v由于程序是单赋值的，并且有正确的数据流，初始程序I的语义完全由映射定义我iv（ w;k）它的数组和定义数组元素实际上，对于每个数组元素，它的映射都标识了数组元素。用作计算值的函数的输入的射线元素，即，每个数组元素如何依赖于其他数组元素（数组依赖性）。如果可以证明初始程序I中的每个映射依赖性也存在于变换后的程序T中，则保持正确性。然而，由于引入了buers，在转换后的程序中不一定存在映射。这可以通过在转换后的程序中追溯数组依赖关系来解决。因此，为了证明正确性，我们将检查初始程序中存在的每个数组依赖关系也存在于转换后的程序中。此外，期望变换后的程序不执行超算，即，除了输出数组之外，还使用每个定义的元素（由数据正确性暗示），并且初始程序和转换程序中的输出数组具有相同数量的定义的元素。我们在下文中对此进行形式化首先定义一个函数为：（IR）=fsjs2T，且s与IRg的命题弱等价. 在I中定义的数组元素，由I R中的语句必须在T中由以下语句之一定义： （I R）.例如，在图5中的变换后的程序T中，（IR1）=fi0;k0;l0 g。接下来，我们计算指定操作数变量对的数组依赖性77vvSnS1得双曲余切值.vCiSnS1CIMMvvvv我v(2)8，所以1我n：si2 TSdef，其中，ci是布尔，并且vu[：]，位于u0[：]的值的原点，因此用作第i个输入在I-R语句中，针对数组依赖，我们定义了一个映射对于声明， （I R）. 因为我们只对那些-0消除指定操作数变量pair（v; w）如下：0v（ w;k）：=f[a]！[b]j存在依赖项T的链Mcn（w;1），不sn1 Mcn1（cn;1），...TM不c1（c2;1）svv（c1;k）使得(1) s v2（伊俄）（3）[a]！[b]2吨Mcn（w;1）不sn1 Mcn1（cn;1）ÆTM不c1（ c2;1）svv（c1;k）g请注意，对于给定的数组v和w，几个可能不同的链长度可以存在。映射TMv（ w;k）是定义的映射的并集每一个单独的链条。此外，代码是单赋值的，因此每个链在映射中定义一组不同的元素现在验证条件可以表述为：语句类IR中的定义变量v和第k个操作数wk之间的每个数组依赖关系也必须出现在变换后的程序的语句（IR）的数组依赖关系中。形式上，让ORv 表示操作数的数量，w k表示I R中（等价）语句的第k个操作数，则：8v2IVdef，8IR 2（ISdef），8k，使得1KOR它认为：我我8i 2IRvv（ wk;k）0v（wk;k）定理5.4设I和T是一对单指派程序，且验证条件成立.如果数组元素z[i1]：[in]在I中被分配了一个值v，那么它在T中也被分配了相同的值v。S ket c h. 对于每个元素ntz[i1]： [in]，在I中分配给它的值v是函数f（u1[： ]; ：;um[： ]）。映射IMzu识别i[： ：：]元素，其用作f的第i个输入。在T中，赋值给它的值v[001 pdf 1st-31 files]由f（u0[：];：：; u0[：]）给出。 映射TM识别元素1米ZUI我我f在T验证条件确保它是相同的元素。作为这对于f的所有解都成立，由f计算的值也相同。2还需要验证转换后的程序没有比初始程序定义更多的数组元素。在测试上述验证条件之前应该进行的廉价检查是验证初始程序和转换后的程序中的定义域对于所有的实例都是相同的，即，8v2IVdef：[IDdef =【日TDdefI v8i2ISdefjv8j2TSdef例5.5为了说明该技术，我们在图1TMÆMTM00vv[7822223334450523455最好的方法，就是在最大的范围内，以最大的范围来判断。p>I中语句2的指定操作数变量对（B;A）。迭代域是：设C0：=（a4 = i^a5= k +1^a3= i 4+ k^[i; k] 2 IDiter）B和A之间的数组依赖关系由下式给出IM2B（A;2）：=f [a4; a5]！ [a3] j C0 g该函数将I中的语句2映射到T中的语句40和50。 但是，数组A被buf替换，buf是在T中的语句20和30中定义的。因此，必须使用语句20和30中buf和A之间的报表2 0 的T具有迭代域：T0Diter：=f[j]j0j3^[j]2Zg在其依赖映射中将使用以下约束C2：=（a1=0^a2=j^a3=j^[j]2T0Diter）对于语句3.0，迭代域和约束分别为：T0Diter：=f[i;j]j0i9^0j3^[i;j]2Z2g，C3：=（a1=10i^a2=j^a3=4（10i） +j^[i;j]2T0Diter）产生的依赖关系映射为：TM20buf（A;1）：=f[a1;a2]！[a3]jC2g; T0Mbuf（ A;1）：=f [a1; a2]！ [a3] j C3 g对于语句40，迭代域和约束分别为T0Diter：=f[i;k]j0i9^0k3^[i;k]2Z2gC4：=（a4=9i^a5=k+ 1^a1=9i^a2=k^[i;k]2T0Diter）最后，对于语句50迭代域和约束分别为：TDiter：=f[i; k] j 0i 9^4k 7^[i; k] 2Z2 gC5：=（a4=9i^a5=12k^a1=10i^a2=7k^[i;k]2T0Diter）产生的依赖关系映射为：TM：=f[a ;a]！ [a ;a]jCg;TM：=f[a ;a]！[a ;a]jCg40B（buf;2）4 5 1 2 450B（buf;2）4 5 1 2 5我们有：TMbuf（ A;1）：=T0Mbuf（A;1）[T0M buf（A;1）：=f [a1; a2]！ [a3] j C2_C3 g关于TMB（buf;2）：=T0MB（buf;2）[T0M B（buf;2）：=f [a4; a5]！ [a1; a2] j C4-C5 g因此，转换后的程序中的数组依赖关系是：TMB（A;2）：=TMbuf（ A;1）0MB（ buf;2）：=f [a4; a5]！ [a3] j（C2_C3）^（C4_C5）g定义：C1：=（（C2_C3）^（C4_C5））现在，满足验证条件时：IM2B（A;2）TM0B（ A;2）：=f[a4;a5]！[a3]jC0^：C1g=这可以用Omega测试框架来验证[17]。复杂性和经验。如上所述的条件检查评估控制的有效性。汉堡算法是222pn[14]第一个问题是，079是一个常数基于Fourier-Motzkin变量消除和许多其他算法的Omega测试框架[17]为Presburger算法提供了一个整数规划求解器，这在实践中非常有效80这促使我们使用Omega计算器[11]来对我们的域和映射执行条件检查。我们检查的映射是针对每个定义-操作数变量对单独进行的，因此，公式的长度仅取决于语句类的大小，并且在所有实际情况下，问题的大小仍然是合理的。在现实生活中的多媒体应用程序的实现，即， H.263视频解码器、MPEG-4运动估计、语音编码器等，对于许多复杂的嵌套循环和多维数组，在先前的工作中，对转换的检查已经被证明是可能的，只需几秒钟。 在过去，测试和基于纸笔的手动检查都花费了不合理的时间，而且不能保证正确性。 我们目前正在建立一个工具，集成调用的几何模型提取器和O兆计算器和协调所有的检查，并提供精确的错误位置信息给用户。错误诊断。一个成功的验证意味着初始程序和最终程序是等价的。失败表示一个真正的错误，或者转换超出了关于初始程序和转换程序之间的语法对应关系的假设，例如，语句右侧的函数已被修改，或者在填充布尔数组时使用了纯复制操作以外的操作。如果条件不成立，则意味着域或映射中缺少某些点。由于我们的条件检查是通过为每个语句类分别计算每个变量或每个变量对的映射的域的差异来进行的，因此得到的非空点集提供了关于错误位置的足够信息。有问题的变量或变量对以及缺失的索引值范围这是所提出的技术的非常有用的性质。6结论正确性检查是一个复杂的问题，它在许多情况下以不同的形式表现出来，无法找到通用的解决方案，因此探索解决问题的每一个入口是很重要的。在本文中，我们提出了一种方法，提供了这样的途径。其主要思想是使用静态程序分析来提取几何模型，在该几何模型上可以检查循环和数据重用转换的正确性的等价条件。在这个意义上，该方法提出了一个证明有用的几何模型检查技术。等价性检查技术在源代码到源代码程序转换的背景下具有广泛的适用性，特别是在我们的内部系统设计活动中非常适用。81在未来的工作中，我们将调查基准应用程序的方法的可行性一般来说，几何模型在抽象程序行为方面的全部理论能力以及它在解决转换验证问题方面的最终局限性都需要研究。致谢。作者感谢Eddy De Greef和MiroslavCupak在所介绍的工作过程中进行了有益的讨论引用[1] Angelo，C.， 在硅编译环境中通过定理证明进行。博士论文，KU鲁汶，比利时。1994.[2] 班纳吉大学，循环转换的重组制造商：基础。Kluwer Academic Publishers.一九九三年[3] 班纳吉大学， 循环重复。 Kluwer Academic Publishers. 一九九四年[4] Bultan，T.，R. Gerber和W. Pugh，Symbolic Model Checking of Inite StateSystems Using Presburger Arithmetic. Proc. 9th Intl.计算机辅助验证（CAV）会议，以色列。Orna Grumberg，编，pp. 400 -411 LNCS1254史普林格出版社一九九七年。[5] Catthoor，F.，S. Wuytack，E.de Greef，F.巴拉萨湖Nachtergaele，以及A. Vandecappelle，自定义内存管理方法-嵌入式多媒体系统设计的内存组织探索。Kluwer Academic Publishers. 1998年[6] 克莱森湖M. Genoe，E. Verlind，F. Proesmans和H.《追踪：可验证性设计的 方 法 论 》 。 在 Correct Hardware Design Methodologies ， P.Prinetto 和P.Camurati编辑，pp. 187-202北荷兰1992.[7] Cousot，P.，和R. 嵌入式软件的验证：问题与展望。第一届国际足球锦标赛（1st Intl.嵌入式软件研讨会（EMSOFT），美国。pp. 97-113 LNCS 2211 2001年[8] Cup ak，M.，F. Catthoor和H. de Man，多媒体应用系统级循环转换 Proc.3rd Intl.高级设计验证和测试研讨会（HLDVT），美国。pp. 72-79. 1998.[9] Feautrier，P.，数组和标量引用的数据流分析。International Journal ofParallel Programming，20（1）：23-53. 一九九一年[10] 古斯，G.编译中的问题。Journal of UCS，7（5）：410-419. 斯普林格。2001年82[11] 凯 利 ， W. ， V. Maslov ， W. Pugh ， E. 罗 瑟 ， T. Shpeisman ， D.Wonnacott，Omega计算器和库，版本1.1.0。1996.可从以下网址获得：url：http://www.cs.umd.edu/projects/omega[12] 米德尔胡克山口一、和S. P. Rajan，从VHDL到高效和实时正确设计：一种形式化方法。ACM TODAES，1（2）：205 - 250.一九九六年。[13] Necula、 G.C.的 方 法， 翻译 验 证 的 优化 编 译 器。 Proc. ACMConf. onProgramming Language Design and Implementation（PLDI），加拿大pp. 83-95. 两千[14] Op pen，D.，A222pn在复杂的presburger算术上有很高的造诣。JournalofComputer and System Sciences，16（3）：323-332. 一九七八年[15] Pnueli，A.，M. Siegel和O.翻译验证：从信号到C。在正确的系统设计中，E.R. Olderog和B. Ste en，编，pp. 231-255，LNCS 1710。史普林格出版社1999年[16] Pandya，P.，A. Pnueli和L. Zuck，通过计算归纳优化翻译器的翻译验证。Tech.代表：美国纽约大学柯朗数学科学研究所。两千[17] Pugh，W.，Omega测试：一个用于依赖分析的快速实用整数规划算法。Communications of the ACM，35（8）：102-114.1992.[18] Quiller e，F.，和S. Rajopadhye，优化多面体模型中的内存使用。ACMTOPLAS，22（5）：773-815. 两千[19] Ramalingam，G.，和T.程序表示图的语义。Tech.代表：TR-900，CS部门，美国威斯康星大学麦迪逊分校。1989.[20] Samsom，H.，L. Claesen和H. de Man，SynGuide：一个用于进行交互式正确性保持转换的环境。在超大规模集成电路信号处理中，埃格蒙特等al. 编，pp. 269-277，IEEE出版社。一九九三年[21] Samsom，H.，F. Franssen，F.Catthoor和H.视频和图像处理规范的系统级验证第八届国际会议论文集Symp.系统综合（ISSS），美国。pp. 144-149.一九九五年[22] 蒂勒湖，和联合Arzt，大规模并行架构的综合。International Journal ofHigh Speed Electronics，2（4）：99-131. 一九九三年[23] Tsichritzis，D.，简单程序的等价性问题。Journal of the ACM，17（4）：729-738. 1970年[24] van Aelten，F.，J. Allen和S. Devadas，同步，全局控制，逻辑设计对信号流图的基于事件的验证。IEEE Trans. on CAD of Integrated Circuits andSystems，13（1）：122-134.1994.[25] Wolf ， M.E 、 和 M.S. Lam ， A Loop Transformation Theory and anAlgorithm to Maximize Maximize Maximize Maximizing.IEEE Trans. onParallel and Distributed Systems，2（4）：452-471. 一九九一年83[26] 吴伟，和A. Jantsch，设计转换技术的调查。Tech.代表：瑞典皇家理工学院电子系1999年[27] 杨伟，S. Horwitz和T.代表，检测具有等效行为的程序组件。Tech.代表：TR-840，CS部门，美国威斯康星大学麦迪逊分校。一九八九年