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

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

| (cap_type, (x, y, z)) =&
let (b, i) := l in
PV (b, i)@Tint32 | → (Vint32 cap_type) **
PV (b, i + 4) @ Tint32 | → Vint32 x **
PV (b, i + 8) @ Tint32 | → Vint32 y **
PV (b, i + 12) @ Tptr Tvoid | → z
end
需要说明的是, CSL-R 不允许一块内存上同时存放不同类型的数据, 这与 C 语言中 union 的定义不同. 所以在
定义 Cap 断言的时候, 我们将 category 和 object 的第 2 分量 (第 1 分量类型相同) 分开定义. 上述定义如果适用于
category 权能, 那么 (x, y) 构成有效值对, z 为无效值; 如果适用于 object 权能, 那么 (x, z) 构成有效值对, y 为无
效值.
至此为止, 我们定义了系统的权能数据结构. 它由多个数组、结构体、联合体嵌套而成, 中间还包括权能有关
的基本数值. 前面我们提到, CSL-R 中提供了结构体和数组的一般性递归断言. 然而, 为了证明更加容易进行, 我们
将权能有关的各个结构体和数组定义为具体的断言, 从而在证明时可以根据断言的具体情况进行权能数据结构的
展开和合并, 来完成断言中权能的修改.
除了权能空间数据结构的断言, 我们还定义了与权能有关的其他断言, 来记录权能空间链表、各任务的父任
务信息以及权能空间的空闲槽 slot 信息.
以上我们描述了操作系统内核权能模块底层实现的权能数据结构. 相对应地, 我们将底层权能数据结构抽象
化, 定义高层的抽象数据状态 acspace, 类型为任务优先级到三元组的映射, 如下所示.
priority → ((list slot_val_type) * (list childs) * parent),
其中, 三元组包括: 该任务所有 slots 中存储的权能值构成的链表, 每个权能值定义和底层一致, 包括 slot 类型, 权
能类型和权能的取值; 该任务所有子任务构成的链表 childs; 以及该任务的父亲 parent. 与底层相比, 具体的数据结
构实现被抽象, 而保留了权能值以及任务之间的父子关系的信息.

4.2 权能全局不变式
权能的全局不变式描述与权能有关的所有共享资源, 以及不同资源之间的一致关系、底层和高层资源之间的
一致关系. 以下 CapabilityInv 定义了权能不变式, 其中高层抽象状态 acspace 作为不变式的参数, 用于与其他功能
模块内核层面的交互. 前两行的断言描述了底层的权能数据结构, Hcapspace 描述高层数据状态, 其余纯断言公式
定义一致关系.
Definition CapabilityInv acspace :=
EX l ptrvl vl cspacels pl objvl,
CSpacePrioTbl l ptrvl vl cspacels ** CSpaceObjectPointer objvl **
//分别为任务权能空间指针数组和任务权能空间 slot 空位置的数组
CSpaceCapParent pl ** CSpaceGVars ** // 任务父亲信息数组, 权能全局变量
Hcapspace acspace ** //高层权能数据状态
[|RL_consistent(ptrvl, pl, vl)|] ** //底层各数据结构之间的一致性
[|RLH_consistent(ptrvl, vl, acspace)|] **//底层和高层数据状态的一致性
[|capability_wellform_descendents vl cspacels|].
最后一个断言表示, 每个权能节点与其后代子孙节点无环, 构成树状结构. 这既符合权能模块的设计需求, 又
保证了递归操作的可终止性. 由于全局不变式定义内核共享资源, 因此只有在临界区内可以展开, 否则是保持封闭
的形式, 也就是 CapabilityInv acspace.