前瞻- 编译器的bug就不能少点？

读PLDI 04 Best Paper Award 《Automatically Proving the Correctness of Compiler Optimizations》
By Sorin Lerner.Todd Millstein and Craig Chambers in Washington U

本博自从接触编译器到现在,几乎都每天都能听到bug这个关键字,编译器中的bug很痛苦,首先,人写的程序很复杂,编译器设计者很难想出所有的情况并一并处理之;其次,编译器的bug很难调,要先排除程序本身的错,接着需要知道到底是分析时出错还是变换时出错;还有这些错都是在怎样的分析和变换中出了错;最后还要担心错误会不会越不越多,没有对编译器整体的理解,很难给编译器打上正确的补丁,从而有可能这个例子补对了,其他又错了一片.
作者在文章里就编译优化正确性的自动证明做了一些尝试,这些尝试在读完文章之后觉得很了不起,只是这里面提到的工作做下来,也是需要很大的积累和投入.作者的尝试我概括如下:将优化分为转换和具体优化两个部分.代码的转换是所有优化都要做的,而并非所有的转换都是优化,所以作者通过增加利益驱动模块来判断某个转换是否是优化,这样优化的自动证明问题,就变成了某个转换正确性的自动证明问题;正确性的定义:转换前后的语义保持不变.接着作者按照转换依据的信息来自转换语句之前还是之后,将转换分成两种模式,即前向转换模式和后向转换模式.然后分别对这两种模式进行讨论,而自动证明也分别针对这两种模式来论述.
不管是前向还是后向,作者都将信息收集部分定义为多个连续语句构成的区间,然后指出某个变换在这个区间内语义不会发生变化.于是作者就使用自动机理论,证明从区间的开始处到结束处语义保持不变,为了证明这一点,作者将将优化从区间开始处到结束处的每个单步看成一种状态,于是语义在区间内不变就演变成在区间内每个状态转移的过程中不变.此外还需要证明基于区间语义不变所做的转换语义也不变.此外作者还实现了纯分析的正确性证明,仅仅比转换少了最后一步转换的证明而已.整个证明过程需要人工的输入一些已正确的定理
这篇文章,其中的局限在于仅能实现单个语句转换类型的优化,且仅能用在过程内优化,作者在文章中以常数传播,死赋值删除为例分别讲解了前向转换模式和后向转换模式.这些都相对简单一些.优点在于能高效的辅助编译器设计者开发正确的编译优化,作者在文中也提到自己在实现优化时,采用自己的自动证明器发现bug的经历,让本博好生佩服了一下.

PS:

1. 这是2004年PLDI的Best Paper Award,根据google学术搜索结果,共被引用109次,这是作者在实现一个真正的编译器时所做的工作,可谓是心血的结晶.完成这样一篇文章,要了解编译器,要写的出编译优化的简单算法,要懂自动机理论,要能将问题抽象,分类处理,很不容易.让我们记住这几个人Sorin Lerner,Todd Millstein,Craig Chambers
2. 阅读这篇文章，尤其是刚开始时，有点晕乎，一直很想理解作者是怎么做到的。看到了最后作者居然一句话带过，说利用自动机规约理论，将使能语句和无害语句分别作为输入。。。。。。.看来自己对于自动机理论了解的太少了，数学学不好看来是不行的。
3. 可信一直都是一个很头疼的问题，计算机不像数学，很多都没有完备的理论证明，几乎大量的可靠都是建立在各种测试和验证上，即给定输入，对比输出。所以如何做到万无一失一直是个大问题，尤其在安全领域。NASA在编译时都不使用任何的优化，全都靠程序员的编程效率来保证性能。这篇文章尝试了一种新的思路，通过特定的中间语言表示加上少量的人工定理输入，就能使用自动机证明简单的优化。
4. 下一篇文章预告《LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation》 CGO2004 by Chris Lattner,ViKram Adve.这篇文章虽然是有点老，而且是CGO的文章，但是综合的介绍了LLVM这个目前炙手可热的编译器，被引用次数达到302次。所以本博打算详细的读一读，消化一下，顺便了解了解LLVM。。。

下面是我的阅读笔记:

• 摘要：

文章描述了一种自动证明编译器优化可靠的技术，作者对可靠的定义是：所有用于优化的转换都能保证语义不变。为此，作者先设置了一个特殊语言Cobalt，这种语言包含非结构化的控制流，本地变量指针，动态存储分配和递归进程调用等特性。Cobalt在类C语言的中间表示上做优化。之后，作者就给出了自动证明的方法，这种方法使用自动机理论证明器，需要每个优化给出优化特征的原理.
作者针对Cobalt实现了一些前向和后向的过程内数据流优化，包括常数传播和展开，分支展开，完全和部分冗余删除，完全和部分死赋值删除和简单的指向分析，之后实现了可靠性检测机制，并使用它自动证明了优化的正确性。这个检测器在开发优化代码的过程中发现了很多诡秘的bug。作者也将成果用在了Whirlwind的编译器架构中。

我的问题：使用自动机的理论也就是说要有状态到转换，状态转换是通过Cobalt定义的吗？为什么作者没有验证过程间优化？为什么只提到了过程内的前向和后向数据流优化，还有其他的数据流优化吗？除了数据流还有其他的优化吗？

• 引言：

首先说编译器的错误程序员很难检测和更正，原因有三：编译器错误很难发现，通常在运行编译器输出的程序时才能发现；通常只在很特定的形势下才错，一般程序不错；一旦发现错很难决定是编译器错或者输入程序错。(还有一个原因，对于优化多的编译器，如何修改也是个问题，牵一发有可能动全局)
然后，介绍目前在增加编译器可靠性方面的研究情况，有三种途径：通过编译大量程序并验证优化后的程序运行是否正确来保证，这样不能保证所有情况都正确，且测试集很难完备；在这种测试集中加入转换验证和可信编译来保证优化前后语义完全等价，能改进前一种机制，但开销很大且可能存在验证的完备性问题，若不能通过验证，程序员可能无所适从；证明编译优化本身的正确性貌似是较好的方式，现在有些优化能通过手工的方式得到证明，但手工证明工作量太大，而且这些正些证明通常是在提出优化的论文里做的，所以若使用论文中的算法实现优化还是可能会有bug。
于是，作者的方法就诞生了，将可信编译和证明联系起来，采用自动的方式能一次性证明针对所有输入，优化的正确性。作者使用一种特定的语言来实现优化，并自动证明的。作者的贡献有六点：一，提出了一种语言，Cobalt，使用这种类C语言的中间表示定义了优化。实现优化时，用户可以定义一个复写规则和一个输入程序控制流图节点上用于开启优化的条件，另外，Cobalt也能用来做纯分析。用Cobalt写的优化和分析能通过一个特殊的数据流分析引擎直接执行；二，作者使用Cobalt实现了一些过程内前向和后向数据流优化以及指针分析；三，作者提出了一中自动证明使用Cobalt语言实现的优化和分析正确性的策略,这种策略使用自动机理论；四,作者将该策略使用Java语言中的Simplity实现为一个检测器，该转换器能将程序的语义简化为作者的中间表示语言；五，作者使用这一检测器自动证明了所有优化和分析的正确性，并发现了在实现优化和分析中的一些隐秘错误；六，作者将该技术用在了Whirlwind中。
作者想通过提供编译优化正确性可靠性依据，实现一个可扩展编译器的基础，这种编译器可以让用户在它特定领域的应用中增加它们独特的优化，并且该编译器能验证正确性找出bug。

我的问题：目前所做的很多优化，我们都尝试去保证它的语义正确性，也去证明了，那么真的不用注意特殊情况了吗？作者的实现真的就能针对完全的语言标准来做吗?Cobalt语言这么神奇能描述好过程内优化并将它们作为证明的依据？已经忍不住想一窥究竟了！！

• 相关工作：

关于Cobalt语言，作者时集成Lacey的思想，扩展Lacey的语言，使其增加指针，动态存储分配和过程概念，更像C，并用它描述基于带标记CFG的优化程序复写引导规则。并且相对于Lacey，能给出更精确的优化制导，而且支持纯分析。在手工证明优化正确性方面，有些人已经做了一些证明工作，但都不是自动的。在可信编译和转换验证方面，基本都是使用某个输入给编译器，看编译器结果，若错，就改。这样的话，输入无法包含所有情况，证明并不普适。还有一些其他的机制，证据携带代码，可信编译，类型化的中间语言，类型化的汇编语言等等都已经被用来证明编译器的可靠性，但是这种证明仅仅用于保证类型和存储安全，而作者的工作号称能确保证明从语义上保持不变。

我的问题：很多都没有读懂，临时逻辑怎么用来表达数据流分析？手工证明的话要参考编程语言标准吗？

• 概述：

简要介绍Cobalt和证明优化可靠的技术。首先,将优化所用的转换及匹配模式分成前向传输模式和后向传输模式两种,之后介绍了利益驱动机制,这种机制用来验证一个优化转换是否真能提高性能,若不能,就不需要再做对应的代码转换.最后介绍了纯分析,只提及了纯前向分析,之所以做纯分析是为了为其他的前向转换提供更多的信息.下面分别介绍之:
1,前向转换模式
作者引入了一个待匹配的模式: C1 followed by C2 until s =>s’ with witness P
这个模式的意义:s能转换为s’,若在CFG中,从过程的开始到s的所有路径上,存在一个满足C1的语句,接着有0或多个满足C2的语句,并有s紧随其后.则s就可转换为s’.作者将C1称为使能语句,C1和C2之间的称为无害语句,P称为证人.这样C1就能检测到使语句可用的属性,C2检测到无害语句,P则代表建立在使能语句基础上允许语句安全转换的条件.例如对于常数传播优化,可以做如下抽象
stmt(Y:=C) followed by ~mayDef(Y) until X:=Y =>X:= C with witness n(Y)=C
意思:若有Y:=C的语句,且接下来没有任何可能的对Y的定义,直到X:=Y,则,将C直接传播为X并令C1和C2之间的证人,定义为Y=C恒成立.
对于转换可靠性定义为语义保持不变.而对于前向转换模式,这显然是成立的,因为C1和C2之间的区域转换的条件正是证人P的内容.也就是说在满足P的情况下,s才能转换为s’.这显然能够保持语义的一致性.
2,后向转换模式
和前向模式相似,除了分析方向方向相反,定义如下:
C1 preceded by C2 since s => s’ with witness P。即，s可以转换为s’,若在CFG的所有从s到过程技术到路径上，存在满足C1的语句，在它之前存在一个或多个满足C2的语句，且在它之前为s。C1和C2之间的成为无害语句，即见证区间。P成为后向证人。以死赋值删除为例:
(stmt(X:=…)OR stmt(return…)) AND ~mayUse(X) preceded by ~mayUse(X) since X:=E =>skip with witness n-old/X=n-new/X
具体含义：自X:=E之后没有任何mayUse(X)直到有新的对X的赋值或过程返回，则可以删除此赋值，并令最开始赋值之后的n-old/X定于删除赋值之后的n-new/X作为证人。
后向转换与前向转换很大到不同在于见证区间在实施转换的语句之后而非之前，因此，后向转换的证人需要保证n-old/X和n-new/X都严格对应相应的语句，
3,利益驱动
这部分区别程序优化和普通的程序转换。优化需要程序转换的结构能减少运行时间，只有优化才有证明的价值，普通的转换若无优化效果，不需要证明.为了区分这两者,作者在实际中,优化被写成两部分,一部分只定义转换合法性,另一部分单独的描述哪种情况下的转换能提升性能，该部分成为利益驱动部分。这部分通过一个choose函数表达。该函数输入为通过转换模式判断出的所有合法转换集合和待优化的过程，输出为能够得到优化效果的转换集合。可以使用下面的表达式表示该集合：
O-pat filtered through choose。
作者认为采用将实际优化分成转换模式和利益驱动两部分很关键，因为转换模式往往很简单而优化获利的判定则比较复杂。对于前面提到的常数传播和死赋值删除，choss函数将返回所有输入，因为优化效果很显然。对于获利驱动，若没有精确给出，则会默认它获利。接下来作者以部分冗余删除为例，介绍利益驱动。
4,纯分析
为了更复杂的优化，Cobalt允许用户编写纯分析规则，这些分析能用用于计算和验证某个过程内的某些属性或为随后的转换提供信息。纯分析将定义一个新的标号，分析的结果就是给定CFG中的一个标号。下面就是一个前向分析的例子，和前向转换相比只少了复写部分：
C1 followed by C2 defines label with witness P。
新定义的label就能插入在满足前向条件的地方。若某个语句s被标记，就意味着它在s执行之前满足证人P。下面作者举例说明纯分析如何实现简单到指针分析。
stmt(decl X) followed by ~stmt(….:=&X) defines notTainted(X) with witness notPointedTo(X,n).
这个纯分析定义notTainted标号。若一个变量的地址可能在某个语句之前被取值，则我们成为该变量在该语句处被污染(Tainted).
于是上面两个转换模式中提到的mayDef(Y)就能使用纯分析定义如下：
case currStmt of
*X:Z , then ~notTainted(Y)
X:=P(Z), then X=Y OR ~notTainted(Y)
else syntacticDef(Y)
endcase
另外，作者还提到目前仅在工作中用到了前向纯分析，且将该纯分析仅用在前向优化中。仅做前向纯分析是因为目前还没遇到需要后向纯分析的情况，且和前向很类似，没必要做。仅用在前向优化是因为用在后向优化可能导致纯分析干扰结果.

我的问题:作者在这部分非形式化地描述了自己的工作.介绍了三中Cobalt语言的用途:前向模式转换,后向模式转换和纯分析;同时还对一些细节做了说明,如将合法转换模式和优化的概念分开,简化自动证明工作。但究竟如何实现证明自动化还是没说，看来还得接着往后看。不过根据这些概念，倒是对编译优化有了更直观的认识，无非时两个方向的信息传播和沿什么方向做传播的问题。

• COBALT语言：

这部分对Cobalt语言做形式化的描述
1，中间语言：
Cobalt语言可以分解成以下部分:
Progs pi ::= pr … pr
procs pr ::= p(x){s;….;s;}
stmts s ::=decl x | skip | lhs := e | x ::= new | x :=p(b) | if b goto t else t | return x
Exprs e ::= b | *x | &x | op b … b
Locatables lhs ::= x | *x
Base Exprs b ::= x | c
Ops op ::= barious operators with arity >= 1
vars x ::= x| y | z| …
Proc Names p ::= p | q | r| …
Consts c ::= constants
Indices l ::= 0 | 1 | 2 | …
其中的含义我就不多说了，和C语言差不多。作者定义了一个五元组来描述程序运行的状态(t,p,a,e,m).其中t表示哪条语句将被执行，p表示程序内变量和主存位置的映射关系；a表示被映射的主存位置中存储的内容；e表示动态的调用栈;m表示新内存分配器。这样整个程序pi就能描述成这样一个五元组状态的转换过程。于是作者定义了转换函数->pi 用来表示pi中的单步转换。同时作者还给出了跨过程的转换函数~>pi，用来表示从当前过程调用语句状态到新过程内语句状态的转换函数。显然若程序在运行时出错就意味着，不存在一个转换到某个状态的转换函数。
2，Cobalt，
为了描述能自动证明的语言，作者对上面的中间表示中的Exprs，Vars和Consts做了扩展，分别如下
Exprs e ::= ……| E
Vars x ::= ……|X | Y|Z|….
Consts c ::= ……| C
可以将这些扩展部分看作是一种普适变量，即它们代表的是一类语言成分
有了这些扩展接下来就能用Cobalt来表示上面提到的转换模式和纯分析了。
对于C1和C2,我们可以使用下面的语法：
C ::= true | false | ~C | C AND C | C OR　Ｃ　| l(t,…,t) | t = t | case t of t => C … t => C else => C endcase
对于优化的语义，我们也同样可以表示出来，分成四个方面。按照上面的讨论，我们将合法的模式转换和优化分开，所以优化的语义分为三个阶段，一是识别，二是转换，三是Choose函数，另外还要加上纯分析的。这些形式化的表述只是将前面的论述符号化，具体内容请参见论文原文。

我的问题：作者貌似只是将普通的程序形式化，然后通过扩展普通程序中的表达式，变量和常数，增加类别代号的方式使得普通的程序语言能够用来作为识别一类语言的识别器。但是这样如何实现自动呢？

• 自动证明可靠性

作者首先给出语义等价转换的定义：对于中间语言是指，对于原程序main(v1)返回V2，对于固定的一些V1和V2组合，利用中间表示实现的该程序也必须满足。优化的可靠性则是指对于所有中间语言表示的程序PI和PI中的过程p，从p到优化后的p’的转换是语义等价转换。因此要想证明Cobalt语言实现的优化可靠，只需要证明该优化中对应的转换是语义等价的就行了。又因为优化常常是对某个转换的一些特定输入成立，所以为了证明可靠性，我们并不需要关心利益驱动部分。
接下来作者先介绍了Cobalt简化证明转换模式可靠的关键点的属性，接着介绍了前向和后向优化转换中的关键点。
证明转换模式可靠的关键点就是干扰，对于多个转换模式存在时，每个转换模式的语义等价也可能导致几个转换同时进行时语义的变化。某个优化可能干扰它自己的情况也不少见。例如一个同时进行死赋值删除和冗余赋值删除的优化。对于下面一段程序
…
S1: x := 5;
S2: x := 5;
…
这个优化可能将S1赋值认为是死赋值，S2认为是冗余赋值，但若同时删除，就出错了。但Cobalt语言描述的转换就不会产生自扰.就如上面这个优化,就必须拆分为两个优化才能用Cobalt来描述—一个前向,一个后向.因为Cobalt的无干扰特性,我们仅需要将特定优化的关键点分成一个个的转换来验证可靠性即可。
接着作者就针对前向转换模式和后向转换模式做了验证。

对于前向转换模式：前面作者提到证人其实就是用来保证语义相同的，这可以使证人区间内执行路径上到被转换语句的状态规约来证明，但通常自动机理论很难决定何时来做如此复杂的规约，作者也只需要能对关键路径和独立的执行状态序列做证明。而且作者也证明了这些关键路径只要对任何特定优化成立则该优化就是可靠的。
作者提出了一个定理：只要一个前向优化 C1 followed by C2 until s =>s’ with witness P 满足以下三个条件，那么该优化就是可靠的(原文中作者用了形式化的语言来描述，这里简化之)
一：证人P在使能语句C1之后的任何状态都成立
二；证人P在无害语句C2处都保持语义
三；s和s‘有相同的执行语义。
该定理证明过程，可以用条件一和二分别作为基础条件和归纳条件，来归纳出证人在整个证人区间内保持语义，而条件三表示转换前后的语句有相同的语义.对于前向纯分析,同理可证.

对于后向转换模式:
C1 preceded by C2 since s => s’ with witness P.
同理,满足下面三个条件则优化可靠
一,后向证人在原始语句和转换后程序之间,且在s和s’执行之后
二,后向证人在无害语句中保持语义不变
三,转换前后的执行结果在使能语句执行之后保持一直.

我的总结:作者就是先将转换的执行过程按照状态元组的方式划分成不同的状态,然后按照自动机的原理加上归约条件,从第一步开始一步步归约所有的无害语句,最终证明转换的语义不变性,妙哉.

• 实现COBALT

作者实现了能自动验证Cobalt优化正确性的检测器和一个运行优化的引擎
正确性检测器:使用Simplify自动机证明器实现的,通过提供一些背景定理分别证明上面提到的三个条件来实现.背景定理分为两类:优化无关和优化相关,再分别不同的动作来证明.作者还提供了将Cobalt转换成Simplify能接收的语言的机制,通过引入函数符号来表示某一类表达式和语句,接着形式化程序的状态.然后给出函数符号evalExpr来将表达式赋给给定状态.详细的实现方式,请参考论文.这里给出最后作者测试的结果:作者生成实现和自动证明了一些Cobalt实现优化和分析的正确性,在工作站上,通常一个检测平均用时28秒
运行引擎:为了能让Cobalt优化不需要应用在其他语言时重新编写,作者在WhirlWind编译器中实现了一个执行引擎,这个引擎从Vortex继承而来

• 实验结果探讨与下一步工作：

作者在Cobalt语言的易表达性，调试难度和精简可信计算上做了评测。
易表达性:主要表现在三个方面：一，因为很多和优化因素有关的实现都放在了利益驱动模块中，而模块中的choose函数可以使用其他语言来实现；二，证人区域的模式对很多过程内数据流前向分析都是相同的，对于后向，情况也非常类似，所以可以一劳永逸；三，传统需要在程序中多处起作用的优化，如不同的代码移动，都能使用Cobalt语言方便的拆解成几个简单的转换，每个转换都和Cobalt的转换模式语法匹配。接着，作者以PRE优化来说明，过去的PRE需要做复杂的代码移动，而使用Cobalt，仅仅需要前向和后向的转换加上合适的利益驱动即可。这种拆分的方式给用户带来了很多遍历。同时作者也承认Cobalt存在局限性，分析和优化中需要构建复杂数据类型时，Cobalt较难表达。
有辅助调试作用：通常些编译优化很难，因为需要考虑到很多语言边边角角的细节，但Cobalt使得将问题简化为若干个子问题。接着，作者举了自己在实际中将公共子表达式删除应用到load操作上是出错和调试的过程，通过可靠性证明失败,作者发现对于指针的公共子表达式删除,可能导致赋值被错误删除掉,进而出错.
精简了可信计算基(Trusted Computing Base,TCB):传统的可信计算基础需要包括整个编译器,而在作者的系统里,将复杂且易出错的优化提到可信计算基外,并将优化的可信性提升到三个层次:正确性验证,人工证明和优化执行的正确性.
下一步的工作:增加对过程间优化的支持,这需要一种可靠的描述跨过程调用的证人;目前Cobalt仅支持单个语句转换的情况,需要扩充;另外作者希望能以后自动推导出证人而非手工提供.还有一个作者称之为重要但未解决的问题:确定优化编写者和正确性自动验证器间的接口.

我的问题:在看到作者关于结果的讨论后,才觉得这件事情很有意义.但有没看出到底解决了什么问题,仅仅知道他提出了一种机制能够实现状态转换中的自动正确性验证,但是可靠吗?

相关文章:

• 前瞻-LLVM大事记(2004-2010)
• GCC初窥
• 前瞻-全时优化和LLVM-1
• 前瞻-全时优化和LLVM-2
• Open64课程-简介，概述和中间表示
• 《多核编译技术研讨会》记一
• 有写编译器的冲动？来看看这些网站
• Open64课程-结语
• 计算机系统结构方向的顶尖会议
• 探秘CPU性能测试：Spec CPU2000之整点篇