关于多线程：证明多线程算法的正确性

多线程算法特别难以设计/调试/验证。 Dekker的算法是设计正确的同步算法有多困难的主要示例。 Tanenbaum的Modern操作系统在其IPC部分中提供了示例。 有人为此提供很好的参考(书籍，文章)吗？ 谢谢！

---

如果不保证担保人就不可能证明任何事情，因此，您要做的第一件事就是熟悉目标平台的内存模型。 Java和x86都有可靠的标准化内存模型-我不太确定CLR，但是如果其他所有方法都失败了，您将建立在目标CPU体系结构的内存模型上。该规则的例外是，如果您打算使用一种根本不允许任何共享的可变状态的语言-我听说Erlang就是这样。

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

可以通过以下方法解决：

• 使状态不变
• 不分享状态
• 用同一把锁保护共享的可变状态(两个不同的锁不能保护同一个状态，除非您始终完全使用这两个锁)

并发的第二个问题是安全发布。您如何使数据可用于其他线程？您如何执行移交？您将在内存模型中以及(希望如此)在API中解决此问题。例如，Java有多种发布状态的方法，而java.util.concurrent包包含专门设计用于处理线程间通信的工具。

并发的第三个(也是更困难的)问题是锁定。错误管理的锁顺序是死锁的根源。您可以基于内存模型保证人来分析证明，代码中是否可能出现死锁。但是，您需要牢记这一点来设计和编写代码，否则代码的复杂性将很快使这种分析在实践中无法执行。

然后，一旦或在做之前，证明并发的正确使用，就必须证明单线程的正确性。并发代码库中可能发生的错误集等于单线程程序错误集，再加上所有可能的并发错误。

---

"并发和分布式编程原理"，M。Ben-Ari
ISBN-13：978-0-321-31283-9
他们在线阅读了野生动物园书籍以供阅读：
http://my.safaribooksonline.com/9780321312839

---

Pi微积分，移动过程理论是一个很好的起点。

---

简短的回答：很难。

从1980年代后期开始，DEC SRC Modula-3和落叶松属植物中确实有一些出色的工作。

例如

• 线程同步：正式规范(1991)
  作者：A D Birrell，J V Guttag，J J Horning，R Levin
  使用Modula-3进行系统编程，第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当前仅限于顺序规范"。

---

我没有任何具体的参考，但是您可能想研究Owicki-Gries理论(如果您喜欢定理证明)或过程理论/代数(也有各种可用的模型检查工具)。

---

@以防万一：我是。但是据我了解，对于非平凡的算法而言，这样做是一个很大的痛苦。我把这种事情留给聪明的人。我从《并行程序设计：基础》(1988)中学到了什么
由K M Chandy，J Misra

---