驱动退出的证明：先让活动静止，再归还最后引用

旧 fd 在设备解绑后仍然存在。实例内存可以靠引用保留，但 work、等待者和未来的 DMA / IRQ 是否还会访问它？退出设计需要证明最后一次访问发生在释放之前。

基础寿命章节已经跟踪 probe、open、read、remove 和 release。本章进一步用并发时序检查退出条件，并讨论把软件设备扩展到真实硬件时哪些推论不再成立。

为每种活动写一份访问许可

公开模块 kernel-labs/archlab/archlab.c 包含 misc 入口、open session、delayed work 和等待队列。它没有真实 MMIO、IRQ 或 DMA。

活动	取得许可的方式	退出时怎样撤销或等待
新 open	注册入口，锁内检查 dead	设置 dead，撤销入口
旧 fd 访问	open 持有实例 kref	drain / EOF，最终 close 放引用
生成 work	初始实例引用，锁内检查 dead	同一锁禁止重排，再同步取消
read 等待	session 引用与谓词	dead 后唤醒，重查状态
poll 等待	先注册等待，再判断状态	状态变化唤醒，报告残留可读 / HUP

入口撤销解决“还能不能找到对象”，引用解决“找到以后对象还在不在”。如果查找与取引用并发，必须在持有保护的区间内取得引用，不能先拿到裸指针、解除保护，再尝试补 kref。kref 使用规则

为什么 dead 和重排必须在同一同步关系中

考虑一个错误的变体：work 在锁外检查 dead，而 remove 只设置 dead 后就取消工作。

work                    remove
读取 dead=false
                        dead=true
                        取消当前排队项
把自己重新排队
                        放初始引用

取消操作与重新入队竞争，退出方就没有证明未来不会再执行。当前实现让 work 的 dead 检查、数据生成和重排都在 mutex 内；remove 在同一锁内置 dead，随后在锁外同步取消。

可以分成两种交错：

1. work 先取得锁：完成本轮并重排；remove 随后置 dead，同步取消处理既有执行与排队。
2. remove 先取得锁：dead 已经为真；work 再进入时不再生成和重排。

同步取消的保证仍要求排除其它并发重新入队者。新增 IRQ、定时器或其它 worker 后，要把它们也纳入撤销协议，而不是沿用一条 cancel 就推断全部静止。workqueue 同步取消

为什么不能持着 work 需要的锁等待它

remove：持 mutex → cancel_delayed_work_sync 等待 work 结束
work  ：准备结束 → 等待 mutex

两边都不可能前进。退出协议通常先在锁内撤销许可，再解锁等待活动完成。同步等待结束后，才能回收活动依赖的存储。

这与用户态 owner 的停止有相同结构：先关闭 admission，再让剩余活动走到明确终态，外部等待者最后销毁。共同思想不代表可以把 Linux workqueue、线程 join 与硬件停止封装成同一个无条件 stop 调用。

wait 与 poll 也要证明不会漏掉退出

read 的等待条件是 count != 0 || dead。唤醒只提示重新检查谓词；拿到锁以后仍可能发现数据已被其它读者取走。

poll 先 poll_wait 登记等待，再在锁下判断可读与 dead。若先看状态、解锁后才登记等待，状态可能在两步之间改变并完成唤醒，等待者就可能错过这次变化。

设备 dead 且还有记录时，可以同时表现为可读和 HUP；旧 fd 先读残留数据，队列空以后读到 EOF。HUP 不等于应用应该立即丢掉全部数据。是否 drain 是接口决定，必须与调用者的读取策略一致。

copy_to_user 放在哪里，也影响退出成本

当前模块在 mutex 内复制一条固定记录到用户缓冲。优点是队列头与复制结果保持简单的事务关系，复制失败不会消耗该记录。代价是用户页访问可能阻塞，生成、其它读者和 remove 都会等待同一锁。

若目标要求缩短临界区，不能只把 copy_to_user 移到锁外。要先回答：记录何时消费，两个读者能否拿到同一条，复制失败是否返还，顺序如何保持，等待期间谁持引用？

一种候选是先保留记录和 session 状态，释放全局队列锁，完成用户复制后再提交消费或回滚。它增加了预留状态、并发消费者规则和退出时的在途复制集合。另一种是接受复制失败会丢记录，并把这一行为明确写进接口。选择由数据语义和时延要求决定，而非只比较锁持有时间。

这两种变体尚未实现。当前教学模块不能据其小记录复制，推导面对任意用户缓冲时 remove 都有固定上界。

真实硬件退出是依赖关系，不是一张通用调用顺序

给模块加入 IRQ 和 DMA 后，需要额外证明：设备不再发起新传输、正在使用的内存已不再由设备访问、IRQ handler 和后续 bottom half / work 已静止，然后才解除映射与释放 buffer。

禁止新软件提交
    → 驱动与设备协议决定怎样停止 / 取消在途操作
    → 不再产生新的硬件完成与后续工作
    → 同步已经进入的 handler / work
    → 解除 DMA 映射，归还 buffer，释放设备资源

这是需要落实的依赖关系，具体顺序由控制器定义。有的设备需要保留完成中断来结束当前传输，有的需要 reset 确认 DMA 已停；先屏蔽 IRQ 后等待一个只能由 IRQ 发出的完成信号，会形成另一个死锁。

DMA 映射与 CPU / 设备之间的同步也遵守 API 的所有权规则。引用保留的是软件对象，并不能禁止设备继续写已经归池的内存。DMA API 指南

退出验证要覆盖哪些交错

已有专用 QEMU 实验覆盖软件设备的持 fd 解绑、阻塞读取唤醒、poll、多实例、故障注入与引用收尾。记录日期与实际范围见 验证页。

进一步的设计验证应按活动列出交错：

交错	要证明的结果	当前证据边界
work 刚准备重排时 remove	dead 后不产生未来 work	当前锁关系可静态推演，历史软件实验支持退出路径
多个 read / poll 与 remove	不丢退出唤醒，数据规则一致	需按读者负载扩大定向对照
用户复制长时间等待	不提前释放；退出诊断可解释	尚无受控页故障停顿实验
IRQ / DMA 完成与 reset	设备最后访问先于 buffer 回收	软件设备没有这些硬件证据

架构评审的输出应包含访问者清单、撤销许可、同步点、最后引用与失败行为。仅有一段“调用 cancel 后 free”的代码，还不足以证明整个设备退出。