在1988年11月15日,苏联的暴风雪号航天飞机完成了它的首次也是唯一一次无人自动飞行,这次任务的成功背后,有一套复杂的计算机系统在默默支撑,而其中最引人注目的设计之一,就是它采用了四台完全相同的Biser-4计算机,而不是当时常见的三台,这个选择并非偶然,而是基于对故障模式、同步机制以及任务需求的深入考量,本文将从历史资料出发,探讨为何四台计算机成为必要,分析其背后的技术逻辑,并与同时期的航天器进行对比,揭示冗余设计中的关键取舍 暴风雪号的计算机系统由NIIAP研究所负责开发,该研究所后来成为NPCAP,其核心部件Biser-4是一款高性能的机载计算机,专门为航天任务定制,根据公开资料,整个系统由两套完全相同的计算机集群组成,一套用于中央控制,另一套用于外设控制,但在实际飞行中,只有中央集群投入了使用,外设集群的插槽被空白面板封闭,中央集群内部包含四台完全相同的Biser-4计算机,它们被称作通道,每一台都运行相同的程序,并且通过硬件同步机制保持严格的时钟同步,这种同步不是依靠复杂的软件协调,而是通过一个统一的时钟源实现的,该时钟源本身也采用了五通道冗余设计,每三个输出进行投票,以确保时钟信号的可靠性,同步的重要性在于,只有当所有通道在同一时刻处理相同的输入帧时,输出比较才有意义,否则一个通道稍有延迟就会被误判为故障 那么为什么选择四台而不是三台呢?这是本文的核心问题,在容错计算领域,三模冗余是一种经典方案,它通过三台计算机同时运行相同的任务,然后对输出进行多数表决,从而屏蔽掉任意一台的故障,这种设计的数学基础是2f+1,即要容忍f个故障,需要至少2f+1个通道,因为只有多数正确的输出才能压倒错误的输出,暴风雪号的时钟系统正是采用了这种思想,五通道中每三个输出进行表决,可以容忍两个同时发生的故障,然而,暴风雪号的计算机系统并没有采用这种屏蔽式容错,而是采用了比较与隔离的策略,也就是说,系统并不在输出端进行实时表决,而是在每个通道的输出端设置比较电路,一旦发现某个通道的输出与其他通道不一致,就将其封锁,从而将其从系统中移除,这种策略要求系统能够承受连续的故障,每发生一次故障,就损失一个通道,直到剩余通道仍能维持运行 如果仅依靠输出比较来识别故障,那么三台计算机在第一次故障后会出现2比1的分裂,此时可以判定少数派为故障并将其隔离,剩下两台计算机继续运行,但当第二台计算机发生故障时,剩下的两台计算机会彼此 disagree,比较电路无法判断哪一台是正确的,从而导致系统失效,因此,三台计算机只能容忍一次故障,而四台计算机在第一次故障后剩下三台,仍可进行多数判断,第二次故障后剩下两台,这两台在正常情况下应该仍然一致,从而可以继续提供服务,因此,四台计算机的配置可以容忍两次连续的故障,这正是暴风雪号的设计要求,即在任意两个通道发生故障的情况下,系统仍能保持运行,这一要求来源于任务安全性的考量,根据设计文档,系统必须在任意两个通道故障时,仍能保证机组人员的安全并返回地球,因此,四台计算机的配置是满足这一要求的最小数量 然而,上述分析基于一个关键假设,即故障的识别完全依赖于输出比较,如果通道具备自我检测能力,例如通过内部看门狗或状态信号来判断自身是否失效,那么情况就会有所不同,在这种情况下,一个通道可以在不依赖比较的情况下主动报告故障,从而减少对通道数量的需求,遗憾的是,现有的公开资料并未明确说明Biser-4是否具备这种自我检测机制,其前身Biser-2确实有一个多数表决元件,但那是用于输入输出通道的内部数据路径,而不是用于冗余通道的故障识别,因此,对于Biser-4而言,最保守的估计是它仅依赖输出比较来识别故障,从而必须采用四台计算机来满足两故障容错的要求 与暴风雪号形成鲜明对比的是美国的航天飞机,航天飞机最初的设计要求是fail operational/fail operational/fail safe,即系统在第一次故障后仍能继续运行,在第二次故障后仍能安全返回,但不要求第三次故障后的运行,为了满足这一要求,航天飞机最初计划使用五台计算机,因为五台计算机可以在两台故障后仍保持三台正常运行,从而进行多数表决,后来,NASA放宽了要求,改为fail operational/fail safe,即第一次故障后继续运行,第二次故障后安全返回,从而将计算机数量减少到四台,但在航天飞机的设计中,这四台计算机的容错机制与暴风雪号有所不同,航天飞机的计算机并不自动关闭故障通道,而是由机组人员手动切断其电源,这样做的目的是防止通用软件故障导致所有计算机同时被关闭,换句话说,航天飞机的设计者已经意识到,如果所有计算机运行相同的软件,那么一个软件错误可能导致所有计算机同时失效,因此他们选择了人工干预的方式,而暴风雪号的设计则更为自动化,其比较电路会自动封锁故障通道 从更抽象的层面来看,输出比较与拜占庭将军问题是两种不同的容错模型,拜占庭将军问题研究的是在存在任意故障(包括恶意故障)的情况下,如何使所有正确节点达成一致,其经典结论是,要容忍f个任意故障,需要至少3f+1个节点,这个结论与输出比较的2f+1不同,拜占庭将军问题的边界更严格,因为它考虑了故障节点可能发送矛盾信息的情况,而输出比较假设故障节点仅产生错误输出,但不会主动欺骗,因此,暴风雪号的四台计算机配置并不能直接套用拜占庭将军问题的结论,事实上,在四台计算机的场景下,如果出现一个拜占庭故障,即某个通道向不同的接收者发送不同的值,那么系统将无法达成一致,然而,现有的资料并未提及Biser-4的通道之间是否存在这种任意故障的可能性,因此,将四台计算机解释为满足3f+1的结论是不恰当的,更合理的解释是,它满足的是基于输出比较的2f+1要求,即容忍两个故障 在实际工程中,拜占庭故障并非理论虚构,而是真实存在的,例如,一个 stuck-at-½信号可能被不同接收者解释为0或1,或者一个损坏的CRC可能被不同节点解读为有效或无效,这些现象在辐射环境或电子干扰下尤为常见,有研究指出,在强辐射条件下,基于TTP/C协议的集群可能分裂成多个独立的小群体,每个群体内部一致但彼此不同,这种现象被称为拜占庭故障,然而,对于暴风雪号而言,其设计并未明确考虑这种故障模式,其比较电路仅针对输出不一致的情况进行处理,而未涉及消息层面的任意故障,因此,将拜占庭将军问题的结论直接应用于暴风雪号是不准确的,更准确的说法是,四台计算机的配置是为了在输出比较的框架下容忍两个故障 软件层面的共因故障是另一个不可忽视的问题,当所有通道运行相同的程序时,一个程序错误可能同时影响所有通道,从而导致系统性失效,这种风险在航天史上并非没有先例,例如,1981年航天飞机的首次发射尝试中,备份飞行系统无法与主计算机同步,原因是一个微小的编程错误,该错误在数千小时的测试中未被发现,导致主计算机提前40毫秒开始处理,虽然这个错误只会在每67次发射中出现一次,但它表明,即使硬件冗余足够,软件共因故障仍可能导致系统失效,另一个例子是波音787的发电机控制单元,2015年发现的一个软件计数器溢出问题,会在248天后同时使所有四个控制单元进入安全模式,导致飞机失去全部交流电,这些案例表明,仅靠硬件冗余无法防范软件层面的共因故障,必须通过多样性设计和严格的验证来补充 为了应对软件共因故障,业界通常采用两种策略,一是多样性设计,即使用不同的硬件、不同的编译器或不同的算法来实现相同的功能,从而降低共因故障的概率,例如,空客A320系列飞机的飞行控制计算机使用两种不同类型的处理器,由不同的团队开发,以减少共因故障的风险,波音777的主飞行计算机则使用三种不同的Ada编译器和三种不同的处理器,尽管它们源自同一份源代码,二是形式化验证,即使用数学方法证明程序满足其规约,从而发现潜在的错误,例如,NASA在猎户座飞船的备份软件中采用了形式化方法,以确保在主计算机因软件错误同时失效时,备份系统能够接管,在暴风雪号的设计中,虽然有资料提到所有通道运行相同的程序,但并未提及是否存在多样性备份,因此,软件共因故障的风险依然存在 从工程实现的角度来看,暴风雪号的四通道比较系统可以抽象为一个决策函数,该函数接收四个通道的输出字,并根据预设的规则决定输出命令或隔离故障通道,这个函数的逻辑相对简单,但其正确性却至关重要,为了确保其可靠性,可以采用形式化方法对其进行验证,例如,使用Lean 4证明助手对决策函数进行机器检查,证明其在所有可能的情况下都不会出现误判,这种验证可以覆盖手工测试难以穷举的边界情况,从而提高系统的可信度,然而,形式化验证也有其局限性,它只能证明代码满足其规约,而不能保证规约本身是正确的,如果规约中遗漏了某些故障模式,或者对故障的假设不准确,那么验证的结果仍然不可靠,因此,形式化验证通常与多样性设计结合使用,以提供多层次的保障 在暴风雪号的案例中,四台计算机的配置是一个经过深思熟虑的选择,它基于输出比较的容错模型,满足了两故障容错的要求,同时考虑了同步机制和软件共因故障的风险,虽然它并非完美无缺,但在当时的技术条件下,是一个合理且可靠的设计方案,通过与航天飞机等其他航天器的对比,我们可以更清晰地看到不同设计理念的优劣,从而为未来的航天任务提供借鉴,在追求更高可靠性的过程中,硬件冗余、软件多样性、形式化验证以及严格的质量管理都是不可或缺的要素,只有将这些要素有机结合起来,才能构建出真正安全可靠的航天计算系统 。
