有没有人知道任何分析技术可以用来设计/调试线程锁定和解锁序列？实质上，我需要一种像真值表一样的技术来证明我的锁定序列不会出现死锁。
这不是通过试错编程解决的问题。
我特别的问题是读写锁，但我是以一般意义来询问这个问题。如果存在某种有用的技术，我相信学习它将很有帮助。
我尝试了因果图，在其中有盒子和箭头，我可以使用它们来跟踪控制流，并解决了80%的问题。但当一个线程在“指令之间的空隙”中溜进去时，我仍然会在压力测试下偶尔出现死锁，如果这有任何意义的话。
总结一下，我需要以某种方式表示该问题，以便能够正式分析互斥锁的重叠。
很遗憾，我不知道有任何技术可以“证明”使用锁来控制对共享内存访问的系统。所谓“证明”，是指你无法通过分析证明程序不会死锁、活锁等。
问题在于线程是异步运行的。一旦你开始拥有合理数量的线程和共享资源，可能发生的事件序列（例如锁定/解锁共享资源）的数量就会变得极高，你无法对每一个序列进行建模/分析。
因此，托尼·霍尔（Tony Hoare）在1978年开发了通信顺序进程（Communicating Sequential Processes）。它是Actor模型的发展，它本身已经在很大程度上解决了这个问题。
Actor和CSP
简而言之，在Actor模型中，数据不是通过具有锁的共享内存进行通信的。相反，副本通过某种类型的通讯通道（例如套接字或管道）发送到两个线程之间。这意味着你从未锁定内存。实际上，所有内存都是线程私有的，当需要向其他线程发送副本时，会自动发送。它是一个非常“面向对象”的东西；私有数据（线程拥有的内存）、公共接口（在通信通道上发出和接收的消息）。它也非常可扩展——管道可以变成套接字，线程可以变成其他计算机上的进程。
CSP模型也是如此，只不过通信通道不会接受消息，除非接收端准备好读取它。
这个添加非常关键，它意味着可以对系统设计进行代数分析。事实上，托尼·霍尔为CSP制定了一个过程演算。CSP的维基百科页面引用了使用此方法证明电子商务系统设计的案例。
因此，如果正在开发严格的CSP系统，则有可能在分析上证明它不会死锁等问题。
现实经验
我做了很多CSP（或类似CSP）的系统，一直很好。我没有做数学运算，而是根据直觉来帮助我避免问题。实际上，CSP确保如果我构建了一个可能死锁的系统，它将每次都死锁。因此，在开发期间至少可以找到问题，而不是在两年后某个网络链接比正常情况更忙时。
现实选项
对于Actor模型编程，有很多选项。ZeroMQ、nanomsg、Microsoft的.NET Data Flow库等。
它们都非常好，如果小心使用，你可以构建一个相当不错的系统。我非常喜欢ZeroMQ和nanomsg——它们使将一组线程拆分成在不同计算机上运行的单独进程变得非常简单，而且你根本没有改变架构。如果绝对性能并不重要，将这两个与例如Google Protocol Buffers一起使用，可以制作出一个非常整洁的系统，其中包含了将不同的操作系统、语言和系统合并到设计中的大量选项。
我怀疑微软针对.NET的DataFlow库将数据的所有者引用移动而不是复制。这应该使其非常高效（虽然我实际上没有尝试过）。