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

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

内容也转变为了新任务的上下文.
这一阶段重点关注发生任务切换时,异常管理的处理情况.系统根据全局变量 swflag 来判断 ESR 中是否发
生了任务切换:若其值为 1,则发生任务切换;否则结果相反,将其状态表示定义为 SW.我们将寄存器窗口保存定
义为 sw_aWReg,保存被打断的任务所使用过的所有寄存器窗口.这里以一个具体的例子进行说明:假设 CWP 此
时指向窗口 4,WIM 指向窗口 7,则说明任务使用过的窗口为 4~6.保存上下文过程中,save_Reg 已经将窗口 4 的
内容存放到了任务堆栈之中,所以此时 sw_aWReg 只需要保存窗口 5 和窗口 6.具体的操作如以下公式所示:
def true, if swflag = 1
⎧
=
SW ⎨
⎩ false, if swflag = 0
def
switch _Ts (M L sp
, ) = CurTcb x
⎧
def true ⎧ if 4 1 7
+≠ g
g
Wim _Cwp G S let CWP x g 4,WIM x g 7 in ⎨
( , ) = ⎨
+=
g
⎩ false ⎩ if4 1 g 7
def
i
li
G g
( , , ) = H sp
g
L
rest _ Reg G L H { ,(0 ~ 8,32 ~ 60,64 ~ 88)}x [ { 0 l ~2, 0 ~ 7}, { 1 ~ 7}]
+
W
⎧ let ( ) =winTL L ( ( S CWP ) 1, ) in
⎪
def ⎪ let sp + 128 in
⎪
o l
sw _ aWReg G L S H ⎨ (0 ~ 7, 0 ~ 7, 0 ~ 7) x
l i
( , , , ) = Lo
i
⎪ =
{ ,(0 ~ 28,32 ~ 60,64 ~ 92)}, if Wim Cwp
⎪ Hsp _ true
⎪ , if Wim Cwp = false
⊥
_
⎩
当 Wim_Cwp 的状态为 true 时,将窗口左移即 CWP 加 1,随后保存当前窗口的所有内容到对应的内存堆栈
之中,全局寄存器的内容通过 save_Reg 已经被保存,所以可以通过全局寄存器来充当数据交换的中介;当 Wim_
Cwp 状态为 false 时,说明使用过的寄存器窗口已经全部保存完毕.要注意的是,窗口 4 的恢复机制与窗口 5、窗
口 6 不同:窗口 4 会在异常管理恢复上下文的过程中进行处理;窗口 5 与窗口 6 则在此任务继续执行以后,发生
窗口上溢时在上溢处理中恢复内容.保存原任务使用过的寄存器窗口之后,接下来需要考虑将新任务的上下文
恢复入寄存器中.在 ESR 处理过程中,系统的 Tcb 指针已经指向了新任务地址,也就说,CurTcb 已经发生了改变,
这也是为什么我们要在上下文保护阶段中备份 CurTcb 的原因.如果要恢复新任务的上下文,则需要将 CurTcb
中的地址信息存储到 sp 寄存器中,然后再进行恢复操作,将其定义为 switch_Ts.恢复寄存器上下文为保护上下文
save_Reg 的逆函数,定义为 rest_Reg.
我们使用公式(8)~公式(10)来表示图 9 中的状态迁移过程:
′
′ ′
_
exce _ enable dis Exce ( )S → S exce _ Nest = false rest Reg ( , , )G L H → ( , , )G L H
_
(8)
′′
′
exce (, , ,G L S M , )H ⇒ ( , , ,G L S M , ) H exce _ disable
′ ′
exce _ enable dis Exce ( )S → S′ exce Nest = _ true SW = false rest Reg ( , , )G L H → ( , , )G L H
_
_
(9)
′
′′
exce ( , , ,G L S M ,)H ⇒ ( , , ,G L S M ,) H exce _ disable
( ) →
exce _ enable dis Exce S ′ S exce _ Nest = true SW = true ⎫
_
⎪
, ′
′′
, ′
, ′
( , , , ) →
( , ′ ′′ L H
′ sw
,L
G
, ) ′ → G L
_
_ aWReg G L S H ( , , ′′ S H ) switch Ts (M L (M L ) ′ restReg G , ′ ) → ( ′′ ′′′ H ) (10)
⎬
, ′
, ′′
exce G L , ) ⇒H ( ′′ ′′′ S M H ) exce disable ⎪ ⎭
,L
_
(, , , S M
,
G