solidot新版网站常见问题,请点击这里查看。

如何编写数学上完美的软件

软件 数学
wanwan (42055)发表于 2022年05月18日 15时01分 星期三

来自太空战
Leslie Lamport 的名字可能不是家喻户晓,但作为计算机科学家,他比起那些名人不遑多让:排版程序 LaTeX 以及让 Google 和亚马逊云基础设施成为可能。他对一些问题给予了更多的关注,给它们起了独特的名字,比如面包店算法和拜占庭将军问题。这绝非偶然。这位 81 岁的计算机科学家对于人们如何使用和看待软件有着不同寻常的深入思考。2013 年,他赢得了被认为是计算领域诺贝尔奖的A.M.图灵奖,以表彰他在分布式系统方面的工作,此类系统由不同网络上的多个组件相互协调实现共同目标。互联网搜索、云计算和人工智能都涉及编排强大的计算机军团协同工作。当然这种协调也会给你带来更多的问题。Lamport曾说过:“分布式系统是这样一个系统:一台你甚至不知道其存在的计算机出现故障,就可能导致你自己的计算机无法使用。”

问题的最大来源之一是“并发系统”,其中多个计算操作发生在重叠的时间片中,导致模棱两可:哪台计算机的时钟是正确的?在 1978 年的一篇开创性论文中,Lamport 借鉴狭义相对论的见解,引入了“因果关系”概念解决这个问题。两个观察者可能在事件的顺序上存在分歧,但如果一个事件导致另一个事件,这就消除了分歧。并且发送或接收消息可以在多个进程之间建立因果关系。逻辑时钟——现在也称为 Lamport 时钟——提供了一种推理并发系统的标准方法。有了这个工具,计算机科学家接下来想知道他们如何能系统地使这些联网计算机变得更大,而不会增加错误。Lamport 提出了一个优雅的解决方案:Paxos,一种允许多台计算机执行复杂任务的“共识算法”。如果没有 Paxos 及其算法家族,现代计算就不可能存在。