A Casual Introduction to Static Resource Analysis (In Chinese)

简单地说，程序的资源分析（Resource Analysis）指的是把该程序的资源消耗表示成一个关于程序输入的函数。 这里的资源可以是运行时间、内存使用、能源消耗，或别的什么数值指标。 高德纳（Donald Knuth）在《计算机程序设计的艺术》（The Art of Computer Programming）中就基于 MIX 汇编语言的语义讨论了一些资源分析的问题。 在计算机科学的课程中，资源分析通常以分析算法、数据结构的时间、空间复杂度的形式出现，而这里面最常见的又通常是渐近分析，即忽略常数、假定输入规模充分大时的复杂度，例如对长度为 $n$ 的数组进行归并排序时间复杂度为 $O(n \log n)$。 在这篇文章中，我们考虑一个稍微困难点的情况，即我们希望得到的分析结果是带有常数信息的非渐近复杂度：从非渐近分析可以容易得出渐近分析的结果，而且前者还可以用来精细地比较渐近复杂度相同的算法、数据结构。

静态资源分析即在不实际运行程序的情况下对其进行资源分析。 Facebook 出品的 Infer 工具提供了函数级的静态运行时间分析，其宗旨是在软件开发的过程中更早地指出性能问题（比方说，在 Code Review 阶段由工具自动反馈，而不是等到后面的性能回归测试）。 下面这个例子来源于 Infer 的官方文档¹：

void loop(ArrayList<Integer> list){
  for (int i = 0; i <= list.size(); i++){
  }
}

Infer 通过静态分析对上面这个函数得出一个描述其运行时间的多项式（比如 $8|list|+16$），从而知道这个函数的时间复杂度和其输入列表的长度呈线性关系。 如果某一次代码修改把这个函数更新为：

void loop(ArrayList<Integer> list){
  for (int i = 0; i <= list.size(); i++){
    foo(i); // newly added function call
  }
}

而此处的 foo 函数的时间复杂度也是与输入呈线性关系，那么 Infer 可以检测到 loop 函数的复杂度从 $O(|list|)$ 增长到了 $O(|list|^2)$，并向开发者发出警报。 （如果想要更深入了解 Infer 中的资源分析，可以参考这个视频。）

笼统地说，Infer 中的资源分析可以大致理解为对循环次数进行计数，从而将资源分析问题转化为程序变量数值关系的分析；这也是很多静态资源分析（比如 SPEED²）背后的原理。 在这篇文章中，我们来聊另一种颇为有趣的静态资源分析：自动均摊资源分析（Automatic Amortized Resource Analysis，AARA）。 这种方法衍生自 Robert Tarjan 在 1985 年的一篇论文³，文中给出了一种推导序列操作的最坏情况资源消耗的方法。 该方法的思路可以概括为：对于很多数据结构来说，一个操作消耗的资源很大程度上是由数据结构的状态决定的，而且有可能会根据状态有很大的不同；但是比较高的资源消耗（例如重新组织整个数据结构）往往会以一种可以预测的频率出现，也就是说，这些消耗在时间轴上均摊了。 均摊资源分析即利用了这种思想：我们可以把程序的执行看做是一个操作序列 $s_1,s_2,s_3,\cdots$，这里的每个 $s_i \in \mathrm{State}$ 都表示一个程序状态，而我们用一个函数 $cost(s_i,s_{i+1})$ 来描述资源的消耗；然后我们设计一个势能函数 $\Phi : \mathrm{State} \to \mathbb{Q}^+$ 把程序状态映射为非负数，使得对任意的 $i$，我们有 $$ \Phi(s_{i}) \ge cost(s_{i}, s_{i+1}) + \Phi(s_{i+1}), $$ 即一个状态的势能要足以支付当前程序操作的资源消耗以及下一个程序状态的势能（思考题：$cost$ 为负时意味着什么？）。 如此以来，$\Phi(s_0)$ 给出了程序的总资源消耗的一个上界，而我们需要做的是定义一个势能函数，并证明在每个程序执行的局部，上述表达式成立。 这意味着均摊资源分析的 Compositionality 是很好的！

我们知道，类型系统的一大特点也是 Compositionality；所以，设计一个用于均摊资源分析的类型系统是非常自然的想法。 考虑下面这段 OCaml 代码，它是连接两个列表的简单实现，而我们想要分析它递归调用的次数（这也是一种资源消耗）：

let rec append (l1, l2) =
  match l1 with
  | [] -> l2
  | x :: xs ->
    let rest = append (xs, l2) in
    x :: rest

我们能够很容易地看出 append 函数递归调用的次数是 $|l_1|$。 假定这个 append 函数的类型为 $L(\alpha) \times L(\alpha) \to L(\alpha)$，这里的 $L$ 即表示列表类型。 均摊分析要求我们给程序状态赋予势能，在这个例子中，我们则需要把我们的势能放在 append 的参数 $l_1$ 和 $l_2$ 里。 让我们给列表类型增加一个数值标注：用 $L^q(\alpha)$ 表示一个列表类型，其中的每个元素都携带了 $q$ 单位的势能，并假定所有程序操作的资源消耗都是 $0$，除了递归调用的消耗为 $1$ 单位。 所以，append 的带资源标注的类型可以写为 $L^1(\alpha) \times L^0(\alpha) \to L^0(\alpha)$：如果我们计算参数和结果之间的势能差，我们就能发现那恰好是 $|l_1|$。 但是，我们如何通过类型系统来检查这个类型是不是正确的呢？ 还记得 Compositionality 吗——我们只需要对局部操作验证一下势能不等式：比如，在模式匹配时，如果 $l_1$ 非空，那么我们把它解构为 $x$ 和 $xs$，其中 $xs$ 的类型与 $l_1$ 相同，为 $L^1(\alpha)$，但是 $xs$ 的长度比 $l_1$ 少 $1$，所以这一步解构给了我们 $1$ 单位的自由势能，我们可以用它来支付紧接着的这个递归调用。 接着我们检查 $xs$ 和 $l_2$ 的类型是否符合 append 的类型签名（当然！）。 最后，类型签名告诉我们 $rest$ 的类型为 $L^0(\alpha)$，所以构建最终返回结果 $x :: rest$ 也不需要往这个数据结构里面存势能了。

我在这份胶片里更详细地展示了这个带资源标注的类型系统。 需要特别提出的是，自动推导这些数值标注并不困难：我们用变量来表示这些类型标注，那么类型检查就成为了生成关于这些变量的约束（通常是线性的）的过程，最后再解这些约束就好了。 在这个页面上你可以和一个实现了自动均摊资源分析的工具（Resource-aware ML，RaML）玩耍，其主要贡献者也在今年发表了一篇还不错的综述⁴。 祝大家玩得愉快！