编程语言与软件工程2014research.microsoft.com编辑精选
Amazon Web Services 中形式化方法的使用（2013）
Use of Formal Methods at Amazon Web Services (2013)
进阶 · 约 45 分钟读完前置知识：分布式系统基础、TLA+ 基础、并发与一致性模型
导读
这篇论文（2013 年，作者来自 AWS 与 Microsoft Research，含 Leslie Lamport）总结 Amazon Web Services 在 S3、DynamoDB 等关键分布式系统中使用 TLA+ 形式化规约的工程经验：先用可执行的形式化模型在设计阶段发现那些代码评审和测试难以发现的深层并发与一致性 bug（文中举例一个需 35 步才复现的 bug），再讨论形式化方法的能力边界。作者明确指出，TLA+ 擅长第一类问题：逻辑设计错误和操作失误；但第二类问题，即由反馈回路引起的“持续性涌现性能退化”（如 GC 停顿引发超时、重试、雪崩），目前难以用硬实时安全性质建模，因为底层基础设施不提供硬实时保证。
HN 关注点：工业界主流公司（AWS）实际落地形式化方法的经验，尤其是它能否发现常规测试漏掉的深层 bug，以及模型的规模、故障建模与模型检查耗时等实际问题。
后来怎么样
该文成为工业界采用 TLA+ 的标志性案例，推动 AWS 在 S3、DynamoDB 等关键系统中持续使用形式化规约，并影响其他公司引入轻量形式化方法。
HN 评论精选
这几条评论里：支持 1 质疑 2 补充 1
补充指出形式化方法能解决逻辑错误，但难以建模反馈回路导致的性能雪崩；这类问题即使没有逻辑 bug 也会让系统不可用。
大型分布式系统有两类主要问题：1) 导致系统偏离逻辑意图的 bug 和操作员错误；2) 复杂系统里的反馈回路引起、令人意外的“持续性涌现性能退化”。我们知道如何用形式化规约来发现第一类问题，但第二类问题即使不涉及逻辑 bug，也能让系统瘫痪。常见例子：服务器短暂变慢（比如 Java GC），导致客户端超时，客户端重试请求，给服务器增加更多负载，使其进一步变慢。这种场景下系统最终仍会前进，并非逻辑死锁、活锁或其他循环，但从客户角度看，由于响应时间持续不可接受，系统实际上等于不可用。可以用 TLA+ 把响应时间上界写成实时安全性质，但我们的系统建在不支持硬实时调度或保证的基础设施（磁盘、操作系统、网络）上，所以实时安全性质不现实。我们构建的是软实时系统，短时间的慢响应不算错误，但长时间严重变慢算错误。我们目前还不知道有什么可行方法来建模真实系统……
gone35查看英文原文
We are concerned with two major classes of problems with large distributed systems; 1) bugs and operator errors that cause a departure from the logical intent of the system, and 2) surprising 'sustained emergent performance degradation' of complex systems that inevitably contain feedback loops. We know how to use formal specification to find the first class of problems. However, problems in the second category can cripple a system even though no logic bug is involved. (...) A common example is when a momentary slowdown in a server (perhaps due to Java garbage collection) causes timeouts to be breached on clients, which causes the clients to retry requests, which adds more load to the server, which causes further slowdown. In such scenarios the system will eventually make progress; it is not stuck in a logical deadlock, livelock, or other cycle. But from the customer's perspective it is effectively unavailable due to sustained unacceptable response times. (...) TLA+ could be used to specify an upper bound on response time, as a real-time safety property. However, our systems are built on infrastructure (disks, operating systems, network) that do not support hard real-time scheduling or guarantees, so real-time safety properties would not be realistic. We build soft real-time systems in which very short periods of slow responses are not considered errors. However, prolonged severe slowdowns are considered errors. We don't yet know of a feasible way to model a real system that would enable tools to predict such emergent behavior. Interesting. TLA+ of course allows for hybrid specifications that incorporate physical constraints --real-time itself being the prime example--, so constraints based on more complicated 'loss functions' like, say, weighted average or total variation of response times, in principle ought to be feasible as well. Leslie Lamport himself laments such specifications are still 'of only academic interest' [1, §9.5], so I wonder how impractical such specifications could they really get. [1] http://research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf
质疑提出三个实践性问题：故障类型如何建模、能否只对部分服务隔离建模、无 bug 时穷尽模型检查的耗时。
很酷的工作。我有几个问题：1) 你们如何建模分布式系统中可能出现的各种故障类型？2) 是否可以对系统做部分建模？比如在 SOA 中，一个服务的行为可能严重依赖其他服务的行为，能否孤立地对每个服务建模并得出有意义的结果？3) 模型检查的运行时间可控吗？论文提到几秒钟就能找到 bug，但要把没有 bug 的模型穷尽检查需要多久？
saosebastiao查看英文原文
Really cool stuff. I have a couple of questions: 1) How do you model the myriad fault types that could possibly occur in distributed systems? 2) Is it possible to partially model a system? For example, in SOA, the behavior of a service can depend on and be greatly affected by the behavior of other services. Can each service be modeled in isolation with meaningful results? 3) Is the run time of model checking managable? The paper mentioned a few seconds to find bugs, but how long to exhaustively check a model without bugs?
支持最赞赏论文中“35 步才出现的 bug 逃过评审与测试”的案例，认为模型检查比完整形式验证更省力，并呼吁关键软件广泛采用。
最精彩的部分是关于发现一个需要 35 步才显现、并且同时通过了代码评审和测试的 bug。能捕捉这种极隐蔽问题是形式化方法长期文献中记载的优势；TLA+、SPIN 这类模型检查器让这件事所需的技巧和时间都少于完整的形式化验证。此外，这些性质还能和 Design-by-Contract、静态分析等方法结合，消除 80–90% 常见问题。如今大多数关键软件若不用这些工具，已几乎找不到不用的理由；连一家主流公司都已经想明白了。希望看到更多采用。 :)
nickpsecurity查看英文原文
The best part was the section about finding a bug that took 35 steps to show up which got through both code reviews and testing. The ability to catch such obscure stuff is a benefit of formal methods that's been in the literature a long time. Model-checkers like TLA+ and SPIN let it get done with less skill and time than full, formal verification. Further, the properties can be combined with methods like Design-by-Contract and static analysis to knock out problems that show up 80-90% of the time. Hardly any justification anymore to not be using these tools for most critical software. Even a mainstream company has figured it out. Hopefully, we'll see more adoption. :)
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
- 评论区提到的论文
历次讨论
- 2014Hacker News 讨论帖91 分 · 13 评
- 2016Hacker News 讨论帖84 分 · 5 评
同领域还值得读
Google 的软件工程（2017）
Software Engineering at Google (2017)
介绍了 Google 的软件工程实践，包括其单一代码库（monorepo）、几乎全部开发在主干进行而非分支、代码审查、构建系统 Blaze、协议缓冲区等工具与流程，并讨论了频繁重…
编程语言与软件工程2017 · 1,127 分 · 465 评 · 引用 15入门 · 约 45 分钟编辑精选Peter Naur：编程作为理论构建 (1985)
Peter Naur – Programming as Theory Building (1985)
Peter Naur 1985 年的经典论文《Programming as Theory Building》提出：编程的本质不是写代码或文档，而是在程序员头脑中构建对程序及其运行…
编程语言与软件工程2016 · 629 分 · 74 评入门 · 约 45 分钟编辑精选SciPy 1.0：Python 科学计算的基础算法
SciPy 1.0: fundamental algorithms for scientific computing in Python
这篇发表于 Nature Methods 的论文介绍了 SciPy 1.0——Python 科学计算生态的基石库，涵盖其核心算法模块（优化、积分、插值、线性代数等）、软件架构与社…
编程语言与软件工程2020 · 387 分 · 98 评入门 · 约 45 分钟编辑精选Lisp 的历史（1979）
History of Lisp (1979)
这是 Lisp 发明者 John McCarthy 于 1979 年为 HOPL（编程语言史）会议撰写的回顾文章，讲述 Lisp 的起源、设计动机与早期演进，文中也涉及 if 表…
编程语言与软件工程2018 · 352 分 · 44 评入门 · 约 45 分钟编辑精选使用 NumPy 进行数组编程
Array Programming with NumPy
这篇 Nature 文章介绍 NumPy 的数组编程模型及其在科学计算中的核心作用：以 ndarray 为中心，通过向量化操作让 Python 高效处理多维数组。
编程语言与软件工程2020 · 318 分 · 134 评入门 · 约 40 分钟编辑精选