Page 70 - 《软件学报》2021年第6期

1644 Journal of Software 软件学报 Vol.32, No.6, June 2021

• 当 ESR 中不包含任务的启动或停止操作时不会产生任务的切换,异常退出时,寄存器中的内容依旧是
原任务的上下文数据.
将系统的初始状态定义为 mac_Status_pre,即异常响应即将进入中断向量表进行处理时刻的状态,任务初
始状态也是 Hoare-logic 中的前置条件 P:
def
,
},
mac _ Status pre = s { 1 ~ 7}∧ G g g L s {CWP ,( 0 ~ 7, 0 ~ 7, 0 ~ 7)}∧l l i i o o s S {psr ,tbr , , pc npc }∧wim M s {nest ,tcb
_
其中,
• G s 表示的全局寄存器的初始状态;
• L s 表示进入异常管理时 CWP 指向的当前窗口状态;
• S s 表示进入异常管理时刻特殊寄存器的状态,其中:tbr 表示记录了异常的类型与优先级,wim 表示原任
务目前已经使用的寄存器窗口都有哪些,pc 保存的是被打断指令的地址;
• M s 表示内存中全局变量在此时刻的值,其中:nest 表示系统中目前发生的异常嵌套的层数,为了方便讲
述建模过程,我们假设目前系统中还并没有进行异常处理,即 nest 的值为 0;tcb 是任务控制块指针,此时
指向的是原任务的代码入口地址.
异常退出时刻,系统的状态为异常管理程序逻辑框架的终止状态,即 Hoare-logic 中的后置条件,若异常中不
发生任务切换,即 swflag 的值为 0,后置条件被定义为 mac_Status_post,也就是说,最终异常退出时,寄存器中的数
据和响应异常时中的大部分数据始终保持一致,指令计数器的值 pc/npc 均指向下一条要被指向的指令,全局变
量 tcb 依旧指向被异常打断的原任务.若 ESR 中有任务切换的情况,异常退出时刻的寄存器中存储的是新任务
的上下文,后置条件被定义为 mac_Status_new,用 G n ,L n 表示窗口寄存器中的新任务的上下文内容,通过函数
sw_aWReg 已经将原任务的使用过的所有窗口寄存器保存到了对应的堆栈之中,所以此时所有的窗口寄存器都
可以被新任务使用.新任务的特殊寄存器的状态被定义为 S n ,内容中全局变量 tcb 中的指针不再指向原任务而是
新任务:
def
mac _ _ post =Status s { 1 ~ 7}∧ G g g L s {CWP l l i o S s {psr ,tbr , , pc ,npc }∧wim M s {nest ,tcb }
,( 0 ~ 7, 0 ~ 7, 0 ~ 7)}∧ i o
def
,( 0 ~ 7, 0 ~ 7, 0 ~ 7)}∧ i o
,
mac _ Status new = { 1 ~ 7}∧ G g g L {CWP l l i o S {psr ,tbr , , pc npc }∧wim M {nest ,tcb }
_
n n n n
定理 1(任务切换异常正确性). 如果有前置条件 P:mac_Status_pre(exce) swflag=1,则通过{S}中的有限步,可
以得到后置条件 Q:mac_Status_new(exce).
下文代码 2 给出了定理 1 在 Coq 中的证明,前置条件即为异常响应时刻的初始状态,被定义为
mac_Status_pre;后置条件即为异常返回时刻的终止状态,被定义为 mac_Status_new.“f0”是异常管理程序逻辑执
行的起始地址,而 exce_design_code 是异常管理在 coq 中的定义.可以通过我们所定义的基本数据类型和遗产管
理逻辑推理公式来证明定理 1 成立.
代码 2. 定理 1 在 Coq 中的证明.
Theorem Switch_Exce_Proof:forall(ex:Exce)(sw:Flags),

{mac_Status_pre (ex)∧(sw=1)}
f0:exce_design_code
{mac_Status_new(ex)}.

Proof.
…
Qed.
定理 2(非切换异常正确性). 如果有前置条件 P:mac_Status_pre(exce) swflag=0,则通过{S}中的有限步,可以
得到后置条件 Q:mac_Status_post(exce).
与定理 1 类似,我们使用了同样的方法对定理 2 进行了证明,如下文代码 3 所示,此处不再赘述.
我们借助于定理证明辅助工具 Coq 对 SpaceOS 异常管理的正确性进行形式化验证,表 1 中给出了我们验
证 SpaceOS 异常管理的 Coq 代码行数统计.