多线程算法特别是很难设计/调试/证明。德克尔的算法是如何努力，它可以设计出正确的同步算法，一个典型的例子。 Tanenbaum的的现代操作系统中充满了在其IPC部分例子。有没有人有一个很好的参考（书籍，文章）的呢？谢谢！

Multithread algorithms are notably hard to design/debug/prove. Dekker's algorithm is a prime example of how hard it can be to design a correct synchronized algorithm. Tanenbaum's Modern operating systems is filled with examples in its IPC section. Does anyone have a good reference (books, articles) for this? Thanks!

推荐答案

这是不可能证明什么，而不在guarentees建设，所以你要做的第一件事就是要熟悉目标平台的内存模型; Java和86都具有坚实的和标准化的内存模型 - 我不敢肯定CLR，但如果一切都失败了，你必须在你的目标CPU架构的内存模型的构建。如果你打算使用确实不允许任何共享可变状态在所有语言的例外就是 - 我听说Erlang是这样

It is impossible to prove anything without building upon guarentees, so the first thing you want to do is to get familiar with the memory model of your target platform; Java and x86 both have solid and standardized memory models - I'm not so sure about CLR, but if all else fails, you'll have build upon the memory model of your target CPU architecture. The exception to this rule is if you intend to use a language that does does not allow any shared mutable state at all - I've heard Erlang is like that.

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

The first problem of concurrency is shared mutable state.

这可以是固定的方式：

在制作状态不变 在不共享状态 在镇守共享的可变状态的一样的锁（两个不同的锁不能守护在同一块的状态，除非你的总是的使用正是这两个锁） Making state immutable Not sharing state Guarding shared mutable state by the same lock (two different locks cannot guard the same piece of state, unless you always use exactly these two locks)

并发的第二个问题是安全的出版物。你如何提供给其他线程的数据？你如何进行切换？你会在内存模型解决这一问题，（希望）的的API中。爪哇，举例来说，有许多方法来发布状态和java.util.concurrent包包含专门用来处理线程间通信的工具。

The second problem of concurrency is safe publication. How do you make data available to other threads? How do you perform a hand-over? You'll the solution to this problem in the memory model, and (hopefully) in the API. Java, for instance, has many ways to publish state and the java.util.concurrent package contains tools specifically designed to handle inter-thread communication.

并发的三分之一（难）问题是锁定。管理不善锁订购是死锁的来源。您可以解析证明，在内存模型guarentees建设，死锁是否是可能的在code。但是，你需要设计和编写code考虑到这一点，的code，否则的复杂性可以快速呈现这样的分析不可能在实践中执行。

The third (and harder) problem of concurrency is locking. Mismanaged lock-ordering is the source of dead-locks. You can analytically prove, building upon the memory model guarentees, whether or not dead-locks are possible in your code. However, you need to design and write your code with that in mind, otherwise the complexity of the code can quickly render such an analysis impossible to perform in practice.

然后，一旦你有，或在你这么做之前，证明正确使用并发的，你必须证明单线程的正确性。这组可能发生在并发code碱基错误等于一套单线程程序的bug，以及所有可能的并发错误。

Then, once you have, or before you do, prove the correct use of concurrency, you will have to prove single-threaded correctness. The set of bugs that can occur in a concurrent code base is equal to the set of single-threaded program bugs, plus all the possible concurrency bugs.