市場で入手可能な静的解析ツールに関係なく、静的解析ツールを使用して、Java (またはその他の命令型言語) コードに競合状態がないことを理論的に証明することは可能ですか?
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 に答える