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

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

N
恢复上下文 窗口下溢? nest减1 还原psr 打开中断
Y
下溢处理 异常退出

Fig.10 State transition diagram of abnormal exit phase
图 10 异常退出阶段状态迁移图
其中,
• 公式(11)中,发生窗口下溢,异常管理进行下溢处理,左移寄存器窗口,还原堆栈中内容;然后右移寄存器
窗口,调整 WIM 的指向,嵌套层数减一,改变内容中的全局变量 nest,还原 psr,保持退出时程序状态寄存
器与进入异常时的状态一致;最后开打异常,使系统可以正常响应异常,最后异常退出;
• 公式(12)中,窗口下溢不发生,则直接跳过下溢处理,执行后续的操作.

4 实例验证
本节使用前文描述的形式化验证框架对北斗三号 [18] 在轨实际应用的航天器实时操作系统 SpaceOS 异常
管理功能的正确性进行证明,SpaceOS 是我国第 1 个自主研发并进行空间飞行的航天器嵌入式实时操作系统,
系统资源占用低、实时性强,具有多任务并发、中断频发等特点,主要功能包括内存管理、异常管理、任务管
理、IO 管理等.如图 11 是北斗三号任务实际运行情况,一个控制周期中包含 6 个控制任务、两个异常嵌套、6
次异常中任务切换.任务 1 运行时被异常 A 打断,高优先级异常 B 打断 A 的处理过程并启动任务 2,异常 A 在上
下文恢复阶段将任务 2 设为就绪态;异常退出时,处理器执行任务 2;任务 2 执行完毕后再次进行任务切换,执行
任务 3.以此类推,当任务 6 执行完毕后,通过异常 G 将处理器分配给任务 1 继续执行.

控 B
制 A A C D E F G
流
异常
T6
T5
T4 任务
T3
T2
T1 T1
0ms 100ms 时间
Fig.11 Beidou 3 mission operation example
图 11 北斗三号任务运行实例
程序逻辑是描述和论证程序行为的逻辑,程序和逻辑有着本质的联系,如果把程序看成一个执行过程,程序
逻辑的基本方法是先建立程序和逻辑间联系的形式化方法,然后建立程序逻辑系统,并在此系统中研究程序的
各种性质.在此给出异常管理程序逻辑的数学规范——P{S}Q,其中,
• S 代表程序逻辑,由第 3 节中介绍的 12 条公式组成;
• P 和 Q 是有关程序变元的逻辑表达式,P 称为前置条件,表明执行程序逻辑之前程序变量应具有的性
质,可看作程序正确执行的前提;Q 称为后置条件,刻画了语句结束执行时的系统状态,可以看作 S 应实
现的逻辑结果.
然后对异常管理的前置条件和后置条件进行分析与刻画,根据异常管理中是否会产生任务切换分为两种
情况.
• 当 ESR 中含有任务的启动或停止操作时会产生任务的切换,异常退出时,寄存器中的内容是新任务的
上下文数据,由 switch_Ts 函数实现;并且需要将原任务使用过的所有寄存器窗口都保存到堆栈之中,由
rest_WF 函数实现;