很遗憾,我不知道有任何技术可以“证明”使用锁来控制对共享内存访问的系统。所谓“证明”,是指你无法通过分析证明程序不会死锁、活锁等。
问题在于线程是异步运行的。一旦你开始拥有合理数量的线程和共享资源,可能发生的事件序列(例如锁定/解锁共享资源)的数量就会变得极高,你无法对每一个序列进行建模/分析。
因此,托尼·霍尔(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库将数据的所有者引用移动而不是复制。这应该使其非常高效(虽然我实际上没有尝试过)。
CSP有点难以获得。您可以通过设置消息缓冲区长度将ZeroMQ和DataFlow几乎变成CSP。不幸的是,您无法将缓冲区长度设置为零(这将使其成为CSP)。微软的文档甚至谈到了通过将队列长度设置为1来实现系统稳健性所获得的好处。
您可以通过在链接之间具有同步消息流来在Actor之上合成CSP。这很麻烦,需要实现。
我经常启动自己的通信框架来获得CSP环境。
我认为Java有一些库,但不知道它们的开发活跃程度如何。
然而,如果您已经编写了锁定共享内存的现有代码,则将其适应为CSP环境将是一项艰巨的任务。因此...
Kernel Shark
如果您使用Linux并且您的内核已编译FTRACE,则可以使用Kernel Shark查看系统中发生的情况。类似地,在Solaris上使用DTRACE,在VxWorks上使用WindView,在MCOS上使用TATL。
您需要运行系统直到其停止,然后非常快速地保留FTRACE日志(它将被操作系统在循环缓冲区中覆盖)。然后,您可以图形化地查看发生了什么事情(打开Kernel Shark的进程视图),这可能会提供关于何时发生了什么的线索。
这有助于诊断应用程序的死锁,这可能会使您朝着正确方向前进,但是最终您无法证明它是正确的。这并不妨碍您拥有一个灵光一现的时刻,现在您深知自己已经做对了。
我不知道Windows是否有类似于FTRACE / Kernel shark的等效物。