多线程算法特别难以设计/调试/证明。Dekker 算法是一个很好的例子，说明了设计一个正确的同步算法是多么困难。Tanenbaum 的现代操作系统在其 IPC 部分中充满了示例。有没有人对此有很好的参考（书籍，文章）？谢谢！
Leandro
问问题
2166 次
6 回答
13
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.
That can be fixed by:
- 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)
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.
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.
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.
于 2008-09-16T17:53:39.877 回答
3
“并发和分布式编程原理”，M. Ben-Ari
ISBN-13：978-0-321-31283-9
他们在网上阅读 safari 书籍：http:
//my.safaribooksonline.com/9780321312839
于 2008-09-18T15:09:27.323 回答
3
于 2008-09-17T22:35:43.983 回答
2
简短的回答：这很难。
从 1980 年代后期开始，DEC SRC Modula-3 和落叶松材料中有一些非常出色的工作。
例如
线程同步：AD Birrell、JV Guttag、JJ Horning、R Levin 使用 Modula-3 进行系统编程的正式规范(1991)，第 5 章
扩展静态检查(1998)，作者：David L. Detlefs、David L. Detlefs、K. Rustan、K. Rustan、M. Leino、M. Leino、Greg Nelson、Greg Nelson、James B. Saxe、James B. Saxe
来自 Modula-3 的一些好想法正在进入 Java 世界，例如 JML，尽管“JML 目前仅限于顺序规范”说intro。
于 2008-09-16T19:08:37.607 回答
1
我没有任何具体的参考资料，但您可能想研究 Owicki-Gries 理论（如果您喜欢定理证明）或过程理论/代数（也有各种可用的模型检查工具）。
于 2008-09-17T22:31:49.047 回答
0
@以防万一：我是。但据我所知，为一个非平凡的算法这样做是一个很大的痛苦。我把这种事情留给更聪明的人。我从 KM Chandy, J Misra 的 Parallel Program Design: A Foundation (1988) 中学到了我所知道的
于 2008-09-16T17:38:14.783 回答