优化验证及其在Java虚拟机语言中的应用

理论计算机科学电子笔记176（2007）37-59www.elsevier.com/locate/entcs优化验证大卫阿斯皮纳尔1英国爱丁堡大学信息学院LFCSLennart Beringer2InstitutfurInforrmatik，Ludwig-MaXimilians- UniversitaütMuénchen，GermanyyAlberto Momigliano3英国爱丁堡大学信息学院LFCS和意大利摘要我们引入优化验证的想法，这是正式建立一个优化转换的实例确实提高了一些资源措施。这与翻译验证有关，但与之相反，翻译验证旨在建立由优化编译器进行的转换的特定实例是语义保留的。我们的主要设置是程序逻辑，Java字节码的一个子集，对于资源注释的操作语义来说，它是可靠和完整的。 后者采用资源代数来衡量动态成本，如时间，空间和更详细的例子。我们描述了优化验证的例子，我们已经在Isabelle/HOL中使用逻辑进行了正式验证。我们还介绍了一个类型和测试系统，用于测量静态成本，如代码大小，这是证明符合操作语义。关键词：编译器优化，翻译验证，程序逻辑，Java虚拟机语言，成本建模，资源代数，轻量级验证。1引言我们感兴趣的是验证Java平台上移动代码的资源使用。在以前的工作[3，1，6]中，我们已经描述了一个证明携带代码基础设施，它可以实现内存使用。一个类文件伴随着一个证明，它描述了程序的主方法的资源使用情况1电子邮件：da@inf.ed.ac.uk。2 电子邮件：beringer@tcs.ifi.lmu.de。3 电子邮件：amomigl1@inf.ed.ac.uk。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.06.01738D. Aspinall等人/理论计算机科学电子笔记176（2007）37我们使用一个程序逻辑，带有形式为De：{P}的判断，声明表达式e满足断言P。例如Demain：{r=F（h）}其中h是程序的起始堆（特别是包含main方法的参数），r是程序的内存消耗，表示为h中参数大小的函数。在本文中，我们研究了这个框架的一个重要扩展和一个特定的应用。首先，我们概括了资源的形式，以便以统一的方式涵盖更广泛的概念。其次，我们考虑资源的排序，这使我们能够讨论优化验证，在这个意义上，我们可以建立一个程序消耗的资源比另一个少。这被证明是编译器社区感兴趣的，在给定可用资源的情况下，在当前上下文中，已经投入了大量的然而，这可能是有问题的：“[. . .当前的优化策略并不总是实现性能目标。事实上，众所周知，优化在某些情况下可能会降低性能。困难在于，目前的技术并不能总是确定何时应用优化是有益的还是有害的。[三十一]这就是优化验证的用武之地：从技术上讲，它受到翻译验证思想的启发[23]，这是对翻译器和编译器进行大规模验证的替代方案在这种方法中，我们构建了一种验证机制，在每次运行编译器之后，该机制正式确认在该次运行中产生的目标代码是源代码的正确翻译。“[. . . ]同样的结果，而（希望）在更少的时间或空间或消耗更少的功率执行。”[24日](our强调）。在这里，优化验证将资源使用的改进作为主要动机，因此，应该检查什么这适用于诸如在携带证明的代码中考虑的安全策略之类的场景，其中资源使用甚至可能比正确性更重要，因为它包含域的安全需求。1.1优化的概念要考虑验证优化，我们必须首先定义在我们的环境中优化的含义。我们假设一个程序是一个类的集合，其中一个类包含一个指定的main方法。动态优化的一个简单概念是指该方法的每次终止执行。设P1为优化前的程序，P2为优化后的程序：P1−→P2D. Aspinall等人/理论计算机科学电子笔记176（2007）3739我们只需要考虑每个程序中主方法的主体的成本，e1−→e2其他方法的变化可能是优化的，中性的，甚至是非优化的;在这一点上，我们不研究嵌套程序上下文中的优化。为了被认为是一种优化，我们希望确定转换相对于成本模型正在改进。我们用资源代数R的概念来捕捉后者，它包含用于测量执行每种指令的成本的组件，以及对这些成本的排序。动态（Dynamic）成本可能取决于程序的输入，它是通过程序的执行来衡量的。一个使用R进行计算的操作语义。如果对于所有输入堆，e1和e2都收敛，那么e2的资源消耗应该比e1有所改善：he1r1h其中排序≤是指从R开始的排序。我们可以假设，不失一般性，main参数的输入指针在每次执行时都是固定的。1.2优化序列。以上定义了我们的单步优化概念对于顺序的几个优化，考虑感兴趣的资源代数R的初始和最终程序之间的优化就足够了。然而，我们经常想把一系列优化分解成几个单独优化的变换然后，我们可以证明存在一系列优化步骤：P1−→P2 −→···−→Pn其中每个Pi−→Pi+1是对某个特定资源代数R i的优化。此外，优化中的每一步对于目标成本模型R都应该是非增加的。一个适当的优化序列至少有一个步骤，R中的成本严格地从某个Pi减少到Pi+1。1.3通过程序逻辑验证优化。为了陈述和证明（动态）成本优化，我们使用了一个程序逻辑，该程序逻辑提供了关于约束所消耗资源的函数的断言。我们必须找到以下形式的断言：ST1De1：{F1（h）≤r}ST2De2：{r≤F2（h）}其中，指定表STi将断言与每个方法和循环相关联在程序中，提供适当的不变量。断言声明执行P1时消耗的资源由输入堆的某个函数F1从下到上限定，P2消耗的资源由下到上限定40D. Aspinall等人/理论计算机科学电子笔记176（2007）37上面的函数F2。为了证明P2是P1的优化，我们现在必须证明：好吧F2（h）≤ F1（h）（特别地，这在F1= F2的情况下平凡地成立）。1.4静态优化。静态成本（如代码大小）通常用作优化的指标，而一些动态成本可以通过静态测量有效地近似。我们通过引入静态资源代数S的概念来涵盖这两种可能性。为了度量静态成本，我们使用了一个带有效果的类型系统。对于两个函数体e1和e2，我们必须找到一个类型t，并且它们分别对应于s1和s2，使得：我的世界第一季第1集 ：t，s1 rmain ：t，s2其中，main的主体的类型上下文的格式为args：String[]，P1和P2分别是程序P1和P2的资源类型签名，见第5节.为了使P2是P1的静态优化，我们应该建立：s2≤s1，其中排序≤现在指的是静态成本上的排序。 一个理想的优化概念是w.r.t.。一对（R，S）目标动态和静态成本模型;一系列优化可以适当地交替动态和静态降低。一个典型的例子是使用时间和代码大小来验证优化，如循环展开，见4.1节。为了简化说明，我们单独考虑成本本文的组织结构如下。节中2.给出了语言的动态语义在第3节中，我们提出了一个程序逻辑，它将[1]中提出的逻辑推广到任意资源代数。节4给出了优化验证示例，包括标准编译器优化步骤、尾调用优化和应用程序规范。第5节审查静态系统，第6节最后总结和讨论相关工作。2资源注释操作语义我们使用一种称为Grail的Java字节码的函数形式[7]，尽管这种方法适用于其他具有结构化操作语义的语言。Grail保留了JVML的对象和方法结构，但将方法体表示为相互尾递归的一阶函数集。该语言是由值v、参数a和函数体表达式e构建的（在本文中，我们不D. Aspinall等人/理论计算机科学电子笔记176（2007）3741...提到静态字段和虚拟调用，这在别处有说明[1]）：v：：=（）|LC|我|空Ca：：= v|Xe：：= a|阿格拉a|新的C|十.f| x.f：=a|e; e|设x=ein e|如果e那么eelsee|称g|C.m（a）在这里，C在Java类名称上，f在字段名称上，m在方法名称上，x在变量（方法参数和局部变量）上，g在函数名称上（对应于字节码中的指令地址值由整数常量i、类型化位置lC、类型unit的唯一元素（）和空引用组成def def零角在JVML中，布尔值bool被定义为true= 1，false= 0。Grail的（不纯的）按值调用功能语义与将其直接翻译为JVML的命令式解释相一致，只要满足某些句法条件。特别是，函数调用中的实际参数必须与函数定义的形式参数一致。图1和图2中显示了Grail程序的Isabelle格式和编译器的具体语法。3 .第三章。为了模拟计算资源的消耗，我们的语义注释与资源计数机制的基础上资源代数。定义2.1资源代数R是偏序幺半群（R，0，+，≤），即（R，0，+）是幺半群，（R，≤）是偏序集，其中(i) 0是最小元素：0 ≤x;(ii)+是两边的顺序保持： x≤y使得x+z≤y+z，z + x≤z + y。此外，对于每个表达式形式，R在R中具有常数：Rint，Rnull，Rvar，R，Rnew，Rgetf，Rputf，Rcomp，Rlet，Rif，Rcall和单调算子Rmeth：R → R.C C，m，v每个常量表示与指令相关联的成本，然后通过monoidal操作组成。 操作员Rmeth计算成本方法调用。对于某些应用程序，我们可能会使用额外的语法来参数化常量，例如，如果我们正在跟踪某些变量的读/写或对不同选择的函数调用和/或原语操作进行收费。对于这里考虑的所有资源代数，复合都是可交换的;然而，对于不是可交换的例子，规则中的操作顺序很重要，并且与求值顺序相匹配。在这样的代数上的一个有用的运算是乘积，我们简单地将其指定为monoidal积;对于R=（R，0，+，≤）和RJ=（RJ，0J，+J，≤J），定义R×RJ为（R×RJ，<$0，0J<$，<$，≤ <$），其中：(i)RJ=r1，rj=r2，RJ=r1+r2，RJ+jrj=R2;1 2 1 242D. Aspinall等人/理论计算机科学电子笔记176（2007）37(ii) ≤ Rj是R × RJ上满足定义2.1中条件的任意偏序。这使我们能够组成各种资源代数，而无需承诺由偏序集的乘积引起的排序。例如，我们可能希望将R× RJ上的排序设为字典序或同时排序，参见例如第16页介绍的乘积代数。 相反，我们可以定义投影πi（Rn）的乘积。操作语义学定义了一个判断埃什，埃什，杰，弗，河它将表达式e与环境E（从变量到值的映射）、初始堆和最终堆h、hJ、结果值v和成本r∈R联系起来。堆是从位置l到对象的部分映射，其中对象表示为类名C和字段表（从字段名f到值v的映射）。我们对堆使用以下符号：h（l）l处对象的类名;h（l）.f在l处的对象中查找f处的值的场;h[l.f<$→v] f用l处的v更新f的场。环境E中的参数求值定义为evalE（x）=E（x），evalE（v）=v，而成本定义为• cost（）=cost（lC）=0;• cost（nullC）=Rnull;• inti= inti;• cost（x）=Rvar.函数fields（C）返回类C中的场序列f，而initvalfi表示场f i的初始值。对于函数和方法，我们写bodyg和bodyC，m分别代表g和C.m的定义。操作语义规则的完整列表如下：a lCEh，a h，evalE（a），cost（a）Eh， a h，va，raE h，a j h，vJ，rJ一一Eh，aaJh，（va，vJ），ra+rJ+Ra al=freshloc（h）场（C）=fEh，newCh[l.fi<$→ initvalf]，l，RnewICD. Aspinall等人/理论计算机科学电子笔记176（2007）3743C、M、VEh，x l，h，rxEh，x.f h，h（l）.f，rx+RgetfEh，x l，h，rxEh，a v，h，raEh，x.f：=ah[l.f<$→v]，（），rx+ra+RputfEh，e1h1，（），r1 Eh1，e2h2，v，r2Eh，e1;e2h2，v，r1+Rcomp+r2Eh，e1h1，v1，r1Ex：=v1h1，e2h2，v，r2Eh，letx=e1ine2h2，v，r1+Rlet+r2Eh，ehJ，1，reE hJ，e1hJJ，v，rEh，ifethene1elsee2hJJ，v，re+Rif+rEh，ehJ，0，reE hJ，e2hJJ，v，rEh，ifethene1elsee2hJJ，v，re+Rif+rEh，bodyghJ，v，rEh，callghJ，v，Rcall+revalE（a）=v x：=v h，bodyC，mhJ，v，rEh，C.m（a）hJ，v，cost（a）+Rmeth（r）2.1资源代数示例表1中示出了一些示例资源代数。时间代数模拟了一个近似执行时间的指令计数器;每个Grail表达式形式都根据它扩展到的JVM指令的数量收费4。堆代数计算在执行期间消耗的堆空间大小（忽略垃圾收集的可能性，这对于任意JVM都不能假设）。只有新指令才消耗堆。Frames代数计算执行过程中堆栈上的最大帧数。MethCnts代数通过累积被调用方法名的多个集合来跟踪调用。[4] if指令的成本为零，因为它们被编译为测试和分支;同样，在这些示例代数中，顺序组合的成本为零。44D. Aspinall等人/理论计算机科学电子笔记176（2007）37C、M、V时间堆帧MethCnts MethFreqIdMethGuard|R|NNNMS（Id）N × N{tt，}RintRnullR varRRnewCRgetfRputfRcompRletRifR callR-甲基（r）C、M、V11113230101|v|+2+ r0000尺寸（C）000000R00000000000R+ 1中文（简体）中文（简体）中文（简体）中文（简体）中文（简体）中文（简体）中文（简体）中文（简体）中文（简体）中文（简体）中文（简体）r+{C. m}FreqC. m，|v|（r）TTTTTTTTTTTTTTTTTTTTGC，m（v）0R+R≤R0+≤0+≤0Max≤中文（简体）++Freq+≤频率TT∧≤保护Thenotation|v|表示第1行的长 度 。 . v; 对于这种情况，将子图+和子图+分别作为集合和子集。对于频率，我们定义FreqId，n（t，p）=（0，max（t，p））和FreqC.m，n（t，p）=（n + 2 + t，p），其中C.m/=Id。在这种情况下，合成是（t，p）+Freq（tJ，pJ）=（t + tJ，max（p，pJ）），并且排序（t，p）≤Freq（tJ，pJ）当且仅当p ≤ pJ。 对于守卫，若f b = t to r b = bj = n，则GC，m（v）是对每个C，m和b≤GuardbJ的布尔值函数.表1示例资源代数MethFreqId代数通过累加连续调用之间的最大周期来计算对方法Id（长标识符C.m）的调用频率的度量;这是应用特定代数的一个例子（参见4.3节的激励示例）。最后，MethGuard代数不计算定量资源，而是维护一个布尔监视器，用于检查在调用类C中的方法m时是否满足任意守卫GC，m（v）。如果防护被认为是资源可用性的先决条件（例如，检查方法参数是否在某些限制内），那么我们可以将优化视为确保资源先决条件始终得到满足的转换。在最后一种情况下，资源操作符Rmeth取决于运行时值vi，而在其他例子中，它是固定的一般来说，像这样依赖于运行时值的资源代数可以沿着计算路径收集跟踪。最终的单词可能会受到进一步的策略的约束，例如安全自动机[27]或线性结构上的逻辑公式。这些可以用我们的程序D. Aspinall等人/理论计算机科学电子笔记176（2007）3745逻辑的高阶断言语言编码，下面将介绍。3资源感知程序逻辑我们优化验证的主要基础是Grail的通用程序逻辑，其中断言是操作语义中出现的所有语义组件（即输入环境E和初始堆h）上的布尔函数，46D. Aspinall等人/理论计算机科学电子笔记176（2007）37CC，m，eval（a）E后堆hJ、结果值v和消耗的资源r。 断言P因此属于E ×H×H×V ×R →BOOL类型。 GDe：P的判断该逻辑将圣杯表达式e与断言P相关联，依赖于上下文G={（e1，P1），.，{en，Pn）}，它存储递归程序结构的假设，这是Hoare最初的过程证明规则的精神[ 17 ]。程序逻辑包括每个表达式形式的一个规则，一个公理和一个后果规则，其中我们使用以下语法约定：• 方括号符号P[E，h，h，J，v，r]表示谓词P的实例化;• 对于公式Φ，如果有一个隐式泛量化变量x的出现，记法G D e：{ Φ（x）}表示GDe：λx。Φ （x）。（e，P）∈GGQe：PGQe：PP−→QGQe：QGQa：{hJ=hv=evalE（a）r=cost（a）}GQa1a2：{hJ=hv=（evalE（a1），evalE（a2））r=cost（a1）+cost（a2）+R}GQnewC：{v=freshloc（h）}hJ=h[v. fi<$→ initvalfi]r=Rnew}GQx.f：{h=hJ（l.E（x）=lv=h（l）.f）r=cost（x）+Rgetf}GQ x.f：= a：{（？ E（x）= l <$hJ= h[l.f <$→ eval E（a）]）<$v =（）<$r=cost（x）+cost（a）+Rputf}GQe1：P1G Qe2：P2GQe1;e2：{\displaystyle {\mathbb {1}r 1}r2}。P1[E，h，h1，（），r1]<$P2[E，h1，hJ，v，r2]<$r=r1+Rcomp+r2}GQe1：P1G Qe2：P2GQl etx=e1ine2：{\displaystyle {\mathbb {v}h1v1，r1r2}。P1[E，h，h1，v1，r1]P2[E[x：=v1]，h1，hJ，v，r2]r=r1+Rlet+r2}GQe1：P1G Qe2：P2G Qe3：P3如果e1，则ne2else3：{\displaystyle {\mathbb {v}1 r}1r} 2。P1[E，h，h1，v1，r1]（v1=1=P2[E，h1，hJ，v，r2]）（v1=0=P3[E，h1，hJ，v，r2]）<$r=r1+Rif+r2}G<${（callg，P）}Qbodyg：P[E，h，hJ，v，Rcall+r]GQ调用g：P[E，h，hJ，v，r]G∈ {（C.m（a），P）}Q体C，m：P[x：=evalE（a），h，hJ，v，Rmeth（r）]GQC.m（a）：P[E，h，hJ，v，r]D. Aspinall等人/理论计算机科学电子笔记176（2007）3747在演示如何使用程序逻辑来验证程序的资源消耗之前，我们总结了一些基本的元理论性质。这些已经通过在证明助手Isabelle/HOL中表示操作语义和程序逻辑得到了正式证明;有关更多细节，请参见[1，2];这里的首先，语义有效性，它有一个部分正确性解释：定义3.1断言P对表达式e有效，|= e：P，如果对于所有E，h，hJ，v和r，E h，ehJ，v，r意味着断言P [E，h，hJ，v，r]成立。上下文G是有效的，|= G，如果对于G中的所有对（e，P），|= e：P.断言P在上下文G中对e有效，如果|= G意味着|= e：P.事实上，证明系统在操作语义方面是合理的：定理3.2（可靠性）如果GDe：P然后G| = e：P.定理3.2的证明通过在推导的高度上的归纳进行，使用适当相对化的（上下文）有效性概念。考虑到所采用的部分正确性解释，很明显，非终止程序空洞地满足它们的规范。为了验证这些程序的资源消耗，开发了辅助终止逻辑[2]。逻辑完备性的处理，以及实际的证明方法，得益于一些关于证明上下文的可接受规则。除了通常的弱化规则之外，其他规则允许人们解除证明上下文，即在没有上下文假设的情况这使用了一个规范表ST，它将函数和方法调用映射到断言中。 我们说一个背景G遵守规范表ST，符号ST| = G，如果其中的所有条目都由函数或方法调用及其在表中的断言组成;而且它们的物体满足相应的断言。见[2]，见[3]，见[4]。St|= G（e，P）∈ GDe：P（SPECTABLE）St|= G（C.m（a），ST（C，m，a））∈ GDC.m（b）：ST（C，m，b）（ADAPT）SPECTABLE规则使用specification表来解释程序片段的验证（可能是相互递归的），而ADAPT可以用来在提取方法specifications时调整实际参数。为了证明相对完备性，我们定义了一个上下文Gstrong，它与每个函数和方法相关联，调用它的最强规范。48D. Aspinall等人/理论计算机科学电子笔记176（2007）37定义3.3e的最强规格为：SSpec（e）{Eh，ehJ，v，r}引理3.4对任意e，G强De：SSpec（e）.此外，G 强满足ST 强|= Gstrong，其中STstrong是由（λg.SSpec（call g），λCma. SSpec（C.m（a）。由此，我们得到：定理3.5（完备性）对任意e和P，|= e：P蕴含De：P。完整性结果意味着我们可以根据程序的结构，使用程序逻辑的规则来推导出任何可证明的4经过验证的优化上一节中介绍的程序逻辑可以用来证明程序转换在优化编译器[20]中的常规应用，只要它们确实在改进。在本节中，我们将给出一些优化示例，并概述其验证的证明。虽然我们在本文中考虑的转换和示例相当简单，但它们用于演示我们的方法。4.1标准低级优化我们首先考虑的是[24]的激励计划i- 0; x- 1; y-2;WHILE i 24 DO {i- i + x + y ; g- 2* i}退出我们的正式验证是指将此代码翻译为我们的语言（的Isabelle表示）。这种（手动）转换的结果是方法R。计算0：方法static int R. calc0（）=leti=0in letx =1in lety =2in letg =0in callffunf（inti，intx，inty，intg）=ifi 24thencallhevarginti，intx，inty，intg，intn=1letj=i+xin leti=j+yin letg=2<$iin callf它与原始代码只有很小的不同：我们通过对变量g的赋值扩展了循环序言，将循环转换为两个表示基本块的函数，并将EXIT语句转换为g的最终值的返回语句。D. Aspinall等人/理论计算机科学电子笔记176（2007）3749⎢⎥F⎦使用前面定义的资源代数时间，我们现在概述判断的Isabelle证明DR. 计算0（[]）：{r= 213}（1）这说明调用R。calc0需要213个时间单位我们首先定义两个辅助（语义）函数costf（n）= 24n+ 10costh（n）= 24<$n +1它们分别描述了对函数f和h求值的成本，其中n是循环迭代的次数。接下来，我们为calc0及其局部函数f和h定义一个规范表ST0。⎡ ⎤你好calc0<$→ {r=11+costf（8）}电话呼叫f⎢⎢⎢⎢⎢紧急呼叫⎣{\fn黑体\fs22\bord1\shad0\3aHBE\4aH00\fscx67\fscy66\2cHFFFFFF\3cH808080} （E（x）=1<$E（y）=2<$E（i）=3<$J<$J≤8）−→<$⎥⎥r=cost（8−J）}⎥⎥{\fn黑体\fs22\bord1\shad0\3aHBE\4aH00\fscx67\fscy66\2cHFFFFFF\3cH808080} （E（x）=1<$E（y）=2<$E（i）=3<$J<$J≤7）−→

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