嵌入式系统的优化代码

19网址：http://www.elsevier.nl/locate/entcs/volume65.html0页嵌入式系统的验证代码Sabine Glesner1 Rubino Gei1 Boris Boesler1InstitutfurProgrammstrukturenundDatenorganisationUniversit地址：Karlsruhe，76128Karlsruhe，Germany联系电话：+49-721-608-7399，传真：+49-721-30047摘要数字信号处理器提供专门的SIMD（单指令多数据）操作，旨在大大提高嵌入式系统的性能。虽然这些操作很容易理解，但它们不寻常的功能和并行性使得自动代码生成算法很难有效地使用它们。在本文中，我们提出了一种新的优化代码生成方法，可以成功地部署这些操作，同时也验证生成的代码是输入程序的正确翻译1引言我们解决的问题，产生优化以及验证的数字信号处理器在嵌入式系统中的代码数字信号处理器（DSP）表现出不规则的体系结构，其特别允许同时执行多个操作，通常是SIMD（单指令多数据）指令，其中在两个或四个独立的操作数对上执行相同的操作。这样的操作专门用于特定的应用领域，并执行复杂的计算。 我们工作的目标是 一种用于产生优化和正确的（WRT.输入程序）代码，其不仅适用于个别情况，而且适用于各种类型的DSP。特别是，我们希望我们的代码生成方法，以满足以下标准：它应该利用DSPs的并行性的SIMD指令的形式，尽可能多地调度适当的计算，在par-history，仅受给定的数据依赖关系。此外，这种优化的结果应该被验证。特别是在嵌入式系统中，这是一个重要的标准，因为随后的改进通常是不可能的，1电子邮件：fglesnerjrubinojboe sle rg@ip d. 我的意思是。你是我的朋友. Dec 2002年由Elsevier Science B出版。诉 在CC BY-NC-ND许可下开放访问。20应用程序的机器代码可以硬连线到嵌入式系统中。在编译器构造领域，大多数翻译方法可以在生成器中实现，从而简化了编译器程序员的工作。因此，我们要求我们的代码生成方法可以实现为生成器。最后，我们希望尽可能多地使用编译器构造的成熟方法，因为它们是最佳实践，并在两个方面简化了我们的生活：我们可以回到理解良好的理论基础上，编译器生成器。验证和优化代码生成是嵌入式系统软件开发过程中的一个重要目标。嵌入式系统由在技术环境中使用的硬件和软件组成。其特点是，它们专门用于固定任务，因此它们的硬件和软件可以根据其应用领域进行定制。这种专业化是保持竞争力所必需的。通常，复杂的计算需要非常快地完成。这样的任务是由DSP完成的，这些DSP针对特殊算法进行了优化，并拥有专门的不规则硬件结构。这种处理器的部署比标准处理器便宜，因为需要几个标准处理器才能与单个DSP的性能竞争。这种论点可能不会被忽视，因为嵌入式系统市场是一个大众市场，非常敏感的成本。在这个市场中，我们看到越来越多的功能部分在软件中而不是在硬件中实现的趋势。这给我们带来了更灵活的优势。相同的硬件可以很容易地适应稍微不同的环境。因此，这意味着软件应该用更高级的编程语言（现在还不是标准）来编写这反过来意味着嵌入式系统处理器的编译器是必要的。我们专注于DSP，这是嵌入式系统中处理器最复杂的情况。由于嵌入式系统的性能要求非常严格，因此DSP的制造商需要高度优化。此外，它们需要是正确的，因为在纠错和进一步开发的意义上的维护是不可能的因为许多程序被硬连线到嵌入式系统中。乍一看，编译方法的验证，优化和可实现为生成器的要求，特别是通过建立在已经存在的生成器上，似乎是不兼容的，因为它太昂贵了，如果不是不可能的话，自动验证生成器实现或生成的代码。相反，我们选择了程序检查的方法[2，7，3，38]，该方法已经成功地应用于Veri x方法[17，13，19，20]，该方法显示了如何为标准处理器构建编译器，检查其结果。编译器中的代码生成过程在计算程序的中间表示之后开始。在我们的方法中，我们选择静态的单一赋值中间表示，因为它什么也不显示21而是函数数据依赖性，这是在并行调度计算时要考虑的唯一约束。通常，编译器中的代码生成阶段被划分为几个阶段，它们是代码选择、寄存器分配、指令调度、寄存器分配和资源分配。尽管它们之间存在联系，但人们试图将它们彼此独立地解决，以将复杂性保持在合理的范围内。由于我们的前提是尽可能地应用编译器构造的好理解的方法，所以我们在代码生成阶段选择相同的任务划分在本文中，我们集中在代码选择和指令调度，因为他们是一个编译器的代码生成过程中的关键阶段，如果一个人想要开发的SIMD并行。由于程序的静态单分配中间表示是其节点是操作并且其边表示程序的数据流的图，因此可以经由将中间表示的子图映射到目标处理器的指令的图重写系统来进行代码选择。生成DSP代码时的特殊问题是SIMD指令可以对不同的独立操作数对执行相同的操作。这意味着纯粹的基于图重写的方法是不合适的，因为只能在局部上下文中找到合适的操作数对。我们通过将处理器架构转换为可以用扩展的图重写机制处理的等效架构来克服这个问题：每当处理器上的操作单元计算SIMD操作时，即，n个操作并行，该单元由n个操作单元代替，这些操作单元执行相同的操作，但是每个操作单元仅对一对操作数执行。为了指定这n个单元表现出与原始单元相同的行为，我们要求每当其中一个单元开始计算时，其他单元必须同时开始计算或等待计算完成。这个要求可以用一组约束来表示。每当图重写机制在中间表示中找到可以用SIMD操作计算的子图时，则对应的机器代码与该子图相关联，并且此外，生成对应的约束集合。在指令调度阶段，我们需要考虑这些约束，以获得有效的指令调度。此外，我们在验证阶段使用的约束作为证明义务，必须由生成的代码来完成本文的结构如下：第二部分，我们给出了基础我们的工作，这是程序检查领域的编译器建设，静态单赋值表示，和图重写系统。部分图3示出了如何可以扩展图重写的机制，使得规则的应用另外引起约束的生成。此外，本节将介绍如何在DSP的代码选择和指令调度阶段使用此机制。这个代码生成的结果可以使用生成的coni来验证，如第4节所示22作为证明义务的约束。在第5节中，我们将展示如何将这种代码生成方法集成到我们现有的编译器生成器环境中。在第6节中，我们将讨论相关的工作。最后，我们在第7节中总结了未来工作的特点。2基础我们工作的基础是双重的，因为我们关心的是验证和优化。 我们的验证方法基于百隆的理念程序检查，如第2.1节所示。我们的工作的优化部分的基础是一个特别适合的静态单赋值（SSA）形式，在语言FIRM中实现，我们将在2.2小节中介绍，以及在代码生成阶段的图重写系统，我们将在2.3小节2.1信任是好的，控制更好程序检查的思想[2，7，3，38]可以适用于Veri x项目[39，17，13，19，20]中所示的编译器在这里，我们总结了Veri x的相关结果。在确定编译器的正确性时，需要考虑两个方面：编译器规范的正确性和编译器实现的正确性。两者都必须正确。给定一个源程序，编译器规范C定义一个目标程序0=C（）。如果0显示与相同的行为，则由C定义的翻译是正确的。为了定义“相同行为”的概念，我们查看程序的可观察状态。这些可观测状态是初始状态和最终状态，以及通过输入和输出操作达到的所有如果需要，更多的国家，例如过程进入和退出可以被定义为可观察的。编译器规范C是正确的，i 0中的每个可观察状态序列具有对应的可观察状态序列，i对于每个可观察状态序列q0; ：;qk，在k步之后以错误消息终止，存在对应的长度为k的可观察状态序列。由于资源的限制，编译器可能无法翻译任意长度的程序。从数学上讲：对于几乎所有的程序，编译器由于资源限制而不能正确工作。这意味着我们不能期望编译器对所有输入程序都是正确的。相反，我们使用验证编译器的概念：编译器是一个验证编译器，如果翻译的目标程序保留了源程序的可观察行为，直到资源限制。验证编译器不需要为每个源程序生成目标程序。为了得到一个可行的方法，正确翻译的程序集必须足够大。为了建立代码生成工具的正确性，我们需要做两个主要任务：我们需要证明rst代码生成算法是23正确的意义在于它保留了变换后的Prorgams的语义对于第一个任务，即建立转换算法的正确性，我们需要形式化地定义中间程序表示的语义以及机器代码的语义。基于这些技术手段，我们可以形式化地证明语义是保持的。虽然我们将在今后的工作中处理这个问题，但我们在本文中集中讨论第二项任务。2.2静态单一赋值表示静态单赋值（SSA）形式[10，11，9]已成为处理各种程序分析和优化代码生成之前的程序转换的首选内部程序表示。它的主要优点包括明确的表示def-use-chains，并在此基础上，进一步的数据流信息可以推导出的容易。根据定义，SSA形式要求程序被表示为基本操作（跳转、存储器读/写、一元或二进制操作）的有向图，使得每个“变量”在程序文本中仅被分配一次。只有对这些变量的引用才能在一元或二元运算中作为操作数出现。因此，操作数显式地指示数据对其原点的依赖性。SSA表示的有向图是程序的控制流和数据流图SSA形式是一个非常优雅和易于理解的程序表示，只要我们只专注于处理当前过程的局部变量。处理对非局部变量、数组、记录字段、对象属性等的访问，通常，存储器访问的处理导致额外的复杂性。Martin Trapp [37]引入了显式依赖图，一种严格的SSA形式，用于处理这些额外的问题。这些显式依赖图已经在我们的库FIRM中实现为抽象数据类型，[36]。其特性可概括如下。从外部看，FIRM中的程序表示可以通过添加不同类型的节点来成功地生成：数据节点表示一元和二元操作（算术，逻辑，.）;传入边表示其操作数;传出边表示结果的使用。块节点表示基本块;所有其他节点与它们所属的基本块相关联。控制节点表示跳转和过程返回。此外，控制节点可以依赖于一个值，该值强制控制有条件地遵循所选择的路径。例如 ， 在 条 件 语 句 的 实 现 中 ， 条 件 的 值 强 制 控 制 进 入 then 或 else-alternative。每个块节点具有一个或多个这样的控制节点作为其前任。一个基本的blocknodes，x=（x1; ：;xn），表示分配给变量x的唯一值，作为在24Const块添块2Cond添块添PhiJMP图1. 企业实例其中xi表示在通过块节点的第i个前趋的控制路径上定义的x的值; n是块节点的前趋的数目。存储器节点表示存储器访问，即。e. 访问非局部变量，如上所述在第一近似中，存储器节点可以被认为是对全局状态变量存储器的ELD的访问但这幅图的细节允许更详细的分析。该分析然后可以展示哪些存储器访问寻址重叠的存储器区域并且因此真正地彼此依赖如果没有这种额外的分析，所有的内存访问都必须严格按照时间顺序进行;重新排序可能会导致从内存中获取错误的值。FIRM表示可以在遍历从编译器前端生成的属性语法树的树遍历期间容易地生成FIRM库的进一步操作允许对表示进行导航和查询，以及对表示进行转换。最后的代码生成可以看作是一个模式匹配过程的SSA表示的程序。作为一个例子，图1显示了程序片段的FIRM表示：a：= a+2; if（..） f a：= a+2; g b：= a+2在第一个基本块中，常数2被加到a上。然后，第二个节点根据比较的结果，将控制权传递给\then”或\next”块。在\then”块中，常量2被添加到前一个add节点的结果中。在\next”块中，Phi节点选择使用变量a的哪个可达定义，if语句之前的那个或\then”块中的那个。252.3代码生成阶段重写系统是用于代码生成的编译器构造中的已知技术。在大多数情况下，程序的中间表示是一组树，这些树在代码生成阶段通过自下而上模式匹配器（Bottom Up Pattern Matchers，BUPM）[16，14，15]或自下而上重写系统（Bottom Up Rewrite Systems，BURS）[28]等技术重写。这两种机制都使用规则来重写树：例如（+（r; c）！r; code）是一个规则，用于根据结果重写两个操作数的加法。此规则的目标代码代码将同时发出。我们使用图而不是树，因为这样我们就不会丢失关于程序的语义分析的任何信息，当使用树时，我们必须重新计算以进行优化。在我们的中间SSA表示FIRM中，程序由具有显式数据和控制流依赖关系的图表示。因此，在代码生成期间我们的代码生成器生成器（称为CGGG）[8]读取规范并生成使用BURS的代码生成器图重写机制。代码生成器有两个主要步骤：首先计算图的所有可能的规则覆盖，然后找到最便宜的一个。第一步是基于上面提到的规则。一个规则有一个非循环模式，如果第一个模式匹配一个子图，它将被第二个非循环模式重写（见下面的例子）。在第二步中，A-搜索算法搜索具有最低成本的覆盖。它返回重写规则搜索图中的路径。通过遍历该路径并在路径的每个节点执行相应的代码来发出代码，该路径将目标代码打印到le。搜索必须照顾至少两个问题：第一个问题出现，如果一个节点（Φ）想要使用的输入在一个基本块的开始，这是在另一个基本块的结束产生。 这种情况在各种for循环中都会发生。其次，一个基本块中的节点想要使用一个尚未产生的输入，因为它是在另一个尚未处理的基本块中产生的。在这两种情况下，搜索都会生成条件来通知有节点必须产生特殊结果，否则代码将不正确。来自代码生成器规范的规则的示例是：规则a：Add（b：Register b）-> s：Shl（d：Register c：Const）;结果d：= b;EVALfATTR（c，value） =1;g发射机FG这个规则描述了两个操作数的加法。在规则的左边，第一个操作数是一个短名为b的寄存器。第二个操作数也是第一个操作数，由短名称标识。规则的左边是一个有向非循环图。如果代码生成器在26图，它用规则的右边重写它。可能又是一场大爆炸。重写后，执行EVAL代码。这段代码将常量1放在Const节点的属性eld值 结果指令通知寄存器分配器寄存器d等于寄存器b。3DSP的代码生成典型地，DSP采用SIMD指令，其并行地对独立数据执行统一的复杂计算。如果一个人写assem- bler代码，这样的处理器，可以确保统一的计算组合正确，以利用SIMD并行。相比之下，当使用更高级的编程语言时，人们通过算法来解决问题，从而很难将独立计算关联起来以便将它们并行化。这是一个高度优化的编译器的工作-在本文中所描述的工作的目标-检测和相关的独立的计算，可以并行执行。作为技术手段，我们介绍了图重写系统与验证约束。在代码选择期间，生成验证约束。 这些约束用于指导指令调度阶段。此外，在验证阶段（见第4节）检查验证约束。3.1动机为了激发我们的方法，让我们进行一个思想实验：假设一个SIMD运算单元，它接受n对操作数并返回n个结果。从概念上讲，我们也可以考虑n个独立的操作单元，每个操作单元接受一对操作数并返回一个结果。这n个操作单元或者同时工作，或者根本不工作，即，他们的执行从不重叠通过这种处理，我们几乎与标准处理器的代码生成中的情况相同 在技术术语中，这意味着给定程序的SSA图表示，我们搜索n个部分DSP指令的局部规则覆盖。为了得到实际DSP的有效指令序列，我们需要通过将多达n个部分独立指令组合成单个DSP指令来将这些部分DSP指令全局地放在一起。我们使用约束来表达这种全局连接。约束通常是表达全局相关性的方法，因为约束中使用的逻辑变量要么没有实例化，要么全局具有相同的值，从而携带和传输本地信息。27Max我我变量top和一元谓词op（t），其中i是我们的思想实验开始了如果t=top，则op（t）为1，否则为08 i 8 j 8 op：t op= t op_ j t optopjtop3.2具有验证约束的我们使用2.3小节中描述的BURS图重写方法，并通过约束生成机制对其进行扩展。在原始形式中，图重写规则是三元组（lhs; rhs; code），其中lhs和rhs是规则的左侧和右侧，code是使用该规则重写图时发出的代码。我们使用四足动物（lhs; rhs; code; vars）代替。 LHS、RHS和代码具有与上述相同的含义。VAR是一组特定于规则的变量和谓词，当用该规则实例重写图时，该变量和谓词被生成并用唯一的编号索引这意味着，每当同一规则被应用多次时，都会为每个应用程序生成一个新版本的vars给定一个DSP指令集，我们将计算n个单独结果的每个SIMD指令分解为仅计算单个结果的n个独立部分DSP指令。对于每个这样的DSP运算操作，我们引入全局变量top，表示最多需要的时间量执行DSP操作。当应用描述部分DSP指令的规则时，即代码是部分DSP指令op时，我们生成我我这个规则的应用。意图的含义如下：t_op是在分解的DSP上执行部分DSP指令从我我在代码选择期间，我们将规则应用于图中的节点，从而发出代码以及变量和谓词。其思想是对生成的变量进行赋值，从而定义部分DSP指令的并行调度。这种并行调度必须满足两个条件：同时性条件此条件说明n个部分DSP指令并行或顺序执行，但不是并行执行：i j i j max该条件规定，对于每个时间t，不超过n个部分DSP操作可以被分配给相同的原始DSP单元：op8t8 op：Pi（t）n在指令调度过程中，必须对部分DSP指令进行合并使得这两个条件为真。注：在以后的工作中，我们还希望解决寄存器分配问题。DSP中的SIMD指令通常采用两个携带n对输入值的输入寄存器，并返回一个携带n个结果的输出寄存器。因此，有必要生成另一种变量来表示寄存器，特别是承载SIMD指令的输入和输出值寄存器赋值的任务是为这些寄存器变量提供一个有效的赋值。op283.3DSP的代码选择与指令调度给定一个具有验证约束的图重写系统，我们可以生成代码选择和指令调度阶段。该原理与通过DSP指令的特殊处理扩展的标准处理器的代码生成的情况相同。在这里，我们给出了代码选择和指令调度阶段的算法。该算法的输入是作为中间程序表示的FIRM图以及具有验证约束的图重写系统。(i) 在本地搜索所有可能的规则覆盖。此步骤的结果：图中的每个节点都分配了所有规则，这些规则的左侧与从该节点开始的有向无环图相(ii) 搜索由实现以下两种算法的成本函数指导的全局规则覆盖：更喜欢DSP指令：我们假设DSP是利用在prob- lem领域，可以更有效地解决与复杂的DSP操作比与标准处理器的操作。这意味着我们需要优先使用DSP指令。当搜索全局规则覆盖时，我们更喜欢那些发射代码是DSP部分操作的规则。更喜欢更复杂的DSP指令：此外，DSP将复杂的计算封装到一个操作中。这意味着我们需要优先选择那些左侧覆盖图的部分比其他规则更大的这一步的结果：一个带注释的FIRM图，这样一个规则分配给图中的一些节点。注意，如果一个节点位于匹配区域的内部，那么它不需要分配一个规则，因为它将被与它的一个子节点相关联的规则重写。注：除了成本函数的特殊设计外，该步骤与标准处理器的代码生成中的相应步骤之间的差异。(iii) 计算所选指令的顺序时间表。从表示程序结果的FIRM图中的节点开始，归纳收集其结果用于计算程序结果的所有节点。 这样我们就可以将节点放入一个顺序的时间表中。此步骤的结果：有效的顺序计划。备注：同样，此步骤与标准处理器代码生成中的相应步骤之间没有差异。(iv) 通过将几个数据独立的部分DSP指令放入单个DSP指令中来计算并行调度。注意，两个操作是数据独立的，29FIRM图中相应节点之间的路径。在这一步中，我们通过线性调度，把部分DSP操作放在一起，只要它们是数据独立的，只要它们之间的所有操作调度也是数据独立的。因此，我们必须注意的是，预订条件和预订的条件是满的。为了确保第二个条件，我们必须注意不要并行调度n个以上的部分操作。由于在线性调度中，只有在处理指令完成的情况下才执行指令，因此通过DSP的bevavior来确保第一条件。(At至少，这是处理器向外部显示的行为，不管指令是无序调度的还是超标量形式的。）可能的情况是，由于FIRM图中的数据依赖性，我们不能总是精确地调度n个部分DSP操作，而只能并行地调度小于n个示例：TriMedia处理器飞利浦开发的TriMedia处理器[33]是一款专为多媒体应用而设计的DSP它结合了一些指令的过程中，荷兰国际集团的视频根据MPEG标准。在视频解码过程中，可以使用TriMedia的特殊指令ume8uu它计算无符号8位数据的绝对值的无符号和。该指令ume8uu是典型的SIMD操作，计算四对独立操作数的四个结果。要生成代码的三媒体，我们需要模型这个指令由四个独立的部分指令计算完全相同的结果为一对输入。在指令调度过程中，我们需要寻找数据独立的部分ume8uu指令，可以并行调度。4使用程序检查进行在本节中，我们将展示如何建立代码生成器的正确性，实现第3节中提出的方法。因此，我们假设底层的图重写系统是正确的。(The这种假设的证明有待于今后的工作。）如果满足下列条件，则转换后的程序是正确的：I 全局规则覆盖是FIRM中间程序表示的正确规则覆盖.II 用于生成机器码的图形重写规则必须已正确应用。III 顺序调度的并行化不改变数据依赖指令的顺序，并且满足预定和不确定性条件。IV内存和寄存器写入正确。30对于代码生成实现的验证，我们使用检查器方法。实际上，不可能验证由代码生成器生成器生成的代码生成器或代码生成器生成器本身。我们通过应用程序检查来验证代码生成阶段的结果来避免这种情况。 通过重申正确性条件I至III，我们为检查器定义了以下验证任务(i) 如果忘记了图形重写规则注释，检查输入的FIRM图形和注释的FIRM图形是否相同(ii) 检查应用的图重写规则是否确实匹配FIRM图的相应子图。(iii) 检查时间表是否有效，即，检查是否所有子图都根据BURS方法进行了评估。(iv) 通过再次应用图重写规则重新计算代码生成器结果。从而检查重新计算的结果和原始结果是否相同。(v) 检查在顺序计划的并行化期间数据依赖性是否持续：因此，检查并行化计划的顺序是否此外，检查并行调度的部分DSP操作是否不超过n个，以使预订条件有效。第一个任务实现条件I，第二、第三和第四个实现条件II，而第三个实现条件III。在未来的工作中，我们将研究如何检查条件IV。(The由于目标处理器的顺序操作语义，自动确保了错误条件：顺序指令调度中的操作以该顺序或以显示完全相同的结果的重新排序执行乍一看，人们可能会认为检查任务与原始计算一样昂贵，但这不是真的：当检查代码生成的正确性时，我们对结果是否是最佳的一点也不感兴趣我们只关心正确性。这意味着实现对优化的或甚至最优的指令序列的搜索的代码不需要被验证。仅某些中间步骤以及结果需要被验证，从而大大简化了验证任务。验证任务独立于具体的源或目标语言，但只依赖于SSA中间表示。因此，我们不需要为不同的源语言和目标语言实现检查器，而是可以生成它们。在这样做时，我们只需要验证一次检查器生成器实现，而不是分别验证每个检查器实现。315一体化我们的代码生成器生成器的当前版本读取代码生成器的规范，并基于BURS生成图形重写系统。代码生成器计算所有可能的封面和搜索最inexpensive一个。当在最便宜的封面中应用重写规则时，不会直接发出相应的代码，而是执行用C编写的Emit代码。这段代码将目标（例如汇编程序）代码打印到一个le。我们将通过扩展EMIT代码来打印额外的约束信息，从而扩展此机制以生成变量、谓词和约束。这个扩展可以很容易地完成。由生成的代码生成器计算的代码生成的结果是具有部分DSP操作以及约束的顺序调度在下一阶段中，我们检查现有的FIRM图中的数据独立的部分DSP操作，并将它们与其他合适的部分DSP操作组合以成为完整的DSP操作，如子部分3.3所述。记住，FIRM图中的两个操作是独立的，他们之间没有直接的路径。对于一个单一的操作对，这个检查可以在二次时间O（n2），其中n是在FIRM图中的n个节点的number尽可能有效地寻找检验这一性质的算法和数据结构将是今后研究的任务要实现一个检查器，我们需要实现步骤1.到5.如第4节所述。这可以直接完成。此外，我们还可以实现一个检查器生成器，如第4节所讨论的。这些实现取决于未来的工作。正如我们所展示的，实现本文中描述的方法所需的修改很简单，因此我们可以很容易地将它们添加到我们现有的工具中。在未来的工作中，我们将研究[26]中的方法是否可以用于自动生成DSP并行器。6相关工作相关工作涉及编译器研究的两个方面：构造可证明正确的嵌入式系统编译器以及优化编译器。Veri x [17，13，19，20]是德国卡尔斯鲁厄、基尔和乌尔姆大学的一个共同研究项目，旨在开发用于构建正确编译器的方法，将顺序真实世界编程语言翻译为标准处理器的机器代码。这个项目已经取得了进展，建立索赔，这是可能的编译器构造的传统框架内，可证明正确的编译器，特别是通过部署生成器。特别是，一个概念的正确性已经给出了这是基于一个程序的可观察的行为。程序检查[2，7，3，38]用于将验证成本保持在合理的限度内。veri x项目没有解决不规则目标ar的问题32建筑在[27]中，展示了如何检查GCC的一些后端优化。证明携带代码[29，30，31，12]是另一种较弱的方法来构造正确的编译器，它保证生成的代码满足某些必要的正确性条件。在翻译过程中，这些条件的正确性证明将与生成的代码一起构建和交付。用户可以通过使用基本上实现面向语法的类型检查算法的检查程序来重建正确性证明。Pnueli [35，34]也解决了构造正确的编译器的问题只有那些程序组成的一个单一的循环与循环自由的身体被认为是和翻译没有通常的优化编译器建设。因此，这样的程序被正确地转换，使得反应系统的某些安全性和活性特性得以维持。在最近的工作[40]中，他提出了一种验证优化编译器的理论，该理论类似于Veri x项目中描述的方法。例如[39，19]。优化代码生成方法可以成功地基于项重写机制：在[16，14，15]中，显示了编译器中代码选择阶段的生成[28]重新制定BURS（自下而上重写系统）方法最初由[32]开发。BURS是[8]的基础，图重写代码生成器的生成器，如在2.3小节中在嵌入式系统中，有几种方法可以解决DSP的优化代码生成问题：Joses项目（Java和CoSy技术用于嵌入式系统）[1]开发了一个在嵌入式系统中使用Java 的编译器环境。AJACS （Applying Java to AutomotiveControl Systems）是信息社会技术（IST）计划中的一个项目嵌入式处理器的代码生成的调查可以在[25]中找到[23]研究了遗传算法的利用和[4，5]使用基于约束的方法为嵌入式系统生成优化代码（仅限于基本块内的优化）。此外，它是研究如何编译器可以生成，使他们可以适应不同的目标体系结构。如果可以模拟这些目标架构[24]，那么结果可以帮助设计新的硬件结构。对这些方法的调查最后但并非最不重要的是，有一些方法[22，21]使用整数线性规划来优化（但不是验证）不规则目标架构的代码生成这些作品都没有生成可证明正确的代码的目标。7结论嵌入式系统中DSP的编译器需要生成优化的以及可证明正确的代码。在本文中，我们展示了如何实现这两个目标：当将程序翻译成DSP的机器语言时，33我们并行地调度尽可能多的计算，仅受源程序中给定的数据依赖性和可用操作单元的数量的限制。作为技术手段，我们将图重写系统扩展为带有验证约束的图重写系统，这些验证约束标识可由SIMD操作计算的局部程序部分，并通过必须在生成的代码中填充的约束连接这些局部程序部分。为了保证翻译的正确性，我们使用程序检查，通过证明验证约束来验证翻译的结果是正确的。特别地，检查源程序的函数依赖性是否持续，以及处理器的操作单元是否正确使用。使用程序检查给我们带来的好处是，我们不需要验证代码生成器的实现，也不需要验证生成它的代码生成器，我们只需要验证代码生成的结果是正确的。当解的正确性检查比解本身的计算容易得多时，这种方法是有帮助的。程序检查允许我们在现有的编译器构造框架内，特别是通过允许我们在计算验证结果时使用未验证的生成器。所提出的代码生成方法不仅适用于特定的DSP，而且提供了一种适用于各种目标体系结构的正确代码生成方法。本文介绍了正在进行的工作，我们要完成和改进的几个方面：在未来的工作中，我们将研究如何设计的成本函数，控制代码生成过程中的DSP指令的使用。此外，如前所述，在为SIMD指令生成代码时，我们需要通过利用FIRM图的结构来检测数据依赖性。我们将研究哪些数据结构和算法适合高效地计算此任务。此外，我们要研究代码生成的剩余阶段，即寄存器分配，寄存器分配，和资源分配，特别强调我们的DSP操作的特殊情况下，独立的输入值需要存储在同一个寄存器。最后但并非最不重要的是，我们希望在我们现有的编译器工具环境中实现所提出的方法。所提出的方法不仅适用于SIMD指令，但似乎也适用于VLIW处理器。我们将在今后的工作中探索这些可能性。最后，我们想在真实世界的应用程序中测试我们的代码生成方法我 们 要 感 谢 格 哈 德 · 戈 斯 ， otzLindenmaier， Florian Liekweg 和 WolfZimmermann对该论文进行了许多有价值的讨论和评论。引用[1] 联合A mann，D.天才，P. Fritzson，H.锡普斯河库尔弗河威廉H. Schepers和T.林德伯格 嵌入式系统的Java和Cosy技术：34乔斯计划。欧洲多媒体、微处理器系统、业务处理和电子商务技术会议（EMMSEC'99），瑞典斯德哥尔摩，1999年。[2] M. Blum和S. Kannan程序正确性检查...以及设计检查他们工作的程序。第21届计算机理论研讨会论文集，1989年。[3] M. Blum和S. Kannan设计检查他们工作的程序。Journal of the ACM，42（1）：269{291，1995.第21届ACM Symp.计算机理论（1989），pp. 86-97.[4] 史蒂文·巴什福德和雷纳·洛珀斯。定点DSP的约束驱动代码选择。第36届设计自动化会议，美国新奥尔良，1999年6月[5] 史蒂文·巴什福德和雷纳·洛珀斯。数据流图到不规则数据路径的相位耦合映射。嵌入式系统的设计自动化，4（2/3），1999年6月[6] 舒夫拉湾Bhattacharyya，Rainer Leupers，and Peter Marwedel.信号处理系统的软件综合与代码生成。 技术报告技术报告UMIACS-TR-99-57，高级计算机研究所，马里兰大学，学院公园20742，美国，1999年9月[7] M.布卢姆，M。Luby和R.鲁宾菲尔德自我测试/纠正与应用数值问题。Journal of Computer and System Sciences，47（3）：549{595，1993.第22届ACM Symp.计算机理论（1990），pp. 73-83.[8] 鲍里斯·博斯勒。由《阿凡吉茨图》编码。1998年6月，卡尔斯鲁厄大学外交官[9] R. Cytron 和 J. Ferrante 。 高 效 计 算 - 节 点 运 行 。 ACM Transactions onProgramming Languages and Systems，17（3）：487{506，1995.[10] R. Cytron、J. Ferrante和B. K.罗森静态单赋值形式的一种有效计算方法。在第16届ACM编程语言原理研讨会（POPL'89）的会议记录中，第25页。ACM-SIGACT，ACM出版社，1989年。[11] R. Cytron、J. Ferrante和B. K.罗森高效地计算静态单赋值形式和控制依赖图。Sigplan Notices，13（4）：451{ 490，1991.[12] 放大图片作者：Christopher Colby，Peter Lee，George C.Necula，FredBlau ， Mark Plesko ， and Kenneth Cline. 一 个 Java 的 认 证 工 具 。 ACMSIGPLAN会议程序设计语言设计和实现（PLDI'00），2000年。[13] 阿克塞尔·多德，蒂洛·高卢，沃尔夫·齐默尔曼。编译器后端的机械化验证。技术转让软件工具国际讲习班会议记录（STTT'98），1998年。35[14] H.埃梅尔曼 通过定期控制项重写进行代码选择。在R. Giegerich和S.L.格雷厄姆，编辑，代码生成-概念，工具，技术，计算。Springer-Verlag，1992.[15] 赫尔穆特·埃梅尔曼代码选择需要定期的终端设置。德国卡尔斯鲁厄大学博士论文atfurInformatik，M ay1994。[16] H. Emmelmann，F. W. Schrer，和R.国防军BEG -一个高效后端生成器。在 ACM Proceedings of the Sigplan Conference on Programming LanguagesDesign and Implementation，1989年6月[17] Thilo Gaul，Andreas Heberle，Wolf Zimmermann，and Wolfgang Goerigk.用程序检查构造验证软件系统：编译器后端的应用。在1999年的《检验结果验证研讨会论文集》（RTRV'99）中[18] Thilo Gaul和Antonio Kung AJACS：将Java应用于汽车控制系统。嵌入式智能会议论文集，Nrnberg。2001年嵌入式智能会议论文集，2001年2月[19] 格哈德·古斯和沃尔夫·齐默尔曼验证制造商。在E.R. Olderog和B. Ste en，编辑，Correct System Design，第201页{230.Springer-Verlag，Lecture Notes in Computer Science，vol.1710年，1999年。[20] 格哈德·古斯和沃尔夫·齐默尔曼用于统一描述多步转换的编译器和ASM或ASM。在ASM-2000中。Springer-Verlag，计算机科学讲义，2000年。[21] 丹尼尔·科斯特纳。PROPAN：一个可重定向的系统，用于后道优化和分析。ACM SIGPLAN嵌入式系统语言、编译器和工具研讨会论文集，温哥华，加利福尼亚州，2000年6月[22] 丹尼尔·科斯特纳。可重定目标的后置传递优化的线性规划。 博士论文，萨尔大学，2000年。[23] 比尔杰·兰德威尔基于遗传算法的多目标数据流图优化方法。1999年1月，在中国香港举行的亚洲南太平洋设计自动化会议（ASP-DAC）[24] Rainer Leupers，Johann Elste，and Birger Landwehr.解释型和编译型指令集模拟器的生成ASP-DAC'99，香港，1999年1月。[25] Rainer Leupers和Peter Marwedel。嵌入式处理器的可重定向编译器技术。Kluwer学术出版社，2001年。[26] 托马斯·穆ller.我们要把所有的钱都花在这上面。博士论文，Universit在卡尔斯鲁厄，1995年6月。[27] George C. Necula翻译验证的优化编译器。ACM SIGPLAN会议程序设计语言设计和实现（PLDI'00），2000年。36[28] A. Nymeyer和J. - P·加藤基于形式化BURS理论和启发式搜索的代码生成。Acta Informatica 34，第597页{635，1997.[29] George C. Necula和Peter Lee携带证明代码。技术报告CMU-CS-96-165，计算机科学学院，卡内基梅隆大学，匹兹堡，PA 15213，1996年11月[30] George C. Necula和Peter Lee 携带证明代码。 法律程序中第24届ACMSIGPLAN-SIGACT S