交付一份截止期可调度性证书
从作业窗到截止期证书路线最后交付的不是“CPU平均还很空”这一句话，而是可逐项复算的任务合同、需求表、执行表和失败窗口。下载标准库核验器；普通运行与python -O都执行显式检查并把JSON写到标准输出，没有外部依赖或网络操作。
一、先冻结允许的工作
时间单位自定为毫秒，单核每毫秒交付一毫秒服务；允许任意时刻抢占，暂不计开销。所有作业释放后可立即运行，不自挂起、不等待锁。任务表按(C,D,T)为A=(1,3,4)、B=(2,5,5)、C=(2,7,10)。
记录中要写明：T是最小到达间隔，实际需求不超过C，deadline等于释放加D。只有同步示例按周期到达；全任务集保证还覆盖间隔更长、各任务首次释放不同步的允许输入。
同步释放表从0开始，取[0,20)中的十一份作业。A的释放为0、4、8、12、16，对应deadline为3、7、11、15、19；B的释放为0、5、10、15，对应5、10、15、20；C的释放为0、10，对应7、17。每份服务取任务的C。
实际机器是否确有这些执行上界，是证书的外部前提。附件没有测量WCET、缓存、时钟或中断，也不替真实系统给出安全认证。
二、用有限检查点覆盖全部窗口
H=lcm(4,5,10)=20，U=17/20。填写并核对：
| t | A份数 | B份数 | C份数 | 必须完成的需求 | 余量t−需求 |
|---|---|---|---|---|---|
| 3 | 1 | 0 | 0 | 1 | 2 |
| 5 | 1 | 1 | 0 | 3 | 2 |
| 7 | 2 | 1 | 1 | 6 | 1 |
| 10 | 2 | 2 | 1 | 8 | 2 |
| 11 | 3 | 2 | 1 | 9 | 2 |
| 15 | 4 | 3 | 1 | 12 | 3 |
| 17 | 4 | 3 | 2 | 14 | 3 |
| 19 | 5 | 3 | 2 | 15 | 4 |
| 20 | 5 | 4 | 2 | 17 | 3 |
每项份数是max(0,⌊(t−D)/T⌋+1)。还要写出两步覆盖理由：需求函数只在D+kT跳升；D≤T和整数周期使dbf(t+H)−(t+H)=dbf(t)−t+H(U−1)。U≤1时后续超周期不比第一个更危险。因此这九行加模型条件给出全偶发到达的EDF保证，而不只是解释一次同步模拟。
预算不足是第三种结果。试把周期改成101与103，并限制最多生成10个候选点，下载器输出UNKNOWN。这个出口没有宣告可行，也没有给不可行证书。若参数使U>1，直接在H给出超载需求，则无需先枚举整个超周期。
三、提交一条可以验真的EDF服务表
破同deadline采用A、B、C次序。EDF同步表如下，A₁表示A的第二份作业，编号从0起。
| 半开区间 | 实际CPU服务 |
|---|---|
| [0,1) | A₀ |
| [1,3) | B₀ |
| [3,4) | C₀ |
| [4,5) | A₁ |
| [5,6) | C₀ |
| [6,8) | B₁ |
| [8,9) | A₂ |
| [9,10) | 空闲 |
| [10,12) | B₂ |
| [12,13) | A₃ |
| [13,15) | C₁ |
| [15,16) | B₃ |
| [16,17) | A₄ |
| [17,18) | B₃ |
| [18,20) | 空闲 |
逐作业累计服务必须恰为C；任何段不能早于对应释放，不能两份同时运行。C₀在6完成，C₁在15完成；十一份全部在各自deadline之前或恰在deadline完成。总服务17、空闲3，总窗口20。
这张表展示政策选择；上一节的有限判据才把结论扩展到所有允许输入。例如把A的后续释放8、12、16一起顺延为9、13、17，间隔变成5、4、4，仍满足T_A=4；那条轨迹需要重新执行，不能把旧完成时间直接搬过去。若只改8→9却保留后继12，间隔3已经违反原合同。
四、同输入换成固定任务优先级
固定A>B>C。A的迭代为1→1；B为2→3→3；C为2→5→6→8。最后一步因为6的窗口里有两份A与两份B，得到2+2×1+2×2=8，超过D_C=7，算法立即停止并给出失败。
执行轨迹最关键的变化在5：B₁虽然deadline10，比C₀的7晚，但固定优先级仍让B₁在[5,7)运行。C₀只已得到[3,4)的一单位，截止点7时还剩1，最终在8完成。记录“7时未完成”与“8时最终完成”是两个不同事件。
把C的D改成9，C迭代再增加8→8，保证变成成功；C的C与T都没变。再试两任务(2,5,5)、(4,7,7)：EDF利用率34/35且可行，固定较短周期优先的第二任务4→6→8超期。不要从一个固定优先级政策失败推断任何调度都不可能。
边界回归取两任务都为(1,2,2)，固定第一任务更高。低优先级响应1→2→2，恰在2完成；时刻2新释放不算入[0,2)干扰。若把⌈2/2⌉错算成2，就会得到错误拒绝。
五、再交一份真正的不可行证书
两任务X、Y都为(2,2,10)，U=2/5。让它们在0同时释放并各需2服务；两个deadline均为2。窗口[0,2]的必做需求为4，容量为2，缺口为2。
这不是EDF失败、也不是破同值方式不好，而是任何单核单位速度调度都装不下。审核者只需读两份作业的释放/截止/需求，就能确认容量矛盾。把D都改成4后，第一次窗口可装下，须重新做完整判定；修改承诺不等于优化了原来的执行。
六、加入锁后重新建立假设
把线程基础优先级定为H=1、M=2、L=3。L在0持有m，需要4单位临界区CPU；H在1到达并请求m，获锁后要1单位；M在2到达，要5单位且不使用m。
- 无继承：L运行[0,2)，M运行[2,7)，L运行[7,9)，H运行[9,10)
- 有继承：L运行[0,4)，H运行[4,5)，M运行[5,10)
H的相对期限为4，绝对deadline为5。有继承时恰好按时；无继承时到10才完成。此处能证明H的低优先级阻塞服务最多3，因此R_H≤3+1=4。只有一把锁、H最高优先级、L无嵌套等待及自挂起等条件必须随结果一起交付。
接着提交四份管理器快照：
- H→M→L时，两级持锁者的有效优先级都变1；只提升M而不提升L的实现不通过
- L基础4持有a、b，H基础1等a、M基础2等b；释放a后a交给H，L必须留在2，不能直接降到4
- 取消H等待后，删除H的捐赠来源，但不能清空L的held或M的等待；全部来源消失才回基础值
- X持a等b、Y持b等a时，继承闭包即使稳定，两个线程仍都BLOCKED；不能把最高有效优先级当成死锁解除
还需检查移交：L释放a交给H后，仍等a的M现在等待H，不再等待L。下载器pending记录锁身份，等待图每次由最新owner重建。状态核验与真实调度执行是两个层面；随机管理器动作测试覆盖更多状态，不声称每段动作都来自某条最高优先级CPU运行表。
七、迁移与验收
把C的WCET从2改成3，或把某任务T缩短，重新求需求表与RTA；不能保留原“17/20”标签。改变相对deadline时，先检查D≤T是否仍成立；超出本模型应报告不支持，而非沿用有限判据。
提交最终JSON时，保留主输入、逐job元数据、服务段、完成/错过事件、需求判据、RTA迭代、锁图快照和失败反例。主脚本用独立时间槽可行性搜索核有限EDF任务，用逐job截止计数核dbf，用同步完整超周期核RTA，再用每个来源的可达路径集合核优先级闭包。各个穷举都只有所声明的有限范围，不能替代正文的一般证明。
成本报告要分开：事件堆调度、超周期候选点枚举、RTA数值迭代、继承图重算、完整日志和指数oracle。只写“EDF是O(log n)”遗漏了任务总数、时间窗口与证书的生成成本。