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

马智 等:面向 SPARC 处理器架构的操作系统异常管理验证 1635

常管理对任务 i 的上下文进行保护,随即执行 ESR1;ESR1 执行过程中,将更高优先级的任务 y 设置为就绪态,执
行完毕后返回异常管理;异常管理接收到任务切换的信号,将任务 y 的上下文信息拉取到寄存器中再退出异常
管理,此时 CPU 被任务 y 抢占,所以系统会执行任务 y 而不是任务 i;当任务 y 执行完毕之后,调度器触发任务切
换异常,进入异常管理中再次进行任务调度,ESR2 结束后返回异常管理进行任务切换,此时,恢复的上下文才是
任务 i 中被保存的信息;最后退出异常管理,任务 i 继续执行.

内 异 保护 ESR1 恢复 保护 ESR2 恢复
核 常
层 向 ESR1中接收到 ESR2中接收到
量 任务切换信号 异常返回后 任务i切换信号
表 任务y被执行
用
户 任务i 任务y 任务i继续
层
异常响应 开始 结束 异常返回
Fig.4 Task switching of exception
图 4 异常中发生任务切换
2.2 Coq形式化证明工具

Coq 是法国国家科学研究中心等机构研发的交互式定理证明辅助工具 [17] ,形式化研究人员可以使用它来
表示规范说明,开发满足规范说明的程序.Coq 非常适合于开发那些在金融、医疗、航空、航天等领域需要绝对
可信的程序,这些领域中的程序需要严格地符合规范说明,需要对这些程序进行形式化验证.Coq 系统提供了一
种具有很强表达能力的逻辑,通常被称为高阶逻辑.Coq 系统也可以被用作一个逻辑框架,在该框架下,我们可以
为新的逻辑提供公理,并基于这些逻辑来开发证明.
Coq 的规范说明语言 Gallina 可以描述程序设计语言中的常用类型和程序.一个标识符的类型通常由声明
和一些规则来描述,后者使用类型规则从较简单的类型出发构造符合类型,每个类型规则表达了类型的子部分
同类型结构之间的联系.比如,在 Coq 中使用“Inductive”来归纳定义一种类型,归纳定义需要一个名称、一个类
型、零个或多个规则来定义一个归纳类,每个规则都具有单独的名称,称之为“构造器”.如下文代码 1 所示,这是
对于自然数的定义,其中:O 是一个自然数;S 是一个构造器,它需要一个自然数作为输入,输出则为自然数.其规
则为:若 n 是一个自然数,那么 S n 同样为自然数.

代码 1. 在 Coq 中定义自然数
Inductive nat:Type:=
|O
|S(n:nat).

在 Coq 中,计算是通过对验证对象进行连续规约,直到得到一个不能归约的形式来完成的.因此,Coq 中计算
总是可终止的(强正规化).可计算性方面的经典结论表明:一个可以描述所有可计算函数的程序设计语言的一
个基本性质就是,必须对包含不停机函数的描述.所以,一些可计算函数能够在 Coq 中表示,但是并不可以通过归
约机制执行.尽管有这些限制,Coq 的类型系统还是十分强大的,它是描述可计算函数的一个很大的子类.因此,
要求强正规化并不会显著地减弱它的表达能力.计算机辅助定理证明工具是一个大家族,除了 Coq 之外,还有很
多享有盛誉的工具,如 Automath,Nqthm,Mizar,LCF,Isabelle 等.我们之所以选择 Coq,是因为它具有一个与众不同
的特性——可以从证明中生成可靠的程序和模块.
3 框架建模

第 2 节介绍了系统异常处理的 3 种需求,本节开展实时操作系统异常管理验证框架的建模工作.在计算机
系统中,CPU 提供了运行动力,这种推动力最直接地体现在指令寄存器的改变上.当计算机上电后,复位逻辑电