1.4 停机问题——工程师的四招降维打击
一道超纲的面试题
面试官递给你一支白板笔，问了一个问题：
“给你无限的时间和一台足够大的计算机，你能写一个程序，让它读完另一个程序的源代码，然后判断这个程序会不会跑飞吗？”
你可能会想：我在ECU上写过几百个task了，我知道什么代码会跑飞、什么不会。递归不设退出条件，跑飞。while(1)里面忘了清看门狗，跑飞。中断里做了浮点运算导致context save爆栈，跑飞。我能写十几种代码让程序跑飞。我都知道得这么清楚了，为什么不能写一个通用的检测器？
答案是：不能。1936年，一个23岁的剑桥研究生已经证明了：不存在一个通用算法，能判断任意程序在任意输入上是否最终停止。
这个研究生叫Alan Turing。那个证明叫停机问题（Halting Problem）。它不是“至今还没找到“，是“数学上不可能存在“。和你能不能写出更好的AI没关系，和计算机多快没关系。这个问题的答案本身就是“无解“，不是因为科技不够，而是因为逻辑自洽。
图灵的证明——自指的又一次凯旋
图灵用了一个和哥德尔如出一辙的手法：构造一个自指的悖论。证明的框架只有三步。
第一步：假设存在。假设世界上存在一台神奇的图灵机H，把它简称为“停机判定器“。你喂给它两个东西：程序P的源代码（编码成纸带上的符号），输入I（也编码成纸带上的符号）。H运行一段时间后，输出1，意思是“P在I上会停机“；或者输出0，意思是“P在I上永远不会停机（进入了死循环）“。
第二步：构造捣蛋鬼。 既然H这么厉害，我们造一个新程序D来捣蛋。D的行为简单到只有几行伪代码：
D 的行为（输入为程序 X 的编码）：
1. 调用 H(X, X) —— 问H："把X的编码作为输入喂给X自己，会停机吗？"
2. 如果 H 返回 1（会停机）：
进入死循环，永不停止
3. 如果 H 返回 0（不会停机）：
立即停止（HALT）
D就是那个捣蛋鬼：它做和H预测相反的事。H说你会停，我就偏不停。H说你不会停，我就马上停。
第三步：自指递进。 现在把D自己的源代码作为输入，喂给D自己。问一个致命的问题：D(D) 会停机吗？
如果D(D)会停机，说明H(D,D)返回了1（“会停机“的判断），但根据D的逻辑，此时D应该进入死循环。矛盾。如果D(D)不会停机，说明H(D,D)返回了0（“不会停机的判断”），但根据D的逻辑，此时D应该立即停止。矛盾。
两个方向都矛盾。矛盾的根源是H被假设存在，正因为假设了H存在，才会推出这个悖论。所以H不可能存在。图灵证明了，在“任意程序、任意输入“这个通用的定义下，停机判定是不可能的。
这个证明和哥德尔不完备定理共享同一个内核：自指导致悖论，悖论摧毁完备性。 哥德尔构造了一个“说’我不可证’的命题“。图灵构造了一个“做和H预测相反的事的程序“。两个系统都来自同一个几何点：系统试图审视自身的属性。
赖斯补刀——不只是停机
停机问题已经够致命了。但1953年，Gordon Rice又补了一刀。
Rice证明了一个比停机更广的定理：对于图灵机计算的任何非平凡语义属性，判定它是否成立是不可能的。 “非平凡“的意思是，不是所有程序都有这个属性，也不是所有程序都没有。“语义属性“是指关于程序做什么的属性（是否访问空指针、是否修改某个全局变量、是否产生死锁），而不是语法属性（是否有100行、是否包含某个变量名）。
换句话说：你永远无法写出一个通用工具，它能自动判定任意程序的“任意的你关心的行为属性“。 不是很难，是不可能。
这意味着什么？这意味着你永远无法有一个“一键OK“的按钮，按下之后自动扫描你的ECU代码，然后告诉你“没有runtime error“。自动代码分析在语义层面是无解的。所有能给出保证的静态分析工具，比如Astrée、PolySpace、BTC EmbeddedValidator，都不声称“通用“。它们声称的是“在这个特定的语言子集、这些特定的验证属性、这些特定的分析范围里，我可以给出确定答案。“
赖斯定理就是分析工具背后的幽灵：任何声称“通用“的分析，要么误报（把正确的报告为错误），要么漏报（把错误的报告为正确），不可能同时全部精准。
工程师的四招——从不可判定到可判定
停机问题和赖斯定理给出了判决：完美的程序分析不存在。但工程师不是数学家。工程师不寻求完美的通用解，他们寻求“给定约束下的具体解“。 这是四个已经被证明了行之有效的策略。
策略1：约束语言，把“所有可能的C程序“压成“一个可以被分析的子集“。
你在MISRA C规则里看到的每一条禁令，比如禁递归（规则17.2）、禁动态内存（规则21.3）、禁goto（规则15.1），不是技术审美的偏好，是约束空间的必须。一条动态内存分配把整个堆的状态拖进分析范围，在最坏情况下，分析工具必须考虑所有可能的malloc/free序列，复杂度立刻变成不可判定。禁掉了，分析工具只需要看栈和静态分配的BSS，这个子空间是可判定的。你付出的代价是编程自由度。你获得的收益是确定性。
策略2：约束硬件，把物理不确定性关在门外。
WCET（最坏执行时间）在现代CPU上做精确分析理论上也是不可判定的，因为缓存、分支预测、流水线、乱序执行共同作用。但ASIL D ECU上你可以锁死指令缓存和数据缓存（cache locking），把关键任务的优先级拉到最高并关闭抢占，关闭分支预测器。这样LDR指令的执行时间变成确定值，2个周期就是2个周期。STR也是2个周期。你把一个物理上不确定的执行环境压成了一个确定的时间通量。你付出的代价是性能。你获得的收益是WCET可预判。
策略3：用守卫代替证明，不需要证明不会跑飞，只需在跑飞时能恢复。
你不证明你的程序不会进入死循环。你在主循环的末尾写一行 watchdog_kick()。独立硬件看门狗定时器用独立时钟源倒计时：CPU没踢它，超时触发，硬件复位，进安全状态。你不证明“不会跑飞“，你只在“跑飞时能恢复“。这就是有界停机判定：不是判断“会不会停“，是判断“在限定的N毫秒内有没有踢我“。
def bounded_halt_check(prog, input_val, max_steps=1000000):
"""
在 max_steps 内，判断 prog(input_val) 是否停止。
如果超时仍未停，返回 False——不确定是否真的死循环。
对于 ECU 来说，这就是看门狗的超时阈值。
"""
steps = 0
# ... 执行 prog，每步计数 ...
if steps >= max_steps:
return False # 超时 → 视同"跑飞"
return True
策略4：用采样代替穷举，没必要测试所有输入组合。
测试100个参数的输入空间是无穷的，但等价类划分、边界值分析、最坏情况测试可以把它们缩小成有限数量的测试用例。ISO 26262 Part 6要求每个安全需求的测试覆盖率，不是要求“所有可能的输入“：是要求“等价类全部覆盖“。
停机问题不是告诉你“放弃“，是告诉你“改变问题的方式“。把“证明安全“改成“在约束下验证安全“。把“穷举“改成“在等价类上采样“。把“完美判定“改成“在安全一侧判定“。这四个策略共同构成了功能安全工程师面对计算边界时的完整反击体系。
赖斯定理——不只是停机
前面赖斯定理的结论你可能觉得太抽象了：“任何非平凡的语义属性都不可判定”。什么意思？你写三个问题去问一个“万能静态分析工具“就清楚了：
“这个程序会不会除以零？“这是语义属性。赖斯说：不可能通用判定。 “这个中断ISR会不会爆栈？“这也是语义属性。不可能。 “这段代码和那段代码在功能上是不是等价的？”：语义属性。还是不可能。
这三个问题都是非平凡的，有些程序会这样，有些不会。所以它们都落在赖斯定理的死亡射程内。
但这不意味着你桌子上的静态分析工具是废物。恰恰相反：Astrée、PolySpace、BTC EmbeddedValidator这些工具之所以能给出确定答案，是因为它们主动退出了“通用“的地盘。 Astrée只分析没有动态内存分配、没有递归、没有并发的同步C程序。它内部用的抽象解释（Abstract Interpretation）把程序的所有可能执行路径映射到一个有限格：浮点运算被过近似为区间算术，控制流被展开成一个有限的超图。它不声称“任意C程序“，它声称“在这个受限子集上的、这些特定run-time error类别，我可以给出确定答案。“
PolySpace走的是类似的路线，但在某些情况下它给出了另一种诚实的答案：灰色区域：“这一段的复杂度过高，我判断不了，请你人工review。” 这不是工具不完美，这是赖斯定理在借工具的嘴提醒你：灰色区域就是分析走到了可判定性边界的尽头。承认“不知道“比给出一个虚假的“通过“要诚实得多，虚假的通过会进入你的安全论证链条，给你的安全档案埋下一颗你永远不知道在哪里的炸弹。
BTC EmbeddedValidator更绝：它不分析C代码本身的行为，它分析的是“Simulink模型和生成的C代码之间是不是等价的“。它用的是形式化等价检查，把模型语义空间和代码语义空间桥接起来，逐条比对。这之所以可行，是因为模型和代码共享同一个功能规范，比对的对象是“同一件事的两种表达“，而不是“任意程序在任意输入上的任意行为“。它把“任意程序分析“的问题转化成了“两个已知规范的等价性判断“。
这些工具的共同秘诀是：它们不试图当“万能分析器“。它们在各自精心裁剪的边界内给出精确答案，边界之外的代码，你必须用其他手段论证。 赖斯定理的结论不是“所有分析都不可能“，是“通用分析不可能“。把“通用“两个字去掉，把问题切小：切到工具能一口吃下去的尺寸：答案就变得可能了。这就是策略1的数学依据：不是工具替你解决了赖斯定理：是你替工具把问题切小到了工具能解决的尺度。
用你的身体打一个比方：你的免疫系统里有T细胞和B细胞，但没有任何一种免疫细胞能识别“所有可能的病原体“。T细胞能识别的是“被MHC分子呈递的肽段“，它退出了“识别一切“的地盘，进入了“识别特定分子模式“的子空间。B细胞能产生抗体，但每一种B细胞只认一个特定抗原表位。它们都不“通用“，恰恰因为不通用，它们才“可用“。你的静态分析工具的逻辑完全一样：Astrée退出了“分析一切C程序“的地盘，进了“分析无动态内存、无递归、无并发的同步C“的子空间。在这个子空间里，它就像T细胞认肽段一样精确。
这反过来也解释了为什么功能安全工程师最怕的不是“工具报错“，是“工具不报错但漏了“。漏报在免疫学里等效于“病原体逃逸了免疫监视“：当分析工具走到了可判定性边界的尽头却没有告诉你“我判断不了“的时候，你在安全论证链条里埋下了一个隐形的漏洞。这就是为什么好的静态分析工具会明确告诉你它的“灰区“：“以下这些构造我的分析覆盖不了，需要人工review”：这不是工具的缺陷，这是工具对赖斯定理的诚实回应。
MISRA C的每一条禁令都是一次约束回归
现在我们把策略1拆开，看看你每天被迫遵守的MISRA C规则，是怎么一条一条地把代码从“不可分析“切到“可分析“的。每一条禁令，本质上都是一次“约束回归“，把可判定的边界往外推一步。
规则17.2（禁止递归）： 递归让函数调用栈的深度变成运行时变量。在最坏情况下，分析工具必须考虑所有可能的调用路径组合，每一个函数可能在自己身上绕多少次是不确定的。这个搜索空间是指数级的，不可判定。禁掉递归，调用栈的深度在编译时就能从调用图上静态算出，每一个函数的调用深度是有限的、可枚举的。这一步约束回归把“调用栈分析“从不可判定拉回了可判定。
规则21.3（禁止malloc/free和动态内存分配）： 动态内存让堆的状态空间变成运行时变量。一个malloc之后跟三个free，哪个free对应哪个malloc？在指针别名分析中，这个问题在最坏情况下需要分析指针的所有可能取值，不可判定。禁掉动态内存，所有内存在编译时就分配完毕，BSS段的大小是常量，栈的大小是编译时确定的常量。这一步约束回归把“内存使用量分析“从动态无限空间压成了静态常数。
规则15.1（禁止goto）： goto可以让控制流从任意位置跳到任意位置，控制流图变成了一张任意有向图。约束为标准的顺序、分支、循环结构，控制流图变成了一棵良构的树加有限回边。这一步约束回归把控制流分析的复杂度从“任意有向图“降到了“树状结构加受限回边“。
你可能会觉得这些规则让你束手束脚：“我用递归写个树的遍历都不行？”“我用malloc临时分个buffer都不行？“对，就是不行。不是因为递归和动态分配不好，是因为它们把你的代码推进了“分析工具无法给出确定结论“的灰区。你失去的是写炫技代码的自由，你获得的是安全论证的可操作性。 每一条MISRA禁令，从前一版标准到今天，都经过了“这条约束让什么变得可证明了“的工程推敲。它不是审美的偏好，它是计算的必然。
你今天写的每一个单元测试都是等价类采样
现在来看策略4，用采样代替穷举，在你日常工作中的落地形态。你今天早上打开IDE写单元测试的时候，可能没意识到：你正在执行策略4。
你有一个函数 int16_t computeTorque(uint16_t angle, uint16_t speed)，angle的范围是0-32767，speed的范围是0-65535。这两个参数的全组合：大约21.5亿种。用你们CI机房的服务器跑到SOP那天也跑不完。
但你没有慌乱。你做了三件事：
第一步，等价类划分。 你把angle分成四个等价类：最小值（0）、正常值（1~32766）、最大值（32767）、超出范围（>32767，触发函数输入守卫返回错误码）。每个等价类内部的值，在这个函数的语义下，行为应该是一致的，你从“正常值“里选了912和16384两个代表。21.5亿种组合被压缩成不到10个测试用例。
第二步，边界值分析。 你不仅要测angle=32767，还要测angle=32766（刚好在边界旁边）和angle=32768（刚好越界）。不是因为三个值的行为不一样（恰好在边界旁边的两个值时行为应该是一样的），但你的直觉和经验告诉你：大量的bug不在数值空间的正中央，就在两个等价类的边界线上。越界判断的if条件写成了>=还是>，只在边界值上能测出来。
第三步，最坏情况测试。 angle和speed都取最大值（32767 × 65535），乘出来的结果可能溢出 int32_t 的容纳范围。你在这个极端点上验证了一次，通过了。好，接下来你不需要再测angle=32766、speed=65535的组合，因为32767×65535比它更坏，最坏点过了，次坏点就不用测了。
现在你看测试覆盖率报告，它显示87%的行覆盖、73%的分支覆盖。给你看这个报告的工具不会告诉你的是：你在这里做的不是穷举验证，你是在用等价类对输入空间做有理论依据的采样。而ISO 26262 Part 6的测试覆盖要求，包括MC/DC、语句覆盖、分支覆盖，本质上就是在规范这个采样应该有多密。
MC/DC（Modified Condition/Decision Coverage）是采样密度标准中最精细的一个：对于每一个安全相关的布尔条件判断，每一个条件变量的每一个独立的真/假取值，在至少一个测试用例中被证实能“独立地决定判断的输出“。比如if (a && b)，你要测a=true/b=true（整体true）、a=true/b=false（整体false，由b决定）、a=false/b=true（整体false：由a决定）。不是“所有组合都要覆盖“：是“每一个变量独立影响输出的那条路径都要覆盖“。这是在布尔决策空间里的独立性采样。
这三个覆盖层级，包括语句覆盖、分支覆盖、MC/DC，形成了一套由粗到精的采样网格。语句覆盖是“每条代码行都被至少执行过一次“，这是最粗的筛子。分支覆盖是“每个if/else的两条分支都被走到一次“，这是中等的筛子。MC/DC是“每一个条件变量的独立影响力都被单独验证过“，这是最细的筛子。你不需要测所有的输入组合，因为一个函数里的某个条件判断的输出，不会因为你输入空间的另一个无关维度而发生意外翻转。一个if (angle > 1000)的结果，只和angle这个变量的取值有关，和speed的值无关。所以你在angle的等价类里采样几个代表，就足以覆盖这个条件的两条分支。这就是等价类采样的数学基础：输入空间的高维性在实际代码中被条件判断分解成了低维的独立子空间。
你回顾一下本章的四招，现在你应该看懂了它们之间的完整的逻辑关系。策略1（约束语言）让分析空间变得有限。策略2（约束硬件）让时间行为变得确定。策略3（守卫代替证明）把“会不会死循环“这个不可判定问题转化成“在N毫秒内有没有踢我“这个可判定问题。策略4（采样代替穷举）把指数级甚至无穷的输入空间压缩成有限测试网格。四招不是四个孤立的技巧，它们是同一个工程哲学在不同维度的展开：把不可判定问题切成可判定问题，把无限空间压成有限空间，把完美保证换成有界保证。 你的安全论证不是数学定理（数学定理要求无懈可击的逻辑推导），你的安全论证是一条工程推理链，它给出的是一个经过定量论证的置信度。
所以，停机问题不是告诉你“放弃“，是告诉你“改变问题的方式“。把“证明安全“改成“在约束下验证安全“。把“穷举“改成“在等价类上采样“。把“完美判定“改成“在安全一侧判定“。 这四个策略共同构成了功能安全工程师面对计算边界时的完整反击体系。
本篇小结
- 图灵停机问题证明：不存在通用算法判断任意程序是否停止。这是数学的不可能性，与硬件速度无关。
- 赖斯定理推广：任何非平凡的语义属性（如“这个程序会不会访问空指针“）都是不可判定的。
- 工程师用四招绕过计算边界：约束语言（MISRA C）、约束硬件（cache locking）、守卫代替证明（watchdog）、采样代替穷举（等价类测试）。
- 看门狗的本质是有界停机判定：不判断“会不会停“，只判断“在限定时间内有没有踢我“。
【下集预告】： 数学告诉我们完美分析不可能。但物理世界还给工程师留了另一个难题：硬件会随机翻转。一个alpha粒子从封装树脂中飞出，穿过SRAM的一个6T单元，一个bit从1翻成了0。不是软件bug，没有逻辑路径。纯粹物理骰子。下节看ECC、lockstep、冗余如何应对。