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

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

也将导致窗口的切换.图中右上角的 WIM 寄存器用来表示每个窗口被使用的状态,每个窗口在 WIM 中对应 1
个 bit 位.当寄存器窗口都被使用时,如果再发生一个额外的 SAVE 指令则会超过窗口的容量,此时将触发一个窗
口寄存器溢出陷阱;与之相反,当发生 RESTORE 或 RETT 指令时,如果 WIM 寄存器对应 bit 位无效,此时将触发
一个窗口寄存器下溢陷阱.

Fig.5 SPARC window register
图 5 SPARC 窗口寄存器

异常管理涉及的内存内容的改变由两部分组成:一是内存中的全局变量,二是内存堆栈.我们使用 M 来表示
内存中的全局变量(MemoVar):
(MemoVar ) M :: nest tcb ossm swflag= | | |
(TcbAddr ) tcb :: CurTcb PreTcb= |
O =
(Offset ) :: 0| 4| 8 |...|128
(HeapStack H O∈→ sp , where sp = L o
( 6)

)
其中,
• nest 表示异常嵌套次数;
• tcb 表示任务控制块指针,由 CurTcb 与 PreTcb 组成:前者指向当前运行任务的 Tcb 地址,后者指向前一
个任务运行的 Tcb 地址.当任务发生切换时,会使用它们;
• ossm 表示异常信号表,异常信号表中保存着系统中所有异常处理函数的入口地址;
• swflag 用来判断 ESR 中是否发生了任务切换:若其值为 1,则发生任务切换;否则不发生;
• H 表示异常管理中使用到的内存堆栈地址;
• sp 表示栈顶指针,在 SPARC 中,使用当前窗口寄存器的 o6 表示 sp 的值;
• O 则表示异常管理中系统设置的地址偏移量.
计算机的运行过程中,系统的某些状态根据寄存器中内容的变换而改变,需要对这些状态进行形式化描述.
程序状态寄存器中的 ET 位为 0 时,系统进入异常屏蔽状态;否则,系统正常响应异常.除了状态的定义,我们对异
常管理中使用的一些基本操作在此进行定义,如打开异常响应(en_Exce)、关闭异常响应(dis_Exce)、寄存器窗
口左移动 win_TL(L))、右移 win_TR(L)等: