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

### 逻辑程序的用户可定义资源边界分析 #### 1. 引言 在计算领域，推断计算成本信息对多种应用非常有用，这些成本通常与执行步骤、时间或内存相关。本文提出一种分析器，可自动推断逻辑程序对用户可定义资源使用的上下界。用户可定义的资源包括应用通过套接字发送或接收的比特数、过程调用次数、打开的文件数、数据库访问次数、消耗的许可证数量、花费的货币单位、使用的磁盘空间等，以及传统的执行步骤、执行时间或内存。 推断这类信息在多种应用中具有重要作用，如资源使用验证和调试、移动代码资源消耗认证、并行/分布式计算中的资源/粒度控制或面向资源的特化。 在本文的方法中，资源是用户定义的概念，它将基本成本函数与基础语言中的基本操作和/或库中的某些谓词相关联。每个资源本质上是一个用户定义的计数器，用户为计数器命名（如“bits received”），然后通过断言定义程序中每个基本操作如何增加或减少该计数器的值。资源的使用通常取决于程序或谓词某些输入的大小或值，因此在描述基本操作的断言中，计数器的增减量不仅可以是常量，还可以是输入数据大小或值的函数。本文方法的目标是从这些基本断言和程序文本中静态推导出函数，这些函数可得出程序中每个谓词（以及整个程序）消耗或提供的这些资源量的上下界，这些函数的输入也是被分析程序或谓词的顶级输入数据的大小或值范围。 与以往的工作相比，本文方法具有以下优势： - 可以处理开放类的资源，这些资源由程序员使用断言语言定义。 - 允许定义外部谓词的资源使用，可用于模块化组合。 - 断言可手动描述自动分析不够准确的谓词的使用情况，防止自动推断中的不准确传播。 #### 2. 资源断言语言 资源断言语言用于描述资源、为资源分析提供其他输入，也是资源分析产生输出的语言。此外，它还用于陈述与资源相关的规范，这些规范可根据分析结果进行证明或反驳，有助于发现错误、验证程序等。 断言语言语法规则如下： ```plaintext ⟨program assrt⟩::= :- ⟨status flag⟩⟨pred assrt⟩. | :- head cost(⟨approx⟩,Res name,ΔH). | :- literal cost(⟨approx⟩,Res name,ΔL). ⟨status flag⟩ ::= trust | check | true | ϵ ⟨pred assrt⟩ ::= pred ⟨pred desc⟩⟨pre cond⟩⟨post cond⟩⟨comp cond⟩. ⟨pred desc⟩ ::= Pred name | Pred name(⟨args⟩) ⟨args⟩ ::= Var | Var, ⟨args⟩ ⟨pre cond⟩ ::= : ⟨state props⟩| ϵ ⟨post cond⟩ ::= => ⟨state props⟩| ϵ ⟨comp cond⟩ ::= + ⟨comp props⟩| ϵ ⟨state prop⟩ ::= size(Var,⟨approx⟩,⟨sz metric⟩,⟨arith expr⟩) | State prop ⟨state props⟩ ::= ⟨state prop⟩| ⟨state prop⟩, ⟨state props⟩ ⟨comp prop⟩ ::= size metric(Var,⟨sz metric⟩) | ⟨cost⟩| Comp prop ⟨comp props⟩ ::= ⟨comp prop⟩| ⟨comp prop⟩, ⟨comp props⟩ ⟨cost⟩ ::= cost(⟨approx⟩,Res name,⟨arith expr⟩) ⟨approx⟩ ::= ub | lb | oub | olb ⟨sz metric⟩ ::= value | length | size | void ⟨arith expr⟩ ::= −⟨arith expr⟩| ⟨arith expr⟩! | ⟨quantifier⟩⟨arith expr⟩ | ⟨arith expr⟩⟨bin op⟩⟨arith expr⟩ | ⟨arith expr⟩⟨arith expr⟩| logNum ⟨arith expr⟩ | Num | ⟨sz metric⟩(Var) ⟨bin op⟩ ::= + | −| ∗| / ⟨quantifier⟩ ::=  |  ``` 谓词可以用零个或多个`pred`断言进行注释，这些断言陈述了谓词调用时执行状态的属性（`pre cond`）、谓词执行终止时执行状态的属性（`post cond`）或整个谓词计算的属性（`comp cond`，本文仅用于与资源相关的属性）。为简洁起见，`<state props>`字段也可以使用“星号表示法”书写。此外，可能有一组全局的`head cost`和`literal cost`声明（每个资源和近似方向各一个）。`Res name`字段确定断言所指的资源，这些`Res name`是用户提供的标识符，为每个需要跟踪的特定资源命名。`<approx>`字段说明`<arith expr>`是提供上界还是下界（`oub`表示“大O”表达式，仅包含阶信息；`olb`表示Ω渐近下界）。 断言的主要用途如下： - 描述某些谓词的执行如何增加或减少程序中定义的资源（计数器）的使用。分析的目的是推断程序中所有谓词的资源使用情况。 - `head co