数据流分析(2) - 框架化分析 distributive framework

之前我简单的介绍过几种常见的过程内分析算法。可以看到这些算法有非常大的相似性，本质都是使用一个worklist里面存放需要分析的语句，再使用Kill/Gen 函数（或者说方程）对系统的约束条件进行求解，最终得到想要的结果。很自然的就可以想到有没有一种理论可以把之前提到这几种过程内分析算法给统一起来，变成一种框架式的代码，这样比较方便我们使用和reason。

使用代数结构来抽象问题，以得到框架化的结构，是程序分析中的常用思路，并且使用抽象代数结构，在证明的时候也会比较容易一点。格(lattice)就是被广泛使用的一种代数结构。

偏序集(Partial Order Set) 与格(Lattice)

在介绍格之前先简单介绍一下偏序集(partial order set)。因为格是定义在他上面的。
偏序关系没啥好多说的，如果你没有学习过代数知识其实也很好理解，通俗的说就是元素之间有大小关系，但是不是每一个元素互相都有大小关系，有些没法比较，经典例子就是拓扑顺序。
偏序集是一个二元组 $(P, \sqsubseteq)$ 其中

$\sqsubseteq : P \times P \rightarrow \{ true, false \}$ 是一个P上的二元关系，
满足自反性，反对称性，传递性

如果在一个偏序集中，存在一个任意两个元素都有唯一的上界和下界那么这个偏序集合构成一个格(lattice)。
根据定义不难发现，两元素之间一定存在取上界和取下界的函数，可定义如下：
$\sqcap$ 是meet操作符，可以求出x ，y的上界

$x ~ \sqcap ~ y ~ \sqsubseteq ~ y$ , $x ~ \sqcap ~ y ~ \sqsubseteq ~ x$
若 $z ~ \sqsubseteq ~ x$ , 并且 $z ~ \sqsubseteq ~ y$ ,那么有 $z ~ \sqsubseteq ~ x ~ \sqcap ~ y$

$\sqcup$ 是join操作符，可以求出x ，y的下界

$x ~ \sqsubseteq ~ x ~ \sqcap ~ y$ , $y ~ \sqsubseteq ~ x ~ \sqcap ~ y$
若 $x ~ \sqsubseteq ~ z$ , 并且 $y ~ \sqsubseteq ~ z$ ,那么有 $z ~ \sqsubseteq ~ x ~ \sqcup ~ y$

如果上述的join和meet操作只有一个被定义了，这种代数结构被称作半格(semi-lattice)

如果我们继续增加限制，meet和join操作必须对所有P的子集都有定义，那么这种格也被称作完全格(complete lattice).
性质：
一个完全格必有一个全局的最大值(top)和一个最小值(bottom), 记做 $\top$ , $\bot$
所以可以完全格也可以用以下的六元组来表示 $(P, \sqsubseteq , \sqcap,\sqcup,\top,\bot)$

回到程序分析上来说，因为我们需要求解的问题的最终都是要通过迭代求得一个不动点，在计算的过程中，中间的结果就一定是有某种顺序的，但是大多数情况下这种顺序又是偏序的，而且因为我们的迭代函数每一步都必然有结果，所以使用格这一代数结构是比较完美符和要求的。
比如求解available expression的过程就可以用下面的格来表述：

available expression

常数传播(constant propagation)就可以用如下格：

constant propgation

Worklist 算法

之前的文章我已经实现过混沌迭代(chaotic iteration)求解数据流分析的问题。在那个算法中，我们判断不动点的时候每次都要把整个step函数的结果和之前一次的执行结果去比较。这个思路非常的直接，其实对于数据流分析，我们有更加简单的判断方法。
我们可以在这个算法的基础上添加一个worklist来统合我们的算法，比如一个Forward Must Analysis就可以用如下算法实现

Out(s) = ⊤ for all statements s
W := { all statements }                    (worklist) 
repeat {
    Take s from W
    In(s) := ∩s′∊ pred(s) Out(s′)
    temp := Gen(s) ∪ (In(s) - Kill(s))
    if (temp != Out(s)) { 
        Out(s) := temp 
        W := W ∪ succ(s)
    }
} until W = ∅

单调性(monotonicity)与算法终止的证明

根据偏序集的性质我们不难在偏序集（为定义域）上定义单调函数
f是单调的(monotonic)：假如 $x ~ \sqsubseteq ~ y$ 那么 $f(x) ~ \sqsubseteq ~ f(y)$
在上面的worklist算法中，观察

In(s) := ∩s′∊ pred(s) Out(s′)
temp := Gen(s) ∪ (In(s) - Kill(s))
也可以内连一下---> 
temp := fs(∩s′∊ pred(s) Out(s′))

其中 $f_s$ 也叫传递函数(transfer function)
可以发现这一迭代的核心计算部分（计算temp）的过程就是一个单调的函数(Forward Must请自动带入available express和上面有过的lattice图)

从前面的格图上我们可以看出来，格是有类似高度的属性的。
首先定义下链(chain):
Y是偏序集P的一个子集，并有 $\forall x_0,x_1 \in Y, (x_0 \sqsubseteq x_1) \lor (x_0 \sqsubseteq x_1)$ .
通俗的说就是格这个图里的一条路径。因为都是用小于链接的所以这是一条下降的路径被称为降链(Descending Chain)
接下来可以定义格的高度(height)了：
格中最长的降链被称为格的高度。

在定义了单调函数和格的高度之后之后我们可以这样来证明算法可终止。
因为上述整个迭代函数中，要么是W在减小，要不是Out(s)在减小，所以，整个迭代函数必然是单调递减的。从格的角度来说，因为格是有限高的，所以对于任意给定的程序语句集合s, (AExp,具体的可以翻之前PPA的小节), Out(s)只能递减有限次。故算法可终止。并且算法的时间复杂度为 $O(nk)$ ,

n是语句集合s的大小
k是格的高度
假设meet的时间复杂度是1

进一步抽象前向分析算法

我们可以把之前Forward Must算法中传递函数 $f_s$ 稍微做一下修改，把原本的集合操作替换成meet操作符，就得到了一个更加泛化的算法。 Must和May不过是算法先从 $\top$ 开始然后选取合适的meet函数,给出符合要求的格P。

temp := fs(⊓s′∊ pred(s) Out(s′))

总结如下：
Available Expression

P = 所有语句
$\sqcap$ = $\cap$
$\top$ = 所有语句

reach definition

P = 赋值语句
$\sqcap$ = $\cap$
$\top$ = $\emptyset$

分配率(distributive)

如果一个偏序集上的函数满足分配率，那么
如果有 $f(x ~ \sqcap ~ y) \sqsubseteq ~ f(x) ~ \sqcap ~ f(y)$
则 $f(x ~ \sqcap ~ y) = ~ f(x) ~ \sqcap ~ f(y)$
定义其实和一般的函数分配率没有什么区别
不难发现我们之前说过的所有kill/gen style的分析算法都符合这一点，我们在Meet函数操作的过程中并没有发生信息的丢失。

满足交换率的问题我们可以统一抽象为meet over all path(MOP) solution.
(其实我应该先定义路径(Path)是算法从程序起点到运行到哪个block入口的遍历过程)
定义如下：

$f_s$ 是传递函数
如果p是路径 $s_1 ... S_n$ , 有代入f后 $f_p = f_{sn}; ...f_{s1}$
paths(s) 是从entry到sd的路径
$MOP(s) = \sqcap_{p \in paths(s)}f_p(\top)$

那么有没有不符合分配率的算法呢？当然是有的，最经典的例子是常量传播(constant propgation)算法。
具体的等下一次我写Constant Prop的时候再证明好啦。

这一次的文章基本完全翻译自Kris导师的slides
因为真的非常好，以前第一次读PPA这个章节的时候真的云里雾里的。

btw, proud of my code here!
我的实现