OceanGate深海潜艇事故的调查报告多次提及“责任制”，但这篇文章认为，责任制并非万能药。文章将问题分为两类：协调性挑战和风险评估失准。在协调性挑战中，责任制可能导致将责任推卸给某个个人，而忽视了系统性问题。在风险评估失准中，即使CEO身兼潜艇驾驶员，承担了最大风险（“把命押上”），但其错误的风险评估依然导致了灾难。文章认为，解决这类问题需要跨团队协作和独立的安全审查机制，而非仅仅依赖于责任制，因为责任制可能加剧“双重束缚”问题，使个人面临互相冲突的压力，从而导致安全隐患被忽视。
阅读更多
本文探讨了形式化规范与传统程序的区别。传统程序是指令列表，而形式化规范是行为集合。作者以计数器为例，说明规范如何定义所有正确行为，并利用集合论的思想，通过生成器（Init和Next）描述无限行为集。这与程序中非确定性的概念有所不同，形式化规范中的非确定性指行为的多种扩展方式，而程序中的非确定性则指代码路径的不确定性。文章强调了理解形式化规范作为行为集合的重要性，这有助于调试和理解模型检查器的错误。
阅读更多
本文分析了亚马逊Alexa在大型语言模型领域落后于竞争对手的原因，并将其解读为韧性工程中的“脆性”系统失败。文章指出，亚马逊Alexa的失败体现在三个方面：一是资源分配效率低下，导致团队无法及时获取必要的计算资源；二是组织结构过于分散，导致团队目标不一致，内耗严重；三是坚持过时的客户至上策略，未能适应AI研发所需的实验性和长期性。这三个因素共同导致了亚马逊在AI竞争中的失利，为企业组织结构和资源管理提供了深刻的教训。
阅读更多
本文批判了根因分析（RCA）在复杂系统故障分析中的局限性，认为其基于错误的因果链模型，无法有效应对复杂系统中多因素交互导致的故障。作者提出了韧性工程（RE）模型作为替代方案，该模型关注系统各组件间的交互作用，而非单一原因。RE模型认为系统总是存在大量潜在故障，成功在于系统的适应能力和容错性，通过理解系统如何适应和应对故障，而非简单地消除故障根源，才能持续改进，提升系统韧性。
阅读更多
作者使用FizzBee，一种新颖的基于Starlark的正式规范语言，对互斥锁算法进行了建模，探索了Redlock算法中存在的问题。文章通过对关键代码段、锁机制、租赁机制和栅栏令牌的建模，逐步揭示了Redlock算法的局限性，并最终发现栅栏令牌并不能完全解决互斥问题。作者总结了FizzBee的易用性和一些不足，并强调了形式化规范在算法设计中的重要性。
阅读更多
FAA数据显示，里根机场发生30起险些事故。文章指出，科技公司往往更关注严重事故的预防，而忽视了大量“险些事故”的潜在风险。“险些事故”是未来严重事故的前兆，但由于其零影响性，常常被忽略。作者认为，应将“险些事故”视为与严重事故同等重要的问题，并建立机制积极发现和分析它们，这需要组织文化上的转变，鼓励员工积极报告并分析“险些事故”，从而提升可靠性。
阅读更多
Canva最近遭遇了一次大规模宕机事件，其根本原因在于系统饱和。Canva部署了一个新的编辑器页面版本，但并非代码错误导致宕机，而是由于Cloudflare CDN的一个过时规则导致亚洲用户加载Javascript文件时延迟剧增。这引发了27万个并发请求，随后对API网关造成了每秒150万次请求的巨大压力，远超其处理能力。同时，API网关中一个已知但未修复的性能问题进一步加剧了情况。最终，Linux OOM killer杀死了所有API网关任务，导致Canva网站完全瘫痪。Canva工程师通过手动增加任务数量、使用Cloudflare防火墙规则临时阻断流量以及逐步恢复流量等措施解决了问题。这次事件凸显了系统韧性的重要性，以及在高负载情况下自动化系统可能带来的负面影响。
阅读更多
本文探讨了当前仪表盘设计的不足之处。作者指出，现有的仪表盘往往设计拙劣，无法有效利用人类视觉系统处理大量信息。文章回顾了80年代和90年代一些关于仪表盘设计的认知系统工程研究，例如生态界面设计和视觉动量，并指出当前行业缺乏对改进仪表盘设计的关注。作者呼吁重视仪表盘设计，使其更好地结合查询功能，提升信息处理效率。
阅读更多
OpenAI于12月11日遭遇重大服务中断，根源在于新部署的遥测服务。该服务意图提升可靠性，却意外地向Kubernetes API服务器施加了巨大负载，导致API服务器饱和，进而使大多数大型集群的Kubernetes控制平面瘫痪，最终破坏了基于DNS的服务发现机制。这次事故凸显了复杂系统中意想不到的交互作用以及全负载条件下才能暴露的问题。OpenAI通过缩减集群规模、阻止对Kubernetes管理API的网络访问以及扩展Kubernetes API服务器等手段恢复了服务。
阅读更多
本文通过一个戏剧化的场景，探讨了软件开发中效率和彻底性之间的权衡。工程经理和技术主管讨论了“谨慎性旋钮”的概念，即在测试、流程 adherence 等方面投入的精力。提高谨慎性可以减少事故，但会延长开发时间，反之亦然。文章指出，在实际工作中，团队会根据风险评估调整谨慎程度，但这种评估并不总是准确，导致事故发生。最终，文章强调了明确权衡谨慎性和时间成本的重要性，而不是隐含地进行这种权衡。
阅读更多
本文以电梯系统为例，详细介绍了如何在TLA+中指定活性属性。文章首先解释了活性属性和安全属性的区别，然后逐步构建了一个简单的电梯模型，并通过模型检查器TLC发现了模型中可能出现的电梯卡住的问题。之后，文章详细介绍了如何使用弱公平性和强公平性来指定活性属性，以确保电梯不会卡住并最终访问每一层。
阅读更多
这篇文章探讨了分布式系统中程序正确性的概念，特别关注线性一致性。文章首先介绍了状态机模型和TLA+语言，并使用它们来指定简单的计数器和队列数据结构。文章详细解释了线性一致性的概念，并提供了一个使用TLA+对线性一致性队列进行建模的示例。为了解决传统求精映射的局限性，文章引入了预言变量的概念，并以Herlihy和Wing队列为例说明了如何使用预言变量来证明线性一致性。
阅读更多
本文讨论了谷歌前首席执行官埃里克·施密特对“粘合剂型人才”的轻视态度。 “粘合剂型人才”指那些在不同团队之间充当桥梁，促进合作，但自身并无突出贡献的人。施密特认为这些“粘合剂型人才” 效率低下，试图将他们从公司剔除。作者对这种观点提出质疑，并引发了关于“粘合剂型人才”在组织中作用的讨论。
阅读更多
这篇文章讨论了系统可用性问题中的帕累托法则（80/20法则）的局限性。作者认为，将事故归因于单一“根本原因”的RCA模型存在缺陷，因为事故往往是多个因素相互作用的结果。作者指出，系统可用性更像是由各种组件和防御机制共同作用产生的，而事故则是这些机制无法完全阻止的“误差项”。因此，简单地将事故归因于少数几个主要原因并不能有效解决问题，我们需要关注系统中各个组件之间的交互和潜在冲突。
阅读更多
本文探讨了不变式在软件开发中的问题，重点关注它们在随着时间推移而改变时所遇到的挑战。文章从一个例子开始，说明了不可变性如何随着时间的推移而失效，并讨论了这个问题的潜在原因，包括不断变化的需求、技术的进步和环境因素。文章继续讨论了应对这一挑战的策略，例如使用松散不变式和设计允许不变式随着时间演变的系统。最后，文章总结了不变式在软件开发中的重要性，同时强调了认识其局限性和制定策略来应对这些局限性的必要性。
阅读更多