证明多线程算法的正确性

多线程算法特别难以设计/调试/证明.Dekker的算法是设计正确的同步算法有多么困难的一个主要例子.Tanenbaum的现代操作系统在其IPC部分中充满了示例.有没有人有这方面的好参考(书籍,文章)？谢谢!

没有建立在guarentees上的东西是不可能证明的,所以你要做的第一件事就是熟悉目标平台的内存模型; Java和x86都有可靠和标准化的内存模型 - 我对CLR不太确定,但如果其他所有方法都失败了,那么你将建立在目标CPU架构的内存模型上.这个规则的例外是如果你打算使用一种不允许任何共享可变状态的语言 - 我听说过Erlang就是这样.

并发的第一个问题是共享可变状态.

这可以通过以下方式解决:

使状态不变

不共享国家

通过相同的锁保护共享的可变状态(两个不同的锁不能保护同一个状态,除非你总是使用这两个锁)

并发的第二个问题是安全发布.如何将数据提供给其他线程？你是如何进行移交的？您将在内存模型中解决此问题,并且(希望)在API中.例如,Java有许多发布状态的方法,java.util.concurrent包中包含专门用于处理线程间通信的工具.

并发的第三个(也是更难的)问题是锁定.错误管理的锁定顺序是死锁的来源.您可以通过分析证明,在内存模型guarentees的基础上,您的代码中是否可以使用死锁.但是,您需要在设计和编写代码时考虑到这一点,否则代码的复杂性会很快导致这种分析无法在实践中执行.

然后,一旦你有,或在你做之前,证明正确使用并发,你将必须证明单线程的正确性.并发代码库中可能出现的错误集等于单线程程序错误集,以及所有可能的并发错误.