在工作中你曾经遇到过停机问题吗?这可能是当你的同事/老板提出了一种违反计算基本限制的解决方案,或者当你自己意识到你试图解决的问题实际上是无法解决的时候。
我最近遇到的一个例子是在学习类型检查器时。我们班意识到,要编写一个完美的类型检查器(接受所有不会发生类型错误的程序,并拒绝所有会发生类型错误的程序)是不可能的,因为这实际上就是要解决停机问题。另一个例子是我们在同一门课程中意识到,在类型检查阶段确定除数是否为零也是不可能的,因为在运行时检查数字是否为零,也是停机问题的一种版本。
在工作中你曾经遇到过停机问题吗?这可能是当你的同事/老板提出了一种违反计算基本限制的解决方案,或者当你自己意识到你试图解决的问题实际上是无法解决的时候。
我最近遇到的一个例子是在学习类型检查器时。我们班意识到,要编写一个完美的类型检查器(接受所有不会发生类型错误的程序,并拒绝所有会发生类型错误的程序)是不可能的,因为这实际上就是要解决停机问题。另一个例子是我们在同一门课程中意识到,在类型检查阶段确定除数是否为零也是不可能的,因为在运行时检查数字是否为零,也是停机问题的一种版本。
我被指派去解决停机问题,也就是说,“编写一个监控插件来确定主机是否永久宕机”。真的吗?好的,那我只需设置一个阈值。“不行,因为之后可能会重新启动。”
随后进行了大量的理论阐述。
import antigravity
之类的东西...) - Roman Starkovhost.self_destruct(); print("Permanently down.");
。 - Mateen Ulhaq多年前,我记得在 Byte 杂志上读到了一篇关于一个名为 Basic Infinite Loop Finder 或 BILF 的产品的评论。BILF 被认为可以扫描您的 Microsoft Basic 源代码并查找任何未终止的循环。它声称能够发现代码中的任何无限循环。
评论者足够精明,指出要使该程序在所有情况下都能工作,它必须解决停机问题,甚至提供了为什么它不能在所有情况下工作的数学证明。
在下一期中,他们刊登了一封来自该公司代表的信,解释说该问题将在下一版本中得到解决。
更新: 我在 imgur 上找到了一张文章图片。我记错了杂志名,它是 Creative Computing,而不是 Byte。除此之外,基本上就像我记得的那样。
你可以在 imgur 上看到一张高清版本的图片。
我现在正在开发的项目中存在许多无法解决的问题。这是一个单元测试生成器,通常它试图回答问题"这个程序做了什么",这是停机问题的一个实例。在开发过程中出现的另一个问题是"是否给定两个(测试)函数相同"?或者甚至是"这两个调用(断言)的顺序是否重要"?
这个项目有趣的地方在于,即使你不能在所有情况下回答这些问题,你仍然可以找到聪明的解决方案来解决90%的问题,对于这个领域来说实际上非常好。
其他试图推理其他代码的工具,如优化编译器/解释器、静态代码分析工具,甚至是重构工具,很可能会遇到(因此被迫寻找解决方法)停机问题。
例子1:我的报告有多少页?
在学习编程时,我尝试创建一个从数据中打印漂亮报告的工具。显然,我希望它非常灵活和强大,以便成为所有报告生成器的终极工具。
报告定义非常灵活,以至于它是图灵完备的。它可以查看变量,选择不同的选项,使用循环重复执行操作。
我定义了一个内置变量N,表示报告实例中的页数,因此您可以在每一页上放置一个字符串,例如“第n页,共N页”。我进行了两遍计算,第一遍用于计算页面数(在此期间将N设置为零),第二遍用于生成页面,使用从第一遍获得的N。
有时,第一遍计算出N,而第二遍会生成不同数量的页面(因为现在非零的N会改变报告的作用)。我尝试进行迭代式的计算,直到N稳定下来。然后我意识到这是没有希望的,因为如果它不能稳定下来会怎样呢?
这就引出了一个问题,“如果迭代永远无法在报告产生的页数的稳定值上达成一致,我是否至少可以检测并警告用户?”幸运的是,此时我已经对图灵、哥德尔和可计算性等方面产生了兴趣,并且做出了联系。
多年后,我注意到Microsoft Access有时会打印“第6页,共5页”,这真是一件奇妙的事情。
例子2:C++编译器
编译过程涉及扩展模板。可以从多个特化中选择模板定义(足以作为“条件”),它们也可以是递归的。因此,这是一个图灵完备(纯函数)元系统,在其中模板定义是语言,类型是值,而编译器实际上是解释器。这是一个意外。
因此,不可能检查任何给定的C++程序并说编译器是否原则上能够成功编译该程序。
编译器供应商通过限制模板递归的堆栈深度来解决此问题。您可以在g++中调整深度。
很久以前,我曾协助公司一位顾问实施一个非常复杂的铁路系统,以便将装有金属零件的篮子从1500度高温炉中运出和运入。轨道本身是一个相当复杂的“小型铁路场”,在车间地面上交叉了几个地方。几个电动托盘会按照时间表来回穿梭,运送零件篮子。炉门尽可能短地开启时间非常重要。
由于工厂正在全力生产,该顾问无法使用“实时”运行软件来测试他的调度算法。相反,他编写了一个漂亮的图形模拟器。当我们看着虚拟托盘在屏幕上移动时,我问他:“您如何知道是否存在任何调度冲突?”
他迅速回答说:“很简单——模拟器永远不会停止。”
复杂的静态代码分析可能会遇到停机问题。
例如,如果Java虚拟机能够证明一段代码永远不会访问数组越界,它可以省略该检查并运行得更快。对于某些代码来说,这是可能的;但随着代码变得越来越复杂,问题就变成了停机问题。
这在GPU应用程序中对着色器仍然是一个问题。 如果一个着色器有一个无限循环(或者计算量非常大),驱动程序应该(在一定时间限制后)停止它,杀死片段,还是让其运行? 对于游戏和其他商业内容,前者可能是您想要的,但对于科学/GPU计算,后者是您想要的。 更糟糕的是,某些Windows版本会假设由于一段时间内图形驱动程序没有响应,就将其杀死,这在使用GPU进行计算时人为地限制了计算能力。
目前不存在API可供应用程序控制驱动程序的行为或设置超时或其他内容,而且驱动程序也无法告知你的着色器是否会完成或不会完成。
我不知道这种情况最近是否有所改善,但我想知道。
我找到了一篇伯克利的论文:Looper: Lightweight Detection of Infinite Loops at Runtimehttp://www.eecs.berkeley.edu/~jburnim/pubs/BurnimJalbertStergiouSen-ASE09.pdf
LOOPER可能很有用,因为大多数无限循环都是微不足道的错误。然而,这篇论文甚至没有提到停机问题!
他们对自己的局限性有什么说法?
[LOOPER]通常无法推理出非终止取决于每个循环迭代中堆突变的循环。这是因为我们的符号执行在具体化指针方面比较保守,而我们的符号推理则不够强大。我们相信将我们的技术与形状分析和更强大的不变量生成和证明相结合将是有价值的未来工作。
换句话说,“问题将在下一个版本中得到解决”。