保障冷调度器正确性及程序调试技术综述

### 保障冷调度器正确性及程序调试技术综述 #### 一、有限状态机数据（FSMD）相关理论与方法 在程序验证中，有限状态机数据（FSMD）是一个重要概念。当重新访问具有相同变量值的各自起始状态时，对于所有可能的输入，某些FSMD的特性是相同的。下面给出相关定义： - **定义2**：若对于FSMD F0的每一个状态μ0，都存在FSMD F1的一个状态μ1，使得μ0与μ1等价，则称FSMD F0包含于FSMD F1，记为F0 ⊑ F1。 - **定义3**：若F0 ⊑ F1且F1 ⊑ F0，则称两个FSMD F0和F1是等价的。 由于程序可能包含循环，且循环边界在编译时可能未知，要捕获所有可能的循环迭代，就需要考虑无限数量的计算，这在一个FSMD中枚举所有此类计算是不可行的。不过有如下定理可以克服这些困难： - **定理1**：对于任意两个FSMD F0和F1，如果存在F0的一个有限覆盖P0 = {p00, p01, ..., p0k}，并且存在F1的一组路径P01 = {p010, p011, ..., p01k}，使得p0i ≃ p01i（0 ≤ i ≤ k），那么F0 ⊑ F1。 等价检查方法需要保持两个FSMD状态之间的对应关系，对应状态的概念定义如下： 1. 复位状态对⟨q00, q10⟩是对应状态（CS）。 2. 设q0i ∈ Q0和q1j ∈ Q1是对应状态，在F0中存在从q0i到q0x的路径α，在F1中存在从q1j到q1y的路径β，且α ≃ β，则⟨q0x, q1y⟩是对应状态。 #### 二、FSMD等价检查方法 基于定理1，有如下用于检查两个FSMD等价性的算法： ```plaintext 算法1：FSMD等价检查 1: 在F0和F1中插入割点。 2: 分别获取F0和F1的路径覆盖P0和P1。设P0为{p00, p01, · · ·, p0k}，P1为{p10, p11, · · ·, p1l}。 3: τ = {⟨q00, q10⟩}，其中τ是对应状态的集合。 4: 对于μ中的每一个⟨q0i, q1j⟩ 5: 证明从状态q0i开始的P0中的每一条路径∀p0x，在F1的P1中都存在一条从q1j开始的路径p1y，使得p0x与p1y等价。 6: 将p0x和p1y的结束状态作为对应状态添加到τ中。 7: 结束循环 8: 交换F0和F1，执行上述循环。 ``` 在这个工作中，选择以下状态作为FSMD中的割点： 1. FSMD的起始状态是割点。 2. 任何分支状态也是割点。 这种选择确保程序的所有循环至少被一个割点切断，因为任何循环都有一个退出路径，会产生一个分支状态，这一思想源自Floyd - Hoare的程序验证方法。 #### 三、从汇编代码中提取FSMD 将汇编代码转换为FSMD的算法维护一个状态哈希表，状态可能与输入程序决定的标签相关联。在分支操作时，可能需要访问之前已经创建的状态，可通过相应的标签获取该状态。算法维护两个变量currentState和nextState，currentState维护输出FSMD的当前状态，nextState维护当前转换的下一个状态。 ```plaintext 算法2：将汇编代码转换为FSMD 为每个标签创建唯一状态； 创建起始状态；将其设为nextState； while (未到输入文件末尾) { 读取下一个键； if (键是标签) 获取与标签对应的状态； else 将nextState复制到currentState； if (键不是分支键) 读取操作并在FSMD中添加一个转换； 根据下一个键确定nextState； else // 是分支键 分别从标签then_part和else_part确定nextState和nextState1； 为分支语句添加两个转换； } ``` 分支可以有多种类型，如等于分支（be）、大于分支（bg）、小于分支（bl）、小于等于分支（ble）等。分支语句后面跟着代码else部分对应的标签，再跟着无操作（nop），然后是then部分的标签。两个下一个状态由这两个标签确定。如果标签已经存在于状态表中，就获取对应的状态；否则，为该标签创建一个新状态并存储在哈希表中。 #### 四、冷调度验证 从汇编代码中提取的FSMD可以用于冷调度验证。例如，从特定汇编代码提取的FSMD中，初始FSMD的路径α = ⟨q00 → q08⟩和输出FSMD的路径β = ⟨q10 → q18⟩，两条路径的条件都是TRU