您绝对应该尝试使用Spin模型检查器。

您使用一种称为Promela的简单C语言编写了类似程序的模型，Spin在内部将其转换为状态机。一个模型可以包含多个并行过程。

然后Spin要做的是检查每个进程中是否 有可能要插入的指令 ， 以检查您要测试的任何条件
-通常情况下，没有竞争条件，没有死锁等。大多数这些测试都可以使用assert()语句轻松编写。如果有任何可能违反断言的执行顺序，则会打印出该顺序，否则将为您提供“全部清除”。

（嗯，实际上，它使用了一种更先进，更快速的算法来完成此操作，但这是有效的。默认情况下，将检查所有可访问的程序状态。）

这是一个 了不起的
程序，它获得了2001年ACM系统软件奖（其他获奖者包括Unix，Postscript，Apache，TeX）。我得到了非常迅速地开始使用它，并在一两天能实现的MPI函数模型MPI_Isend()，并MPI_Irecv()在PROMELA。Spin
在转换为Promela进行测试的并行代码的一部分中发现了一些 棘手的 竞争条件。