Proving correctness of multithread algorithms多线程算法特别难以设计/调试/验证。 Dekker的算法是设计正确的同步算法有多困难的主要示例。 Tanenbaum的Modern操作系统在其IPC部分中提供了示例。 有人为此提供很好的参考(书籍，文章)吗？ 谢谢！ 如果不保证担保人就不可能证明任何事情，因此，您要做的第一件事就是熟悉目标平台的内存模型。 Java和x86都有可靠的标准化内存模型-我不太确定CLR，但是如果其他所有方法都失败了，您将建立在目标CPU体系结构的内存模型上。该规则的例外是，如果您打算使用一种根本不允许任何共享的可变状态的语言-我听说Erlang就是这样。 并发的第一个问题是共享可变状态。 可以通过以下方法解决：
并发的第二个问题是安全发布。您如何使数据可用于其他线程？您如何执行移交？您将在内存模型中以及(希望如此)在API中解决此问题。例如，Java有多种发布状态的方法，而java.util.concurrent包包含专门设计用于处理线程间通信的工具。 并发的第三个(也是更困难的)问题是锁定。错误管理的锁顺序是死锁的根源。您可以基于内存模型保证人来分析证明，代码中是否可能出现死锁。但是，您需要牢记这一点来设计和编写代码，否则代码的复杂性将很快使这种分析在实践中无法执行。 然后，一旦或在做之前，证明并发的正确使用，就必须证明单线程的正确性。并发代码库中可能发生的错误集等于单线程程序错误集，再加上所有可能的并发错误。
"并发和分布式编程原理"，M。Ben-Ari Pi微积分，移动过程理论是一个很好的起点。 简短的回答：很难。 从1980年代后期开始，DEC SRC Modula-3和落叶松属植物中确实有一些出色的工作。 例如
Modula-3的一些好主意正使其进入Java世界，例如 我没有任何具体的参考，但是您可能想研究Owicki-Gries理论(如果您喜欢定理证明)或过程理论/代数(也有各种可用的模型检查工具)。
@以防万一：我是。但是据我了解，对于非平凡的算法而言，这样做是一个很大的痛苦。我把这种事情留给聪明的人。我从《并行程序设计：基础》(1988)中学到了什么 |
