1.4 计算的边界一个不可能完成的 KPI你是一家汽车零部件厂的工程师。老板给你提了一个需求“写一个程序它会读入另一个程序的源代码然后自动判断这个程序会不会跑飞。”跑飞的意思是程序会不会进入死循环会不会访问空指针会不会在某种输入下爆栈会不会在中断嵌套中发生优先级反转导致死锁你接到这个任务之后想了三天三夜然后找到老板“这个程序——我写不出来。”老板愣了“为什么”“不是因为我能力不够——而是因为数学上就不可能。”停机问题图灵的第二个震撼图灵在 1936 年的论文中除了发明图灵机还证明了一个震撼世界的结论不存在一个通用算法能够判断任意程序在任意输入上是否最终会停止。这就是停机问题Halting Problem。证明的核心思路极其优雅而且和哥德尔如出一辙——构造一个自指的悖论。假设存在一台图灵机 H它能读入程序 P的编码和输入 I的编码然后输出 1P 在 I 上会停机或 0永远不会停机。现在我们构造一台捣蛋的图灵机 D。D 的行为很简单——它接收一个程序 P的编码然后D 的内部逻辑 1. 调用 H(P, P) → 问 H以 P 为输入的程序 P会停机吗 2. 如果 H 返回 1会停机 → D 进入死循环永不停机 3. 如果 H 返回 0不会停机 → D 立即停机现在问一个致命的问题D(D) 会停机吗——也就是把 D 自身的编码作为输入喂给 D问它会怎样。假设推理结论D(D) 会停机则 H(D,D) 返回 1D 进入死循环 →矛盾D(D) 不会停机则 H(D,D) 返回 0D 立即停机 →矛盾无论哪种情况都矛盾。所以H 不可能存在。这个证明的妙处在于——D 不需要对 H 做任何复杂的攻击。它只是诚实地调用 H然后诚实地做出与 H 预判相反的行为。矛盾不是来自恶意——而是来自自指。哥德尔构造了说’我不可证’的命题图灵构造了问’我会不会停’的程序——结构完全相同。这两篇论文的发表时间只隔了 5 年但它们共同定义了一个事实任何足够强大的形式系统或计算模型都无法逃脱自指悖论的阴影。赖斯定理不只是停机——所有非平凡属性停机问题只是冰山一角。1953 年亨利·赖斯Henry Gordon Rice——当时还是雪城大学的博士生——在他的博士论文中证明了一个让所有程序员绝望的定理。赖斯定理说对于程序的任意非平凡语义属性都不存在一个通用算法能判断程序是否具有该属性。什么是非平凡就是不是所有程序都有、也不是所有程序都没有的属性。比如“这个程序是否会访问空指针”——有的程序会有的不会 → 非平凡 → 不可判定。“这个程序是否会在第 42 行打印 ‘hello’”——非平凡 → 不可判定。“这个程序在运行时变量 x 的值是否会出现大于 1000”——非平凡 → 不可判定。“这个程序在运行到函数 foo() 时栈指针是否超出栈空间”——非平凡 → 不可判定。注意这些属性都是你在日常开发中非常想知道的。但赖斯定理说不存在一个程序能自动、正确、无遗漏地帮你判断这些属性。赖斯定理是停机问题的惊人推广。停机问题说你不能自动判断程序会不会停赖斯说你不能自动判断程序的任何非平凡语义属性。这解释了为什么 MISRA C、CERT C、AUTOSAR C14 这些编码规范禁止那么多东西——递归、goto、动态内存分配、函数指针、变长数组、union 的类型双关。这些约束不是在限制你的编程自由——它们是在删掉那些让程序属性不可判定的语言特性。你删掉了递归栈深度变成静态可分析的。你删掉了动态内存分配内存泄漏变成不可能出现的。你删掉了函数指针控制流图变成完全静态的。每一次你不许的背后都是一个赖斯定理的判决。忙海狸狂欢明知存在却永远算不出停机问题不是唯一一个揭示计算边界的例子。还有一个更直观的——忙海狸函数Busy Beaver。1962 年匈牙利数学家蒂博尔·拉多Tibor Radó提出了一个绝妙的思想实验。考虑所有具有 n 个状态不算停机状态的、能最终停机的图灵机。在这些图灵机中有一个“最勤奋的”——它在停机之前在纸带上写了最多的 1。这个“最多 1 的数量”就是 BB(n)。BB 函数是多快就变大了BB(1) 1 1 个状态的图灵机最多只能写 1 个 1 然后停机 BB(2) 4 4 个 1 BB(3) 6 6 个 1 BB(4) 13 13 个 1 BB(5) 47,176,870 2024 年才确定 BB(6) ≥ 10↑↑15确切值未知但至少这么大。这个数字大到无法用常规符号写下——远超宇宙中的原子总数注意BB 是一个良定义的函数——对于每一个 nBB(n) 是确定的数值。因为候选的图灵机总数是有限的虽然非常多你可以枚举所有 n 状态图灵机检查哪些会停机统计它们的输出取最大值。BB(n) 确定地存在确定地唯一。但你能计算它吗不能。拉多证明BB 函数是不可计算的。不存在一个通用算法输入 n输出 BB(n)。理由很简短如果存在就能用 BB 函数的值来判定停机——而停机问题已经证明了这不可能。BB 函数是人类已知的最简单的定义明确但算不出来的函数。它界定了可计算性的边界不是所有良定义的数学对象都可以用算法求值。有些问题——即使是像用 n 个状态的图灵机最多能写几个 1这么简单的问题——答案虽然存在但通向答案的道路被哥德尔和图灵联手的自指悖论封死了。P 与 NP不动刀子的陷阱停机问题和忙海狸是不可判定的——数学上不可能。但还有另一类问题理论上可解实践中算不动。这就是 P 与 NP 问题。PPolynomial time是可以被算法在多项式时间内解决的问题。“多项式时间”——O(n)、O(n²)、O(n³)、O(n log n)——都 OK。随着问题规模的增大计算量的增长是可控的相对而言。NPNondeterministic Polynomial time是那些如果你猜对了答案能用多项式时间验证它是否正确的问题。P 是能找到答案NP 是能验证答案。P NP 吗——这是千禧年七大数学难题之一悬赏一百万美元至今未解。但工程师的直觉告诉我们P ≠ NP。不然银行加密、HTTPS 证书、数字签名——所有这些依赖某些问题很难解的技术——都会在一夜之间崩塌。如果 P NP破解 RSA 加密和解一个字谜的难度就等价了。对汽车工程师来说NP-hard 问题的典型代表是什么最优线束布局。你要在整车车身上布线——电源线、CAN 总线、传感器信号线——总长度最短、重量最轻、不允许交叉走线、避开高温区排气管附近、避开电磁干扰源。这是一个旅行销售员问题TSP的变体。TSP 的搜索空间是 n! 级别的。按照 30 个连接点计算可能的路径组合数约为 10³²——比宇宙中的星星还多。优化它需要启发式算法、遗传算法、模拟退火——不是完美解而是足够好。ECU 的网络拓扑设计。车载网络里哪些 ECU 挂在 CAN A 上、哪些挂在 CAN B 上、哪些挂在 FlexRay 上、哪些挂在 LIN 上——这个问题最小化网关转发延迟 最小化总线负载的区块分割问题是 NP 难的。汽车网络架构师花了几个月设计一个拓扑本质上是在一个无法暴力搜索的空间里做工程折中。NP 困难问题是不动刀子的陷阱。停机问题是不可判定——根本不存在算法。NP 问题是可判定——但存在的算法在你死之前算不完。两者的工程后果一样你永远没法得到完美的解。你必须妥协。从不可判定到可判定工程师的降维打击既然停机问题和赖斯定理宣告了完美的自动化分析不可能那我们是怎么保证汽车软件安全的答案是改变问题。我们不是去证明任意程序的任意性质——那是赖斯禁区。我们的策略是策略一约束语言——把问题空间缩小。你用的不是 C23 全特性集。你用 MISRA C——禁止递归、禁止动态内存分配、禁止 goto 乱跳。这相当于在所有可能的 C 程序的宇宙里划了一个矩形——矩形以内的程序属性是可判定的。你付出的是编程的自由度换来的是分析的确定性。策略二约束硬件——把物理不确定性关在门外。WCET最坏执行时间在现代 CPU 上做精确分析理论上是不可判定的——因为有缓存、分支预测、流水线、乱序执行。但汽车 ASIL D 级别的 ECU 上你可以把指令缓存和数据缓存锁死cache locking把关键任务的中断优先级拉到最高并关闭抢占让分支预测器关闭。这样一来指令的执行时间变成确定的值——LDR 就是 2 个周期STR 就是 2 个周期。你重新把物理世界压成了一个充分确定的子集。策略三用守卫而不是用证明。你不证明这个程序不会跑飞——你写一个独立看门狗independent watchdog定时器。程序每个周期在 main loop 里踢它一脚。如果程序跑飞了、进入了死循环、爆了栈——看门狗超时硬件复位进入 safe state。你不需要证明不跑飞——你只需要在跑飞时能恢复。策略四用采样代替穷举。你不测试所有可能的输入组合——输入空间太大了。你设计等价类、边界值、最坏情况——ISO 26262 的测试方法论从 Part 6 到 Part 11 全在干这一件事。你不在无穷的输入海洋里游泳——你把海洋缩小到一个可游的游泳池然后保证在这个池子里你的程序的每一个分支都被覆盖了。有界环境下的停机判定——代码演示为了帮你建立直觉这里给出一段 Python 程序。它在有限步骤内100 万步判定一个特定的、极其简化的程序是否会停机。注意——这不是解决了停机问题这是在明确画好的圈子里停机问题是可判定的defbounded_halt_check(prog,input_val,max_steps1000000): 在 max_steps 步之内判断 prog(input_val) 是否停机。 如果 max_steps 之前停机了返回 (True, 步数)。 如果超过 max_steps 步还没停返回 (False, max_steps)。 这不是通用停机判定器——它有 max_steps 上限。 但对于 ECU 来说这就是我们需要的在 10ms deadline 之前 这个 task 能不能跑完 ip0# 指令指针accinput_val# 累加器steps0whileiplen(prog)andstepsmax_steps:opprog[ip]ifopINC:acc1ip1elifopDEC_JZ:ifacc0:ip2else:acc-1ip1elifopHALT:return(True,steps)else:ip1steps1ifstepsmax_steps:return(False,max_steps)# 超时——不确定是否真的死循环return(True,steps)# 测试一个计数到 10 然后停机的程序prog[INC]*10[HALT]print(bounded_halt_check(prog,0,100))# (True, 10)这段代码做了什么呢它把原始的停机问题“在无限步内判断”改写成了有界停机问题“在 N 步内判断”。有界版本是可判定的——因为你只需要执行最多 N 步。这就是 ECU 上的 watchdog 原理。Watchdog 不证明程序不会死循环——它只限定时限给你 10ms你踢我一次。“你不踢 你死了 我复位你”。时间约束本身就是让不可判定问题变成可判定问题的武器。行业实践在计算边界的悬崖上走钢丝理解了上面这些理论你就能看懂行业里那些看似过度约束的规定了。AUTOSAR 的 OS 模块规定Task 不能有无限循环每个 task 必须在有限时间内完成并让出 CPU。这是一种有界停机要求。ASIL D 系统里的 Freedom From InterferenceFFI要求内存分区Memory Partitioning——不允许一个 QM 级别的任务访问 ASIL D 任务的内存。这是一堵物理墙防止低安全等级的程序污染高安全等级程序的数据。注意——如果用软件做检查“if (address boundary) …”这个检查本身可能出错。用 MPUMemory Protection Unit硬件做CPU 在总线层面拦截非法访问——这是一层物理保证。物理比逻辑可靠是因为物理没有自指悖论。Astrée 静态分析器在空客 A380 和某些 ASIL D 项目中使用的技术称为抽象解释Abstract Interpretation——它不跟踪程序的每一个具体状态而是跟踪状态的抽象域。比如变量 x 在 0 到 100 之间这个抽象状态。如果 x 的抽象域和某个数组边界不冲突则证明没有越界访问。这是用保守近似换取保证如果 Astrée 说没有运行时错误则确实没有。如果它不能断定它会报可能错误让你手动检查。误报可以存在漏报不能——因为漏报 安全声明是假的。这个 tradeoff——允许误报、杜绝漏报——是静态分析在计算边界面前的基本策略。我们不追求完美判定。我们追求安全的一侧。芯片良率和计算边界——同一个故事在面板厂里我的工作之一是在线缺陷检测Inspection。你不能检查每一个面板单元的每一个 TFT。你把基板放进扫描电子显微镜用 10nm 分辨率的电子束扫过几个区域统计缺陷密度defect density用来推算整片基板的良率。这是不是完美良率判定不是——它是有界的、基于采样和统计推理的近似。但它足够好了。足够让你的车规 MCU 在 -40°C 到 125°C 的环境下跑 15 年不坏。这和停机问题告诉我们的道理一样完美不可得足够好可得。而足够好的定义是工程的需求驱动的——不是数学的定义。在 ISO 26262 的语言里足够好叫 ASIL 对随机硬件故障的概率性度量目标PMHFProbabilistic Metric for random Hardware Failures小于 10 FIT。10 FIT 意味着 10 亿小时的运行中出现少于 10 次故障——大约相当于 11415 年出现一次。这个数字不是数学保证的——它是统计推断给出的信心区间。知道边界才知道怎么走路停机问题的哲学启示是有些问题答案不存在。——不是还没找到是永远找不到。这很残酷。但它也解放了我们。你不会因为修不了所有 bug 而自责——因为数学说不可能。你不会因为测试不能覆盖所有边界而焦虑——因为数学说不可能。你手里的 ISO 26262 安全案例、你写的单元测试、你设置的每一个 MPU 区域的权限——都不是在证明完美——它们是在证明在给定约束下安全性不低于某个阈值。理解了边界你才真正自由了。但这不意味着放弃。恰恰相反。我们知道通用 bug 检测不可判定所以我们发明了形式化方法、模型检查、符号执行——它们不能解决一切但能在特定的、可判定的子集里做到完美。我们知道停机不可判定所以我们发明了 watchdog 定时器——程序跑飞了硬件替你复位。不需要证明它不会跑飞只需要在它跑飞时能恢复。我们知道 WCET 的精确定界在复杂硬件上是不可判定的所以我们在安全关键任务中关掉缓存、关掉分支预测、禁止使用共享资源——把不确定性关在门外。我们面对不可解的问题不投降——我们走侧面。走侧面是工程师最重要的战术素养。编程语言的设计者在图灵完备的雷区里划出了安全子集——MISRA C。硬件架构师在不可预测的缓存迷雾里插入了确定性锚点——锁定缓存。编译器作者在指令重排的乱序世界里保证了高阻隔离——内存屏障。每一次走侧面都是在不可判定的阴影下找到一小片有光的角落。这正是你在汽车电子领域每天做的事面对物理极限——EMC 干扰、芯片良率、温度漂移——你不是打败物理定律而是绕过去。加屏蔽罩、选宽温芯片、做冗余设计。知道边界在哪里是跨越边界的第一步。你的大脑也是一台计算机——只是在用不同的约束在讨论计算的边界时一个自然的问题是人类的大脑呢你的大脑有大约860亿个神经元每个神经元平均有7000个突触连接。它做图像识别、语言理解、运动控制——所有这些功耗只有大约20W。而一台训练GPT-4的GPU集群可能消耗几兆瓦。你的大脑不仅在“低功耗”上碾压芯片——它在“容错”上也碾压每天有成千上万个神经元自然死亡但你的意识不受影响。而一颗芯片上一个关键晶体管失效整个die可能报废。但你的大脑也有自己的“有限资源”——而且它的限制比芯片更深刻。你的工作记忆working memory只能同时维持大约4-7个信息块。你无法像计算机一样“记住一百万个数”——你只能“记住规律”。你的计算速度大约相当于每秒几十次“意识层操作”——而一颗112MHz的Cortex-M4每秒可以做1.12亿次指令。你不是比芯片“慢”——你是在用完全不同的策略“计算”。你用模式识别替代穷举搜索。你用经验替换算法。你用“直觉”跳过中间推理步骤。理解你的大脑这台“计算机”的局限性——会让你对自己写代码这件事产生一种有趣的敬意你正在用一台功耗20W、容错率极高但精确度极低的“人脑”去指挥一台功耗100mW、容错率为零但精确度极高的“芯片”。这是两种完全不同的“计算哲学”的对话。本篇小结今天我们做了一件事走进计算的边界看清楚了哪些问题数学上永远无法解决。关键结论停机问题和赖斯定理宣告了完美自动化分析的不可能通用bug检测、任意属性的自动判定——数学上做不到。工程师的回应不是投降是走侧面约束语言MISRA C、有界化watchdog、采样替代穷举、用安全的一侧替代完美判定。知道了边界才真正自由了你不会因为修不了所有bug而自责——把不可判定问题变成可判定问题是工程师的核心战术素养。下一节我们看冯·诺依曼如何把图灵的纸带变成真实的电路图——ENIAC的机房已经等在那里了。【下集预告】图灵机是抽象模型但你的 ECU 是真家伙。从图纸到硅片中间经历了什么1945 年一份 101 页的报告被分发给了 ENIAC 项目的核心人员。作者署名是约翰·冯·诺依曼。他把图灵的纸带变成了真实的电路图——而且做了一个天才的决定把程序也存进内存里。从此软件诞生。不——等一下。在冯·诺依曼之前还有一台机器叫 ENIAC。它重 30 吨用 18000 根真空管。每次换程序需要几十个女工程师在机器内部爬上爬下手动插拔电缆耗时数天。冯·诺依曼看着她们说“这不合理。”下一章我们走进 ENIAC 的机房闻一闻 1945 年的焊锡和真空管烧焦的味道——然后看冯·诺依曼如何用一个想法把这些电缆和真空管全部虚拟化成了软件。本文内容摘自本人的开源书《从沙子到车辙 - 一个工程师的理解》 在线阅读/下载from-sand-to-rutsgitclone https://github.com/Lularible/from-sand-to-ruts⭐ 如果对您有帮助欢迎 Star 支持也欢迎通过 GitHub Issues 交流讨论。