Karr's algorithm算法学习

摘要

主要是学习文章《A Note on Karr's Algorithm》

简述

这篇论文的重要贡献是用仿射基代替原始算法的核表示，将Karr算法的时间复杂度降低了一个因子k，从原来的$O(nk^4)$优化到了$O(nk^3)$。同时也推广到了在$O(nk^{3d})$时间内确定所有次数不超过$d$的多项式关系。

引言

Karr提出算法用于计算流图(flow graph)中每个程序点(program point)处，当控制流到达该点时，程序变量之间所满足的仿射关系构成的向量空间。

Karr算法是一个迭代不动点算法，通过流图传播仿射空间，为每个程序点u计算一个仿射空间，该空间过近似了在u处可能出现的所有运行状态的集合。对计算出的仿射空间中所有状态都成立的仿射关系，也对所有可能的运行时状态成立。

Karr算法是用核表示(把仿射空间拆分为线性方程组的解集)，而这篇论文所提出的方法是利用基表示法(用m+1个点表示m维空间)

但是Karr算法也存在困难:使用了相当复杂的操作，算法可能存在指数级增长。

这篇论文则是简化了操作，降低了时间复杂度，并且降低到多项式时间增长。

这个简化算法采用了仿射独立点的方法来表示仿射空间A(降低了并集操作和传递函数的复杂度)，通过半朴素迭代降低复杂度，同时还将Karr算法从仿射关系推广到多元多项式中。

本文研究的是仿射程序。

仿射程序

通常假设变量取值于有理数域。

每个仿射赋值s诱导了程序状态上的一个变换[[s]]，是一个仿射变换，即可以写成$$[[\boldsymbol{s}]]\boldsymbol{x} = A \boldsymbol{x} + \boldsymbol{b}$$ 其中$A \in \mathbb{Q}^{k*k}, \boldsymbol{b} \in \mathbb{Q}^k$

在程序中，每个赋值语句都可以表示为这种形式，这让我们可以用线性代数的全部工具来分析程序。

一个仿射程序由一个控制流图$ G = (N, E, st) $给出，其中$ N $是程序点的集合；$ E \subseteq N * Stmt * N $是边的集合；$st \in N$是一个特殊的入口点。

通过程序的收集语义作为评判Karr算法正确性和完备性的参考点，可以被刻画为约束系统$\boldsymbol{V}$关于状态集合的最小解(只包含确实可能到达的状态)。

收集语义是理想目标——它精确描述了每个程序点所有可能的状态。但直接计算收集语义通常是不可行的(可能有无穷多种状态)，所以我们需要抽象:用一个更简单的对象(仿射空间)来近似它。

算法

算法的目标:为每个程序点$u$计算其收集语义的仿射包$\operatorname{aff}\left( V[u] \right) $。显然$\operatorname{aff}$是一个闭包算子，即它是单调的。

仿射空间对交集封闭，对并集不封闭。仿射空间空集的维度定义为-1，在严格递增的链中维数必须严格递增，最长链从-1到k。

完备格表示为$\left( \mathbb{D}, \sqsubseteq \right) = \left( \{ \boldsymbol{X} \subseteq \mathbb{Q}^k \mid \boldsymbol{X} = \operatorname{aff} ( \boldsymbol{X} )\}, \subseteq \right)$

下面有几条性质

先并集再取仿射包 = 先取仿射包再求格上界

在抽象域上的join运算和具体域上的"并集 + 仿射闭包"是完美对应的$$\operatorname{aff}(\bigcup \mathcal{X}) = \bigsqcup \{ \operatorname{aff}(X) \mid X \in \mathcal{X} \}$$

维度上下界保证了链有限

任何严格递增的仿射空间序列至多有$ k + 2 $个元素，即最多$ k + 1 $次增长(即整个算法必然在有限步内终止，最坏情况下每个点被加入的点数不超过$k + 1$个基向量)。

仿射变换与仿射包可交换

仿射变换与仿射包可交换$ \operatorname{aff} \left( f_{s} \left( \boldsymbol{X} \right) \right) = f_{s} \left( \operatorname{aff} \left( \boldsymbol{X} \right) \right)$，这说明我们不需要在具体状态上操作，可以直接在抽象的仿射空间上操作，并且不损失任何精度。

从"具体约束系统"到"抽象约束系统"

具体约束系统$\boldsymbol{V}$:$$[V1] V[st] \subseteq \mathbb{Q}^k$$ $$[V2] V[v] \subseteq f_{s} \left( V[u] \right) $$

抽象约束系统$\boldsymbol{V}^{\#}$:$$[{V1}^{\#}] V^{\#}[st] \sqsubseteq \mathbb{Q}^k $$ $$[{V2}^{\#}] V^{\#}[v] \sqsubseteq f_s \left( V^{\#}[u] \right) $$

解出每个程序的仿射空间为最小仿射空间

抽象解=具体解的精确抽象

$V^{\#}[v]$就是包裹住所有可达状态的最小的仿射空间$$V^{\#}[v] = \operatorname{aff} \left( V[v] \right) $$

也就是把仿射空间域的高量化到$ k + 1 $，并说明join和具体并集加仿射包的一致性，以及仿射变换如何完美适配这个域。共同构成了Karr算法可以从空集开始，沿着控制流反复做join，最多k不就必然达到不动点的数学理由。

因此可以采用仿射空间的有限表示。算法用仿射基来表示仿射空间$ \boldsymbol{X} \subseteq \mathbb{Q}^k $。这使得我们可以使用半朴素不动点迭代来计算约束系统的解。

算法部分

用$G[u]$储存每个程序点$u$的状态，用工作集$W$存储还没有传出去的增量(存放形如$\left( u, \boldsymbol{x} \right)$的配对。

初始化起始点$G[st]$为$$\{\boldsymbol{0}, \boldsymbol{e_1}, ..., \boldsymbol{e_k} \}$$ 初始化$W$为$$\{\left(st, \boldsymbol{0}\right), \left(st, \boldsymbol{e_1}\right), ..., \left(st, \boldsymbol{e_k}\right)\}$$

之后我们对每个$W$的值进行出边的计算，并得到对应点上的状态和新的$W$值，如果不属于$G$的仿射空间，则把它放进$G$内并存回$W$中。

部分解释

流图

流图:由节点(程序点，表示代码的位置)和边(代表语句执行组成。

程序点

程序点:程序点某个位置，算法要求的就是每次执行到这个位置，变量之间有什么不变的关系。

非确定性分支

非确定性分支:当程序执行到某个分支时，不预测走哪个分支，而是假设两个分支都走(放弃对条件的判断，以便让算法保持简单、快速、保证结果的安全，分析的时候默认变量可以取所有值。

仿射程序

仿射程序:具有非确定性分支，并且只包含右端为仿射表达式或等于未知值的赋值语句。

$N * Stmt * N$

$N * Stmt * N$:是卡迪尔积，把所有节点、语句、节点排成三元组的所有可能组合。

收集语义

收集语义:把所有可能执行路径中，在同一个程序点出现过的状态，全部收集到一个大集合中，即保存一个程序点到所有可能状态。

约束系统$\boldsymbol{V}$

入口可以是任何状态(我们并不知道初始值)$$[V1]V[st] \subseteq \mathbb{Q}^k $$ 如果有一条从$u$到$v$的边，那么执行这条边上的语句后，从$u$能到达的状态也会到达$v$ $$[V2]V[v] \subseteq f_{s} \left(V[u]\right)$$

仿射包

仿射包:子集$ G \subseteq \mathbb{Q}^k$ 的仿射包定义为所有可以表示为$G$中点的仿射组合的集合。

仿射组合

仿射组合:每个点配一个权重，所有权重加和为1，对所有点的所有加权情况求加权和的集合。

仿射基

仿射基:如果$\boldsymbol{G}$是使得$\boldsymbol{X} = aff \left( \boldsymbol{G} \right)$的最小集合，则称$\boldsymbol{G}$为$\boldsymbol{X}$的一个仿射基。

闭包算子

闭包算子:取最小闭包，关键性质(做一次和做两次的结果一样)。

格

格:格是用来严谨地描述谁比谁更准确的工具，格具备三大要素。

格的第一要素

偏序关系:$ a \sqsubseteq b $读作"$a$比$b$更准确，包含关系是偏序的一部分。

格的第二要素

最小上界:符号$a \sqcup b $，把两个空间包起来的最小仿射空间。

格的第三要素

最大下界:符号$a \sqcap b $，两个空间的交集。

完备格

完备格:在格的基础上把两个元素推广到任意子集。

半朴素迭代

半朴素迭代:不用每次把整个仿射空间重新传播，只传播增量。

公式引入测试

行内公式：$E = mc^2$

块级公式：$$\sum_{i=1}^n i^3 = \left( \frac{n(n+1)}{2} \right)^2$$