静态线程分析:好主意?

我帮助维护和构建一个相当大的Swing GUI,有很多复杂的交互。我经常发现自己修复了一些错误,这些错误是由于代码中其他位置的某个竞争条件而导致事情进入奇数状态的结果。

随着代码库变得越来越大,我发现在通过文档指定哪些方法具有线程限制方面,代码库变得不那么一致:最常见的是必须在 Swing EDT 上运行的方法。同样,了解并提供静态感知,通过规范在 EDT 上通知哪些(我们的自定义)侦听器,这将是很有用的。

因此,我突然想到,这应该是可以使用注释轻松执行的东西。瞧,至少有一个静态分析工具CheckThread,它使用注释来完成这项工作。它似乎允许您将方法声明为限制在特定线程(最常见的是 EDT)中,并且将标记尝试调用该方法的方法,而不同时将自身声明为仅限于该线程。

因此,从表面上看,这似乎是对源代码和构建周期的低痛苦,巨大收益的补充。我的问题是:

  • 对于使用CheckThread或类似库来强制实施线程约束的人来说,是否有任何成功案例?任何失败的故事?为什么成功/失败?
  • 这在理论上是好的吗?理论上有缺点吗?
  • 这在实践中是好的吗?值得吗?它带来了什么样的价值?
  • 如果它在实践中有效,那么支持这一点的好工具是什么?我刚刚找到了CheckThread,但承认我不完全确定我在寻找什么来找到其他做同样事情的工具。

我知道它是否适合我们取决于我们的方案。但我从未听说过有人在实践中使用这样的东西,说实话,它似乎并没有从一些一般的浏览中占据主导地位。所以我想知道为什么。


答案 1

这个答案更侧重于您问题的理论方面。

从根本上说,您正在做出断言:“此方法仅在某些线程下运行”。此断言与您可能做出的任何其他断言(“该方法仅接受参数 X 小于 17 的整数”)没有什么不同。问题是

  • 这种说法从何而来?
  • 静态分析仪可以检查它们吗?
  • 您从哪里获得这样的静态分析仪?

大多数情况下,这样的断言必须来自软件设计人员,因为他们是唯一知道意图的人。传统的术语是“按合同设计”,尽管大多数DBC方案仅基于当前程序状态(C的断言宏),并且它们实际上应该超过程序的过去和未来状态(“时间断言”),例如,“此例程将分配一个存储块,最终某些代码段将解除分配它”。人们可以构建工具,试图以色调确定断言是什么(例如,恩格勒的断言归纳工作;其他人在这方面已经做了工作)。这很有用,但误报是一个问题。实际上,要求设计人员编写这样的断言似乎并不特别繁重,而且从长远来看,这确实是很好的文档。无论你是用特定的“Contract”语言构造,还是用if语句(“if Debug && Not(assertion) Then Fail();”)或将它们隐藏在注释中,这实际上只是一个方便的问题。当语言允许直接编码这样的断言时,它很好。

静态检查此类断言很困难。如果只坚持使用当前状态,则静态分析器几乎必须对整个应用程序进行完整的数据流分析,因为满足断言所需的信息可能来自应用程序的另一部分创建的数据。(在你的例子中,“inside EDT”信号必须来自分析应用程序的整个调用图,以查看是否有任何调用路径从不是EDT线程的线程通向方法)。如果使用时态属性,则静态检查几乎还需要某种状态空间验证逻辑。这些目前仍然是几乎的研究工具。即使使用所有这些机器,静态分析仪通常也必须在使用中“保守”;如果他们不能证明某些东西是假的,他们几乎不得不假设它是真的,因为停止问题。

您从哪里获得这样的分析仪?考虑到所需的所有机器,它们很难建造,所以你应该期望它们是罕见的。如果有人建造了一个,那就太好了。如果没有...作为一般规则,您不希望自己从头开始执行此操作。从长远来看,最好的希望是拥有通用的程序分析机制来构建这样的分析仪,以分摊构建所有基础设施的成本。(我构建程序分析器工具基础;请参阅我们的 DMS 软件再设计工具包)。

使构建此类静态分析器“更容易”的一种方法是将它们处理的案例限制在狭窄的范围内,例如CheckThread。我希望CheckThread能够完全按照它目前的作用去做,而且它不太可能变得更强大。

“断言”宏和其他此类动态“当前状态”检查之所以受欢迎,是因为它们实际上可以通过简单的运行时测试来实现。这很实用。这里的问题是,您可能永远不会执行导致失败条件的路径。因此,对于动态分析,没有检测到的故障并不是正确性的真正证据。还是感觉不错。

底线:静态分析仪和动态分析仪各有其优势。


答案 2

我们还没有尝试过任何静态分析工具,但是我们已经使用AspectJ编写了一个简单的方面,该方面可以在运行时检测java.awt或javax.swing中的任何代码何时在EDT之外被调用。它在我们的代码中发现了几个缺少.我们在整个 QA 周期中都启用了这一方面,然后在发布前不久将其关闭。SwingUtilities.invokeLater()