双向CTL：优化时间逻辑生成Java编译器的效率验证

理论计算机科学电子笔记190（2007）49-63www.elsevier.com/locate/entcs用双向CTL凌芳1、2佐佐正孝3部东京工业大学数学与计算科学研究所，东京152-8552，Meguro-ku，O-okayama，2-12-1，Japan摘要已经有一些研究工作，分析和优化程序使用时序逻辑。然而，没有评估的优化时间或执行时间的这些实现已经做了任何真正的编程语言。在本文中，我们提出了一个系统，生成一个Java优化器从具体的时间逻辑。规范更简单，生成的优化器比以前报告的工作运行更有效。我们实现了一个新的模型检测器的双向CTL（计算树逻辑）称为CTLbd，它在删除自由变量后等效于CTL-FV [9]。模型检测器可以对称地检测未来和过去的时态CTL操作符，而不需要任何转换。 我们还提出一种新的基于双向CTL的规范化语言，可以非常自然地表达典型的优化规则。通过添加重写条件以允许临时变量并考虑诸如异常的真实世界语言特征，系统可以执行Java程序的优化。到目前为止，使用时态逻辑的编译器优化器被认为是不切实际的，因为它消耗太多的时间。然而，使用我们的方法，生成的Java编译器优化器可以编译七个SPECjvm98基准测试，编译时间从4秒到4分钟不等。关键词：编译器优化，时序逻辑，CTL1介绍在编译器设计中，代码优化是最重要的环节之一，它可以提高目标代码的执行速度和空间效率[1]。当前的优化器几乎总是由某种编程语言实现的然而，通过CTL（计算树逻辑）[6]（一种分支时序逻辑）实现优化器的方法近年来引起了人们的兴趣。这种方法有两个主要优点。• 转换更容易编写和原型化。它们可以通过编写几行特定语言而不是数百行1 这篇文章的早期版本出现在JSSST的一次会议上。2 电子邮件地址：fang3@is.titech.ac.jp传真：+81-3-5734-32103 电子邮件地址：sassa@is.titech.ac.jp传真：+81-3-5734-32101571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.09.00750L. 芳，M.Sassa/Electronic Notes in Theoretical Computer Science 190（2007）49的代码。• 变换可以形式化地分析和证明，因为它们的表达更简单用CTL进行的最优化可以简洁地表达许多经典的优化问题通过使用以下指定语言（条件重写规则），其表示如下。I=IJ，如果φ在我们的工作中，我们实际上使用了一种双向CTL，我们称之为CTLbd。CTLbd基于CTL-FV [7]，其中当引入这些时，过去时态算子可以与未来时态算子和自由变量对称地使用。删除自由变量后，CTLbd我们实现了一个直接处理CTLbd的模型检查器。过去的时间操作符与未来的时间操作符对称检查。由于用于转换到μ计算或从PCTL转换到NCTL [10]的过程时间不会产生，并且由于消除了过去的时态运算符，公式不会变得更复杂，因此我们的模型检查器非常有效。在模型检查之前，自由变量4必须被绑定。因此，当条件表达式中有很多自由变量时，处理时间变得不切实际。我们通过实验澄清了这样一个事实，即使用Kripke结构的节点数作为自由变量，如在所有以前的工作[9][2][19]中所做的那样，将大大增加优化时间。因此，形式化的优化应该使用最少的自由变量。我们开发的规范语言并不涉及Kripke结构的节点模型检查器计算的不是特定数量的指令，而是满足相同条件的指令集。因此，描述重写许多指令的复杂重写规则变得非常容易。此外，由于省略了与Kripke结构的节点数对应的自由变量，从而提高了效率到目前为止，由于需要大量的处理时间，具有时序逻辑的优化器被认为是不切实际的。通过添加一些处理现实世界的语言功能，我们得到了几个典型的优化阶段的Java语言编译器，其性能现在接近使用传统算法的优化器。在我们的研究中，七个SPECjvm98基准测试能够在4秒到4分钟的时间内使用上述改进进行优化。此外，我们的规范允许使用临时变量同时转换程序中的几个点，并且可以在现实世界的编译器中使用。因此，我们的优化器可以使用CTL执行以前工作中没有执行的几个优化[9] [2][19]。我们认为我们的实现是第一个具有时态逻辑的现实Java编译器优化器。此外，对现有问题的见解，以及缩短优化时间的技术和其规范4自由变量表示逻辑公式的自由变量。 参见第6节。 他们不应该 与程序中的变量混淆。L. 芳，M.Sassa/Electronic Notes in Theoretical Computer Science 190（2007）4951E2 1 0i i≥0被收购。2CTLbdCTLbd是一种时态逻辑，其中过去时态运算符与未来时态运算符对称地引入。←−←−CTLbd具有过去时间运算符A和E以及通常的量化器A和E，通过颠倒A和E而得到。CTL bd公式是状态公式φ或路径公式φ，由以下语法生成，其中非终结符φ和φ，终结符true，false和pred（x1，.，xn）∈Pred，起始符号φ，以及以下结果。语法CTLbd的语法是：φ：：=真|虚假|预测值（x1，...，x n）| φ ∧ φ |φ ∨ φ |¬ φ←−←−| E| A.|E|A .φ：：= Xφ| φU φ标准缩写，例如， Fφ=真U φ、Gφ=真F<$φ和φ1Rφ2φ（<$φ1U<$φ2）也成立语义在Kripke结构上给出了CTLbdKripke结构K是三元组（S，R，L）。S是一组状态，R→S×S是转换关系，L：S→2Pred是一个函数，它将每个状态映射到一组对该状态为真的谓词。在K中从s 0开始的路径是状态的无限序列π =（s0，s1，. . ），使得∈i≥0：（si，si+1）∈R.从s0开始的反向路径是一个序列，（si+1，si）∈R.K，s |= φ表示逻辑公式φ的值在Kripke结构K中的状态s中为真。K可以省略，如果它是显而易见的。关系|=定义如下。国家公式：S| = true i trueS| = false i falseS| = pred（x1，x2，.，xn）i_pred（x1，x2，.，xn）∈L（s）s| =<$φ i not s| = φS|= φ1φ2i s |= φ1和s |= φ2s| =φ1φ2i s| = φ1或s| = φ2S| = E i路径（s=s0→s1→s2. . ）：（s i）i≥0|= 100|=一条路径（s=s0→s1→s2.. . ）：（s i）i≥0|=←−s|=ipat h（.. . s→s →s=s。 . . ）：（s）|=←−S|=一条路径（. s2→ s1→ s0= s.. . ）：（s i）i≥0|=52L. 芳，M.Sassa/Electronic Notes in Theoretical Computer Science 190（2007）49路径公式：（s i）i≥0|= Xφ i s1|= φ（s i）i≥0|= φ1U φ2ik ≥ [s k|= φ2i：[0 ≤ i

下载后可阅读完整内容，剩余1页未读，立即下载