逻辑程序的用户可定义资源边界分析

### 逻辑程序的用户可定义资源边界分析 在逻辑程序的分析中，资源边界分析是一项重要的任务，它有助于我们了解程序在运行过程中对各种资源的使用情况。本文将详细介绍基于数据依赖的大小分析方法，以及如何利用这些方法进行资源使用分析。 #### 1. 大小分析 大小分析的目的是推断谓词头部输出参数的大小界限，这些界限是输入参数大小的函数。同时，大小分析还能得到子句体文字输入参数大小的界限，这些界限同样是子句头部输入参数大小的函数。后续，我们将利用子句体文字输入参数的大小来推断其资源使用情况。 ##### 1.1 大小度量 对于参数的“大小”，可以使用多种度量方式，如值、长度等。为了简化，本文仅考虑长度度量。 我们定义了两个重要的操作： - `size(⟨sz metric⟩, t)`：返回项 `t` 在指定度量 `⟨sz metric⟩` 下的大小。以长度度量为例： ```plaintext size(length, t) = ⎧ ⎨ ⎩ 0 if t = [ ] (the empty list) 1 + size(length, T ) if t = [H|T ] ⊥ otherwise. ``` 例如，`size(length, [X, Y ]) = 2`，而 `size(length, [X|Y ]) = ⊥`。 - `diff(⟨sz metric⟩, t1, t2)`：返回两个项 `t1` 和 `t2` 在指定度量 `⟨sz metric⟩` 下的大小差异（上界）。以长度度量为例： ```plaintext diff(length, t1, t2) = ⎧ ⎨ ⎩ 0 if t1 ≡t2 diff(length, t, t2) −1 if t1 = [ |t] for some term t ⊥ otherwise. ``` 例如，`diff(length, [a, b|T ], T ) = -2`。 ##### 1.2 参数依赖图 为了表示子句体中参数位置之间以及它们与子句头部参数位置之间的数据依赖关系，我们使用有向无环图，即参数依赖图。图中的每个节点表示一个参数位置，如果节点 `n1` 生成的变量绑定用于构造节点 `n2` 处的项，则存在从 `n1` 到 `n2` 的边。此时，`n1` 是 `n2` 的前驱节点，`n2` 是 `n1` 的后继节点。 ##### 1.3 大小关系的建立 利用 `size` 和 `diff` 函数以及参数依赖图，我们可以建立大小关系，以表达每个参数位置的大小与其前驱节点大小的关系。 - **输出参数**：设 `l1, ..., ln` 为文字 `L` 的输入参数位置，`Ψ b p : N n ⊥,∞ → N⊥,∞` 是一个函数，表示文字 `L` 的谓词 `p` 的第 `b` 个（输出）参数位置的大小与输入位置大小的关系。如果 `a` 是子句中的输出参数位置，则建立如下大小关系： ```plaintext sz(a) ≤ Ψ a p(sz(l1), ..., sz(ln)) ``` 如果 `L` 是递归的，`Ψ a p(sz(l1), ..., sz(ln))` 是一个符号表达式；如果 `L` 是非递归的，则该函数已递归计算，我们将其替换为应用该函数得到的显式表达式。 - **输入参数**：假设 `a` 是子句体文字中的输入参数位置，`predecessors(a)` 是参数依赖图中 `a` 的前驱节点集合。有以下几种情况： 1. 计算 `size(@a)`。如果 `size(@a) ≠ ⊥`，则建立大小关系： ```plaintext sz(a) ≤ size(@a) ``` 2. 否则，如果存在 `r ∈ predecessors(a)`，使得 `r` 和 `a` 对应的大小度量相同，且 `d = diff(r, a) ≠ ⊥`，则： ```plaintext sz(a) ≤ sz(r) + d ``` 3. 否则，如果可以使用 `size` 函数的定义扩展 `size(@a)`，则将 `size(@a)` 扩展一步，并递归计算 `@a` 适当子项 `ti` 的 `size(ti)`。如果这些递归大小计算都有定义的结果，则使用它们来计算 `size(@a)` 的大小关系；否则，`sz(a) = ⊥`。 大小关系可以传播，将子句体文字输入参数或子句头部输出参数的大小关系转换为关于头部输入参数大小的函数。基本思想是将子句体文字的大小关系反复代入头部参数的大小关系，这就是归一化算法的目的。对于递归子句，需要先将递归文字的符号表达式求解为显式函数。 ##### 1.4 示例 考虑一个程序，为了简化表示，将 `exchange buffer/3` 和 `exchange byte/3` 分别表示为 `ex buf` 和 `ex byt`。对于 `exchange buffer/3` 的递归子句： - 首先，系统为子句体文字的输入/输出参数建立大小关系： ```plaintext sz(ex byt1) ≤ size(B) = sz(arg(1, head1)) sz(ex byt2) ≤ size(Id) = sz(head2) + diff(Id, Id) = sz(head2) sz(ex byt3) ≤ Ψ 3 ex byt(sz(ex byt1), sz(ex byt2)) = 1 sz(ex buf1) ≤ size(Bs) = sz(head1) + diff([B|Bs], Bs) = sz(head1) - 1 sz(ex buf2) ≤ size(Id) = sz(head2) + diff(Id, Id) = sz(head2) sz(ex buf3) ≤ Ψ 3 ex buf(sz(ex buf1), sz(ex buf2)) ``` - 然后，为头部的输出参数建立大小关系： ```plaintext sz(head3) ≤ size([B0|Bs0]) = size(Bs0) + 1 = sz(ex buf3) + diff(Bs0, Bs0) + 1 = sz(ex buf3) + 1 ``` - 应用归一化算法得到： ```plaintext sz(head3) ≤ Ψ 3 ex buf(sz(ex buf1), sz(ex buf2)) + 1 ≤ Ψ 3 ex buf(sz(head1) - 1, sz(head2)) + 1 ``` - 系统为头部的输出参数（`head3`）建立差分方程，并从非递归子句中得到边界条件 `Ψ 3 ex buf(0, y) = 0`，然后通过调用差分方程求解器得到封闭形式的函数： ```plaintext Ψ 3 ex buf(0, y) = 0 Ψ 3 ex buf(x, y) = Ψ 3 ex buf(x - 1, y) + 1 ⇒ Ψ 3 ex buf(x, y) = x ``` #### 2. 资源使用分析 为了推断资源使用函数，程序中的所有谓词将按照调用图的逆拓扑顺序进行单次遍历。 ##### 2.1 谓词的资源使用 考虑由子句 `C1, ..., Cm` 定义的谓词 `p`，假设 `n` 是一个元组，每个元素对应谓词 `p` 输入参数位置的大小。则调用谓词 `p` 时，对于大小为 `n` 的输入，其资源使用（以资源 `r` 的单位表示，近似值为 `ap`）可以表示为： ```plaintext RUpred(p, ap, r, n) = ⋀(ap ```