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

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

予了极大的重视.文献[10]中,作者提出了基于投影时序逻辑(PTL)的定义,并将这种定义推广到包含任意多中断
事件的中断系统上,同时使用投影时序逻辑定义的基本中断语句扩充建模仿真和验证语言(MSVL),并扩展了
MSVL 语言的解释器,使其可以对嵌套中断系统进行建模仿真和验证.在文献[3]中,作者针对外部设备为
CertiKOS 带来的异步异常(中断)开展了形式化验证工作,构建了“虚拟”设备对象进行驱动程序验证,并使用了
一种抽象中断模型,试图解决代码验证中由于中断而导致的不确定性.文献[11]中,作者利用多线程系统验证的
方法来验证中断系统.由于中断缺乏形式化语义支持,所以使用该方法时,将中断的语义用等价的线程语义进行
形式化描述.然而,中断和线程之间精细的差别,使得用线程语义描述中断这个过程变得棘手.文献[12]利用时间
Petri 网建模嵌套中断系统,并将 Petri 网所建立的系统模型转换为时间自动机,从而借助时间自动机理论进行模
型检测.文献[13]中,针对于中断驱动系统中容易产生的时序错误,作者使用时间自动机对中断事件以及中断处
理过程进行建模,并使用模型检测技术来进行可达性分析.
但遗憾的是,目前大部分关于异常的形式化研究,都是基于外部设备产生的异步异常(中断)带给操作系统
的不确定性问题和时序问题为焦点来开展的,并没有对操作系统异常管理本身的正确性进行验证.本文重点关
注实时操作系统异常管理功能的逻辑正确性,主要面临以下难点.
• 异常根据触发条件可分为同步与异步异常,面对两种不同类型的异常,异常管理功能的执行逻辑也不
尽相同,两种不同的系统状态都需要进行考虑;
• 实时操作系统的内核可抢占特性,导致系统不仅仅要面对最基本的异常响应情况,还需要考虑异常嵌
套、异常处理子程序(ESR)中发生任务切换 [14] 的情况;
• 面对基本异常的响应,异常管理在进行上下文保护和恢复的过程中,上下文内容始终保持一致.面对含
有任务切换异常的响应,进行上下文恢复操作时的上下文内容已经发生了变化,在形式化建模过程中,
需要对其进行全面覆盖.
针对以上难点,本文提出一种基于 Hoare-logic 的验证框架,用于证明面向 SPARC 处理器架构操作系统异常
管理的正确性.第 2 节介绍操作系统的异常控制流和实时操作系统可能发生的 3 种异常的情况.第 3 节详细介
绍异常管理验证框架的形式化建模工作,并且给出解决以上 3 个难点的详细方案.第 4 节借助半自动化证明工
具 Coq,使用该验证框架对实际应用在北斗三号航天器系统上的 SpaceOS 操作系统异常管理的正确性进行验
证.最后一节总结全文,并对未来研究提出进一步的展望.
2 基础知识

本节对基础知识进行介绍,其中,第 2.1 节对异常执行流以及实时操作系统面临的 3 种异常情况进行介绍,
第 2.2 节对半自动化证明工具 Coq 进行介绍.
2.1 实时操作系统异常处理

现代计算机系统通过使控制流 [15] 发生突变来对某些突发情况做出反应,一般而言,我们把这些突变称为异
常控制流(exceptional control flow,简称 ECF).异常控制流发生在计算机系统的各个层次,比如:在硬件层,硬件检
测到的事件会触发控制突然转移到异常处理程序;在操作系统层,内核通过上下文切换控制一个用户任务转移
到另一个用户任务;在应用层,一个任务可以发送信号到另一个任务,而接收者会将 CPU 控制权突然转移到它的
一个信号处理程序.异常是异常控制流的一种形式,对它的管理一部分由硬件实现,一部分由操作系统实现.由
操作系统实现的这一部分即为异常管理,由于和硬件密切联系,对于操作系统的异常管理设计将随硬件平台的
不同而有所不同.异常根据触发事件的不同,一般被划分为两类:同步异常与异步异常.前者是执行一条指令的
直接产物,通常被称为陷阱;后者则是由处理器外部 IO 设备产生,也被称为中断.
系统中可能发生的每一种类型的异常都被分配了唯一的非负整数种类的异常标号,其中一些标号是由处
理器的设计者分配的,例如被零除、内存地址未对齐、窗口上溢等;其余的标号则是由操作系统的开发者进行
分配,例如系统调用、任务切换和响应外部 IO 信号等.计算机启动时(重启或加电),操作系统会分配和初始化一
张称为异常向量的跳转表 [16] ,这张表中包含异常标号和对应的跳转地址.当系统在执行某个程序时,若处理器检