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

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

( S ET = 0) ⇒ _ disable S (ET ≠ exce 0) ⇒ exce _enable
def def
( ) =
() =
_
dis _ Exce S ( S ET ) = 0 en Exce S (ET ) 1
= S
def
+
_TLL = win ) 1, ) where L = (( SCWP W
), )
( ) (( SCWP
W
def
−
), )
W
() (( SCWP
_TRL = win ) 1, ) where L = ( ( SCWP W
3.2 异常管理的状态迁移
本节开展异常管理系统的建模工作.为了对系统进行细粒度的建模,将系统的状态由〈寄存器内容,内存内
容〉扩展为一个五元组:〈G,L,S,M,H〉,G 表示全局寄存器,L 表示当前窗口寄存器,S 表示特殊寄存器,M 代表内存全
局变量,H 代表内存堆栈地址.将异常管理程序逻辑形式化框架建模分为 5 个阶段,分别是异常向量表处理阶段、
上下文保护阶段、ESR 跳转阶段、上下文恢复阶段和异常退出阶段,5 个阶段在时序上是顺序执行的.在每一阶
段中,我们使用结构化的操作语义对其进行建模并勾画出了对应的系统状态迁移图进行对比.
1) 异常向量表处理
异常发生之后,系统会根据 ET 位信息来决定是否对异常进行响应.
• 若系统处于异常屏蔽态,则忽略异常继续维持原本的状态;
• 若系统处于异常响应状态,则会根据不同的异常类型分别进行处理:对于同步异常(陷阱),系统立即进
行响应;对于异步异常(中断),系统执行完当前指令之后才会响应.这种区别也导致中断返回时,需要将
程序计数器指向当前指令的下一条.
系统响应异常后,控制流转入系统内核,首先进入异常向量表中进行基本数据处理,随后正式进入异常管
理,这样做的目的是为所有异常提供一个统一的接口.异常向量表中的操作可以归纳为 3 步:首先关闭异常响应
(dis_Exce),然后将 psr 中的数据存入 l0 之中(save_psr),最后使用 save_pc_npc 将程序计数器 pc 与 npc 存储到 l1
与 l2 中.l1 即是异常处理完毕后的指令返回地址,l2 存储的是返回时的下一条指令地址:
def
save _ pc npc ( , ) =S L ( S pc x ) L ( 1), (l S npc ) x L ( 2)l
_

def
)
save _ psr ( , ) =S L ( S psr x L ( 0)l
异常向量表中系统的状态迁移定义为公式(1)与公式(2),主要涉及寄存器内容的改变,对应的状态迁移图如
图 6 所示.公式(1)中异常响应处于关闭状态,系统不会对异常进行响应;公式(2)中异常响应处于开启状态,控制
流转入异常向量表中执行操作(evt),最终跳转到异常管理入口(exce),此时系统处于异常屏蔽状态,这是为了防
止接下来的上下文保护过程中出现数据丢失的情况:
_
exce _ disable win TR ( )L → abort
(1)
evt (, , )G L S ⇒ abort
( )
_
exce _ enable dis Exce S → S′
( , )S L →
_
_
_
save pc npc ′ ′ ( ,S L′′ ′′ ) save psr ( ,S L′ ′′ ) ′ → (S L′ ′′′ , ′ ) ′ (2)
evt (, , )G L S ⇒ exce ( ,G L S′′′′′ , ′ ) exce disable
_
异常向量表 转入异常
异常响应
操作 管理

Fig.6 Exception vector table processing migration diagram
图 6 异常向量表处理迁移图
2) 上下文保护
进入异常管理首先需要检查是否发生窗口上溢,将检查窗口上溢函数定义为 win_Ovf,特殊寄存器 WIM 指
向已经被系统使用过的窗口,如果接下来要使用的窗口(CWP-1)等于 WIM,系统进行窗口上溢处理,将异常管理
中对窗口上溢的处理函数定义为 save_WF.具体的操作是把需要保存的窗口寄存器 i0~i7 和 l0~l7 中的数据保存