Page 157 - 《软件学报》2025年第8期

3580 软件学报 2025 年第 36 卷第 8 期

数 class 的值进行索引并打开 (unfold) 断言, 直至到达该参数对应的 Cap 断言. 按照代码实现, 对 Cap 断言中的各
个权能参数进行修改. 所有操作完成后, 需要建立后条件, 而为了得到以上规范定义的后条件, 我们需要再按照反
着的顺序, 将断言进行逐层的合并 (fold), 重新得到断言 CSpacePrioTbl. 以上的证明过程非常复杂, 我们主要使用
了以下两类引理 (这两个引理表示打开权能结构第 1 层, 到达断言 CSpace).

Definition CSpacePrioTbl_unfold_any_idx:=
forall s l ptrvl vl cspacels i,
i < len (ptrvl) →
s ⊨ CSpacePrioTbl l ptrvl vl cspacels →
s ⊨ CSpacePrioTbl l1 ptrvl1 vl1 cspacels ** CSpace ptr v ** CSpacePrioTbl l2 ptrvl2 vl2 cspacels
** [ptrvl = ptrvl1 ++ ptr::ptrvl2|] ** [|vl = vl1 ++ v::vl2|]**[|length ptrvl1 = i/\length vl1 = i|]

Definition CSpacePrioTbl_fold_any_idx:=
** [ptrvl = ptrvl1 ++ ptr::ptrvl2|] ** [|vl = vl1 ++ v::vl2|]**[|length ptrvl1 = i/\length vl1 = i|]
i < len (ptrvl)→
s ⊨ CSpacePrioTbl l1 ptrvl1 vl1 cspacels ** CSpace ptr v ** CSpacePrioTbl l2 ptrvl2 vl2 cspacels
** [ptrvl = ptrvl1 ++ ptr::ptrvl2|] ** [|vl = vl1 ++ v::vl2|]**[|length ptrvl1 = i/\length vl1 = i|]→
s ⊨ CSpacePrioTbl l ptrvl vl cspacels

其中, s ⊨ P 表示断言 P 在状态 s 下成立. 以上引理中, CSpacePrioTbl_unfold_any_idx 是将权能指针数组 ptrvl 和权
能值数组 vl 根据下标 i 分成 [0, i–1]、[i:i] 和 [i+1, len(ptrvl)–1] 这 3 段, 其中 [i:i] 为访问的权能空间, 其对应的指
针为 ptr, 对应的值为 v. 展开的效果是, 前后两端仍旧是权能指针数组, 而中间为一个权能单点节点, 由 CSpace 断
言表示. 然后接着继续展开 CSpace 的结构, 一直到 Cap 结构, 这里我们省略了 CSpace 断言之后的展开过程.
CSpacePrioTbl_fold_any_idx 是 CSpacePrioTbl_unfold_any_idx 的逆过程, 用于将展开的断言合并回去, 确保函数执
行前后断言的一致性, 保持资源的良构性.

4.3.2 cnode_revoke 的建模、规范和验证

4.3.2.1 接口函数 cnode_revoke 的功能和形式模型
函数 cnode_revoke 的主要功能是, 撤销给定任务所对应的权能节点及其后代的对应权能节点. 具体来说,
cnode_revoke 调用内核函数 cnode_revoke_kernel 进行权能撤销操作.
cnode_revoke 函数代码首先检查优先级 prio 是否越界, 如果越界了返回 err, 表示 revoke 操作失败. 若 prio 范
围没有越界, 则调用内核函数 cnode_revoke_kernel, 尝试对于 prio 任务对应的权能节点 CSpacePrioTbl[prio] 及其
后代节点进行相应的权能撤销操作, 并且将返回值存放在局部变量 z 中. 如果 z 的值是 success 表示撤销操作成功,
则 cnode_revoke 返回 revoke_success; 否则 cnode_revoke 返回 revoke_failure.

实现 1. 函数 cnode_revoke 代码.

Int cnode_revoke(Int8u prio, Int8u type, Int8u capability)
{
1. Int8u z
2. if(prio>=lowestprio){
3. return err;
4. }
5. …
6. z = cnode_revoke_kernel(prio, type, capability);