Sebastian Wolff 是 Simons Society of Fellows 的初级研究员十几岁的时候，塞巴斯蒂安·沃尔夫 ( Sebastian Wolff ) 梦想成为一名建筑师，但当他发现自己有编码天赋时才转向计算机科学。他进入大学希望成为公司 IT 部门的计算机程序员。当他被创造优雅的计算机代码的挑战所吸引时，沃尔夫的兴趣再次转向，这一次转向了计算机科学的理论基础。
沃尔夫在德国布伦瑞克工业大学获得博士学位，现在是纽约大学库朗研究所的博士后，在 Thomas Wies 的指导下。作为Simons Society of Fellows的第一年初级研究员，Wolff 使用理论来解决由并发计算机系统的出现引起的实际计算机问题，其中一台计算机或一组计算机同时处理许多任务。
沃尔夫和我最近讨论了他的工作。为了清楚起见，我们的对话已经过编辑。
什么是“并发”计算机系统？
在计算机编程的早期，一切都是连续的：一个任务在下一个任务开始之前完成。但是今天，事情变得更加复杂了。计算机是“并发的”，这意味着它们可以同时执行许多任务。这种转变的发生部分是因为我们达到了顺序计算的速度极限。但随着全球可用 Web 服务的稳步增长，并发性也自然而然地出现了。例如，人们希望他们访问过的每个网站都能立即加载且没有任何错误。如果没有并发，这是不可能发生的。
并发计算可以在单个服务器上执行，也可以在多个连接在一起的服务器上执行。假设您和我都想在亚马逊上购买相同的商品，而世界上只剩下一件。我可能正在欧洲的服务器上搜索，而您将相同的物品放在美国服务器上的购物车中。也许我比您早几分钟下订单，但是该商品在美国仓库中，因此可以比发送给我的速度更快地运送给您，而亚马逊的成本更低。
我是按照先到先得的原则获取商品，还是根据后勤便利获取商品？亚马逊是向我们双方出售相同的东西并向我们中的一个人退款，还是拒绝向我们中的任何一个人出售并希望以后只有一个人寻找它？这些选项中的每一个都是嵌入在计算机代码中的决策。之所以会出现复杂性，是因为这些决策都是同时做出的。在旧的顺序世界中，我的订单会毫无疑问地占上风，因为我把它放在了第一位。故事结局。但今天几乎从来没有这种情况。
在您刚刚描述的情况下，如果只有一件物品可用，该程序似乎只允许出售一件物品——无论其位置如何，这似乎是理想的。计算机理论是如何出现的？
如您所见，并发程序中的决策非常复杂。这反映在代码中，代码也很复杂。事实上，即使是最优秀的程序员也会在他们编写的代码中犯错误。而这些错误会导致不受欢迎和意想不到的行为，例如两次出售一件商品。
计算机理论——或者我们喜欢称之为形式化的方法——提供了检查你编写的代码并使你能够查看你的程序是否按预期运行的机制。激发我兴趣的是形式化方法可以应用于任何潜在的代码或程序。有了这些无限的可能性，随之而来的挑战就是提出有用的理论机制。在我的工作中，我和我的合作者通常从研究程序员如何编写代码开始，从中提炼出基本原理，然后将这些原理转化为理论。
您如何使用理论来测试代码是否有效？
这有两个方面：在不同条件下测试代码的输出，然后在所有可能的条件下验证该代码。
测试正是它听起来的样子：我们针对一堆不同的场景运行代码，看看它是否按预期运行。在我们的购物示例中，我们可以输入不同的商品并确保只出售仓库中存在的商品。有可能获得 99% 的确定性表明这样的代码可以工作的测试，尽管这对于并发系统来说是不太可能的。从理论上讲，测试永远不会产生 100% 的确定性，因为总有一个参数可以测试。可能性是无止境。确保程序底层代码始终有效是验证的用武之地。
告诉我更多关于验证的信息。
验证分为三类。手动验证是纸笔数学证明，如果适用某些条件，给定的代码将始终有效。这是最容易创建和理解的验证类型，但始终存在错误假设意味着证明无效的风险。因为人们发布了后来证明是错误的手动验证证明，所以这种方法不像以前那样流行。
机械化验证采用人工生成的手动验证，然后运行“证明助手”，本质上是一个检查证明有效性的计算机程序。这比手动验证更可靠，但仍需要大量前期工作来输入机械化验证工具尝试验证的参数。
这给我们带来了自动验证，这是我特别感兴趣的，也是我博士工作的重点。这种类型的验证涉及编写算法来证明程序是否将始终有效。这是有利的，因为它不需要预先投入这样的时间，同时也可供非专家使用。
您在博士工作期间验证了什么？
我研究的一个关键基础是数据结构的概念。从广义上讲，数据结构维护着一组相互链接的对象，以及管理这些对象之间关系的规则。字典中的单词集合是一种数据结构，例如，在线市场中的产品集合也是如此。
非阻塞数据结构的手动证明大纲，即所谓的 Harris 列表。代码（黑色）使用分离逻辑用证明参数（蓝绿色）进行注释。信用：迈耶等人。 , 具有未来和历史的并发程序逻辑，正在提交中。我在读研究生期间开始感兴趣的是内存回收，或者从数据结构中删除并且不再使用的项目会发生什么。例如，门票销售已关闭的音乐会网页应该如何处理？你会在演唱会发生很久之后永远离开售票网站吗？您是否完全删除该页面？如果是这样，你什么时候删除它？
许多数据结构会使项目保持原样并定期扫描所有项目以删除那些没有更多传入链接的项目。这需要时间和资源。手动删除项目有时是首选，但也不完美；很难以不再访问已删除项目的方式进行操作。
在我的研究中，我提出了一组关于数据结构的条件，以保证上述手动删除和定期扫描和删除过程的使用是无法区分的。这种方法通过防止访问已删除的项目来减少系统崩溃。更重要的是，在验证过程中摒弃了手动删除的过程，也让整个过程变得简单了许多。我们是第一个为这些类型的数据结构提出自动验证的小组。程序员可以完全以这种方式使用我们的工作，使两个删除过程之间的切换更容易。
在哈里斯的名单上运行全自动工具浮游生物。 （镜头加速。）该工具将程序代码作为输入，然后生成正确性证明，无需任何工作。信用：迈耶等人。 , 具有未来和历史的并发程序逻辑，正在提交中。
多么激动人心！你现在在做什么？
我的博士工作专注于解决一类数据结构中的挑战。虽然我们的理论是通用的，但为了我们的实际结果，我们不得不限制数据结构的一个方面：项目如何链接在一起。在纽约大学担任博士后期间，我想利用那次经验中的原则，为面临更大数据结构集的类似挑战提供自动化解决方案。
最后，您对西蒙斯团契有何看法？
在计算机科学中，输出可以波涛汹涌：有时什么都没有发生，有时一切都同时发生。所以，西蒙斯基金会三年来无限制的支持真是一件幸事。这个初级奖学金给了我资源和时间来跟随我的研究道路。
原文： https://www.simonsfoundation.org/2022/04/27/computers-have-memories-too/