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

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

保其排他性. 第 5 个算子表示锁的状态分为 3 种: 开放状态, 半开放状态和关闭状态, 半开放状态锁的状态数组中
所有位置均为 false. 这个不变式确保了锁在各种操作 (如获取和释放) 中的正确性和一致性. 可以看以下例子理解
详细过程.
假设锁的容量为 3, 当前状态如下.
● o= 0, 表示当前锁的持有者位置.
● i = 2, 表示有两个线程在等待队列中.
● xs = [true, false, false], 表示锁的状态数组.
在这种情况下, 不变式 lock_inv 确保:
● 锁的状态数组长度为 3.
● key 值 nextPtr 存储的值为 0 + 2 = 2.
● 锁的状态数组 arr 存储当前状态 [true, false, false].
● 锁的拥有者是位置 0, 当前的队列范围是 [0, 2).
● 锁的状态为开放状态, 即 xs = list_with_one(3, 0).

4.3.2 任务管理与调度模块建模
在任务管理与调度模块, 某内核主要涉及一个主循环, 所有的调度等操作都存在于主循环中, 调度器中包括 3
个函数.
(1) set_current_thread: 选择线程队列中的第 1 个 Ready 线程作为当前线程, 无可用线程时进入待机等待中断.
(2) run_current_thread: 循环调用 thread 的 run 函数执行当前线程, 线程执行中遇到系统调用、中断、异常后
run 函数退出, 再调用 handle_user_trap 函数处理陷入内核原因. 完成处理后根据线程状态进行不同处理:
● Ready: 处理完当前陷入线程可继续执行.
● Wait: 线程执行异步等待系统调用陷入内核, 在内核中被设为 Wait 状态.
● Suspended: 线程运行时遇到时钟中断陷入内核, 线程时间片用完时被设为 Suspended 状态.
● Exit: 线程执行 ky_proc_exit 系统调用陷入内核, 在内核中被设为 Exit 状态.
(3) clear_current_thread: 根据线程状态清除当前线程.
● Suspended: 说明线程已经经历了中止, 将状态改回 Ready, 再重新加入队尾.
● Wait: 将在协程函数中将状态改回 Ready (后续章节介绍), 再重新加入队尾.
● Exit: 说明线程已终止, 无需加入队尾, 此时需要根据终止的线程是否为根线程, 进行相应的清理操作.
在内核主循环的最后, 循环依次调用上述 3 个函数. 当线程队列为空时, 系统进入待机. 每次调用完 3 个函数
后, 执行一次协程调度器.
我们的建模是从代码层面上建模的, 下面介绍线程状态清除的建模. 其余建模与此类似.
对于 clear_current_thread, 并且在仅考虑 GhostArc 的情况下, 在执行前的状态确定如下, 表示当前必须要有一
个正在运行的线程.

pre_clear_current_thread(s) := ∃t, s.current_thread = Some(t).
在执行后状态确定为:

post_clear_current_thread(s) := ∃t, s.current_thread = Some(t)∧
(match t.state with

′
|Suspended => s .suspended_queue = t :: s.suspended_queue∧ s .current_thread = None∧update_ref_count(s, s )
′
′

′
′
|Wait => s .wait_queue = t :: s.wait_queue∧ s .current_thread = None∧update_ref_count(s, s )
′

′
|Exit => s .current_thread = None∧remove_re f_count(s, s )
′

′
|Ready => s .ready_queue = t :: s.ready_queue∧ s .current_thread = None∧update_ref_count(s, s )
′
′
end)