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

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

时对 safe 代码部分进行抽象规约. 建立两类形式化之间的接口, 接口的定义会在第 4.3 节详细阐述. 本节整体的验
证方案如图 1 所示.

Arc::clone Mutex::new Mutex::get_mut …
unsafe 代码块

get_ref_count get_ownership transfer_ownership …

GhostArc::get_ref_count GhostArc::get_ownership GhostArc::decrease_ref_count …

safe代码 set_current_thread scheduler clear_current_thread …

方案图
示说明
调用 抽象 接口 GhostFunc形式化代码 形式化代码 内核代码
图 1 整体验证方案

GhostFunc 为 safe 代码块和 unsafe 代码块的验证代码提供了连接的接口, 使得验证更具模块化. 在保证验证
细粒度的同时也降低了验证的复杂性. 验证过程细节会在后续章节详细介绍.

4.1 任务管理 unsafe 代码段形式化
本节将对内核中 unsafe 代码段进行形式化建模. 任务管理与调度模块代码 (包含数据结构以及标准库) 共
473 行代码. 其中代码来源如表 1 所示.

表 1 模块代码统计

代码来源 行数
alloc::sync::Arc 91
alloc::sync::Weak 11
spin::sync::Mutex 46
spin::sync::rwlock 9
core::sync::atomic 4
core::ptr::read 49
core::ptr::write 38
core::slice 17
arch64 (非标准库) >100