不管市场上有哪些静态分析工具，理论上是否有可能使用静态分析工具证明 Java（或任何其他命令式语言）代码没有竞争条件？
问问题
286 次
3 回答
4
“Java 代码没有竞争条件”这句话非常含糊。也许您的意思是其中之一：
静态分析工具能否证明没有 Java 程序存在竞态条件？显然不是，因为确实存在具有竞争条件的 Java 程序。
静态分析工具是否总能证明无竞态条件的 Java 程序没有竞态条件？不，因为这相当于解决了停止问题（在可能终止也可能不终止的循环之后放置一个静态竞争条件。要判断竞争是否会实际发生，您需要知道循环是否终止）。
静态分析工具有时能证明无竞争条件的 Java 程序没有竞争条件吗？是的。事实上，这样的工具可能会非常有用。
于 2012-04-25T16:23:49.330 回答
2
这只是我的直觉，但我会说不，至少对于一般的 Java 程序来说。证明某些程序不存在竞争条件应该不难（通常，任何单线程程序，识别单线程并不难）。但是要为所有Java程序做出决定？我怀疑 Java 的并发模型对此太无限制了。
我认为有可能证明在任意 Java 代码中确定不存在竞争条件等同于停止问题，因为某些东西（最明显的是公共静态字段）可以被所有线程隐式访问，并且它们可以通过以下方式访问反射，使用任意复杂的代码确定用于查找它们的字符串。
于 2012-04-25T16:17:57.370 回答
0
这应该可以使用像 spin (http://spinroot.com/spin/whatispin.html) 这样的模型检查器。
但是，您需要创建从 java 到模型语言的翻译，并且这种类型的模型检查在计算上非常昂贵（包括占用大量内存），因此它的可行性是另一个问题。
如其他答案所述，对于特别复杂的代码，可能很难或不可能进行适当的建模，这些代码会掩盖实际调用或访问的数据成员。但是，对于合理的代码，这实际上在数学上不应该是不可能的（而不是真的很慢）。
也不可能考虑代码外部的任何特定竞争条件 - 因此，如果存在竞争条件的真正风险，将某些东西建模为非原子的原子 IO 操作将导致模型无效。
于 2012-04-25T16:10:10.267 回答