你在这个领域中何时遇到过停机问题?

67

在工作中你曾经遇到过停机问题吗?这可能是当你的同事/老板提出了一种违反计算基本限制的解决方案,或者当你自己意识到你试图解决的问题实际上是无法解决的时候。

我最近遇到的一个例子是在学习类型检查器时。我们班意识到,要编写一个完美的类型检查器(接受所有不会发生类型错误的程序,并拒绝所有会发生类型错误的程序)是不可能的,因为这实际上就是要解决停机问题。另一个例子是我们在同一门课程中意识到,在类型检查阶段确定除数是否为零也是不可能的,因为在运行时检查数字是否为零,也是停机问题的一种版本。


1
静态类型系统难道不只检查变量的类型而非其值吗?我认为你的类在期望静态类型检查器在编译时拒绝运行时错误时,曲解了问题。 - andandandand
1
@dmindreader - 不是的。大多数编译器/类型安全语言确实只检查类型,但通过静态分析有时可以看到某些东西的值范围。考虑一下ReSharper或Coverity如何产生“可能为空值”的警告。 - Robert Fraser
3
我曾担任医疗设备的设计工作。曾有一次,我被要求在一个电池供电的设备中加入一个指示灯来显示电池是否耗尽。 - David Schwartz
1
@DavidSchwartz:电池即使已经没电无法为设备供电,但仍然可以为LED提供足够长的时间,以便被能够更换电池的人注意到。 - endolith
13个回答

61

我被指派去解决停机问题,也就是说,“编写一个监控插件来确定主机是否永久宕机”。真的吗?好的,那我只需设置一个阈值。“不行,因为之后可能会重新启动。”

随后进行了大量的理论阐述。


5
哇,真是让人吃惊。那个人的思维深处一定存在着非常荒谬的逻辑,让我感到十分困惑... - Erik Forbes
14
在.NET中,解决这个问题其实非常容易。只需添加对System.Future的引用,然后可以使用System.Future.Fact类中的一些静态方法。在您的情况下:如果(System.Future.Fact.IsPermanent(在此处检查服务器是否宕机的委托)){...} - Lasse V. Karlsen
5
如果我们讨论的是Python,这个说法会更加可信 :) (不是我不喜欢.NET,但你懂的... import antigravity 之类的东西...) - Roman Starkov
7
不,你才是不合逻辑的。这个程序非常简单:host.self_destruct(); print("Permanently down."); - Mateen Ulhaq
6
@muntoo,你好像在第2行有一些无法到达的代码。 - Filip Haglund
显示剩余5条评论

45

多年前,我记得在 Byte 杂志上读到了一篇关于一个名为 Basic Infinite Loop Finder 或 BILF 的产品的评论。BILF 被认为可以扫描您的 Microsoft Basic 源代码并查找任何未终止的循环。它声称能够发现代码中的任何无限循环。

评论者足够精明,指出要使该程序在所有情况下都能工作,它必须解决停机问题,甚至提供了为什么它不能在所有情况下工作的数学证明。

在下一期中,他们刊登了一封来自该公司代表的信,解释说该问题将在下一版本中得到解决。

更新: 我在 imgur 上找到了一张文章图片。我记错了杂志名,它是 Creative Computing,而不是 Byte。除此之外,基本上就像我记得的那样。

你可以在 imgur 上看到一张高清版本的图片。

enter image description here enter image description here


19
这太搞笑了!有没有可用的副本? - rodion
1
Google上唯一的结果就是这篇帖子和与之相关的链接。 - SLaks
3
这应该是在70年代末或80年代初。当时互联网不太流行;-) - Ferruccio
3
BILF 公司何时停止营业? - Geoffrey Zheng

35

我现在正在开发的项目中存在许多无法解决的问题。这是一个单元测试生成器,通常它试图回答问题"这个程序做了什么",这是停机问题的一个实例。在开发过程中出现的另一个问题是"是否给定两个(测试)函数相同"?或者甚至是"这两个调用(断言)的顺序是否重要"?

这个项目有趣的地方在于,即使你不能在所有情况下回答这些问题,你仍然可以找到聪明的解决方案来解决90%的问题,对于这个领域来说实际上非常好。

其他试图推理其他代码的工具,如优化编译器/解释器、静态代码分析工具,甚至是重构工具,很可能会遇到(因此被迫寻找解决方法)停机问题。


30

例子1:我的报告有多少页?

在学习编程时,我尝试创建一个从数据中打印漂亮报告的工具。显然,我希望它非常灵活和强大,以便成为所有报告生成器的终极工具。

报告定义非常灵活,以至于它是图灵完备的。它可以查看变量,选择不同的选项,使用循环重复执行操作。

我定义了一个内置变量N,表示报告实例中的页数,因此您可以在每一页上放置一个字符串,例如“第n页,共N页”。我进行了两遍计算,第一遍用于计算页面数(在此期间将N设置为零),第二遍用于生成页面,使用从第一遍获得的N。

有时,第一遍计算出N,而第二遍会生成不同数量的页面(因为现在非零的N会改变报告的作用)。我尝试进行迭代式的计算,直到N稳定下来。然后我意识到这是没有希望的,因为如果它不能稳定下来会怎样呢?

这就引出了一个问题,“如果迭代永远无法在报告产生的页数的稳定值上达成一致,我是否至少可以检测并警告用户?”幸运的是,此时我已经对图灵、哥德尔和可计算性等方面产生了兴趣,并且做出了联系。

多年后,我注意到Microsoft Access有时会打印“第6页,共5页”,这真是一件奇妙的事情。

例子2:C++编译器

编译过程涉及扩展模板。可以从多个特化中选择模板定义(足以作为“条件”),它们也可以是递归的。因此,这是一个图灵完备(纯函数)元系统,在其中模板定义是语言,类型是值,而编译器实际上是解释器。这是一个意外。

因此,不可能检查任何给定的C++程序并说编译器是否原则上能够成功编译该程序。

编译器供应商通过限制模板递归的堆栈深度来解决此问题。您可以在g++中调整深度。


21

很久以前,我曾协助公司一位顾问实施一个非常复杂的铁路系统,以便将装有金属零件的篮子从1500度高温炉中运出和运入。轨道本身是一个相当复杂的“小型铁路场”,在车间地面上交叉了几个地方。几个电动托盘会按照时间表来回穿梭,运送零件篮子。炉门尽可能短地开启时间非常重要。

由于工厂正在全力生产,该顾问无法使用“实时”运行软件来测试他的调度算法。相反,他编写了一个漂亮的图形模拟器。当我们看着虚拟托盘在屏幕上移动时,我问他:“您如何知道是否存在任何调度冲突?”

他迅速回答说:“很简单——模拟器永远不会停止。”


6
“meta parts” 是我理解他的轨道系统并不是 Ruby 网络应用程序的原因,直到我了解到高炉的时候。 - Karl
1
元数据!我不得不多次重新阅读我的帖子,直到我理解了你的意思!当然是MetaL! - n8wrl

13

复杂的静态代码分析可能会遇到停机问题。

例如,如果Java虚拟机能够证明一段代码永远不会访问数组越界,它可以省略该检查并运行得更快。对于某些代码来说,这是可能的;但随着代码变得越来越复杂,问题就变成了停机问题。


11

这在GPU应用程序中对着色器仍然是一个问题。 如果一个着色器有一个无限循环(或者计算量非常大),驱动程序应该(在一定时间限制后)停止它,杀死片段,还是让其运行? 对于游戏和其他商业内容,前者可能是您想要的,但对于科学/GPU计算,后者是您想要的。 更糟糕的是,某些Windows版本会假设由于一段时间内图形驱动程序没有响应,就将其杀死,这在使用GPU进行计算时人为地限制了计算能力。

目前不存在API可供应用程序控制驱动程序的行为或设置超时或其他内容,而且驱动程序也无法告知你的着色器是否会完成或不会完成。

我不知道这种情况最近是否有所改善,但我想知道。


7
另一个常见的版本是“我们需要消除多线程代码中的任何死锁”。从管理角度来看,这是一个完全合理的请求,但为了防止死锁的发生,您必须分析软件可能进入的每种可能的锁定状态,这等效于停机问题。
有一些方法可以通过在锁定之上强加另一层(例如定义获取顺序)来部分地“解决”复杂系统中的死锁问题,但这些方法并不总是适用。
为什么这等效于停机问题:
假设你有两个锁A和B,以及两个线程X和Y。如果线程X拥有锁A,并且还想要锁B,而线程Y拥有锁B并且也想要锁A,则会发生死锁。
如果X和Y都可以访问A和B,那么确保永远不会进入错误状态的唯一方法是确定每个线程可以通过代码采取的所有可能路径,以及它们可以在所有这些情况下获取和持有锁的顺序。然后确定两个线程是否可以按不同的顺序获取多个锁。
但是,在一般情况下,确定每个线程可以通过代码采取的所有可能路径等效于停机问题。

1
为什么不可能呢?当然,过度加锁会降低性能,但这并不是停机问题!或者我在这里漏掉了什么吗? - Jaywalker

5
Perl的测试系统维护着一个测试计数器。你可以在程序顶部放置要运行的测试数量,或者声明你不需要跟踪它。这可以防止测试过早结束,但也有其他保护措施,所以并不是很重要。
偶尔会有人试图编写一个程序来为你计算测试数量。当然,这种尝试很容易被简单的循环打败。他们仍然继续前进,使用越来越复杂的技巧来检测循环并猜测迭代次数并解决停机问题。通常他们会声明它只需“足够好”。 这里有一个特别复杂的例子。

2

我找到了一篇伯克利的论文:Looper: Lightweight Detection of Infinite Loops at Runtimehttp://www.eecs.berkeley.edu/~jburnim/pubs/BurnimJalbertStergiouSen-ASE09.pdf

LOOPER可能很有用,因为大多数无限循环都是微不足道的错误。然而,这篇论文甚至没有提到停机问题!

他们对自己的局限性有什么说法?

[LOOPER]通常无法推理出非终止取决于每个循环迭代中堆突变的循环。这是因为我们的符号执行在具体化指针方面比较保守,而我们的符号推理则不够强大。我们相信将我们的技术与形状分析和更强大的不变量生成和证明相结合将是有价值的未来工作。

换句话说,“问题将在下一个版本中得到解决”。


运行时循环检测,当状态空间已知且固定时,实际上是可判定的;请参见http://cs.stackexchange.com/a/11646/2242。 - Andrew

网页内容由stack overflow 提供, 点击上面的
可以查看英文原文,
原文链接