用于检测F#中并发问题的代码分析器

Question

我正在寻找一些代码分析工具(静态或动态分析)，可以检测并发问题，如竞态条件或F#程序中的死锁。

我知道F#是基于“参与者模型”的，并且它有一些固有的并发支持，所以我假设可能会出现竞争条件和死锁等问题。如果是这样的话，我想知道是否有任何工具可以接收F#源代码并找到可能发生此类问题的程序点。

有人对此有什么想法吗？提前感谢！

Answer 1

我不认为有任何工具可以做到这一点。这仍然是一个非常困难的问题(考虑到程序状态爆炸)。微软研究院开发了用于并发测试的CHESS tool、Win32和.NET代码(面向锁和可变数据)，该工具仍处于实验阶段，我不认为已经开发或至少发布了更多版本。

因此，解决这个问题的最好方法仍然是模型检查。也就是说，根据您的问题开发一个抽象模型，并使用特定的工具来分析此模型。例如，CSP是一种用于对交互进行建模的语言(面向角色模型)，而FDR是一种用于在这些模型中发现并发问题的工具。

顺便说一句，F#不是基于角色模型的。您可以使用mailboxes实现角色模型，但也可以使用锁和可变数据(相关，因为检查器工具需要同时检查这两种方法)。