multithreading - 如何推断互斥量组成的正确性？

Question

我正在尝试使用互斥量实现信号量，以了解有关并发基元和模式以及如何编写正确的并发程序的更多信息。

这是我找到的资源:
http://webhome.csc.uvic.ca/~mcheng/460/notes/gensem.pdf

第9页上的解决方案＃1标记为“不正确”。我实现了here算法。多次运行此程序可能会导致线程冻结。我进行了一些分析，意识到在d互斥锁上可能发生以下操作序列:

            // d was initialized as locked
d.unlock(); // d is unlocked
d.unlock(); // d is still unlocked (unaffected)
d.lock();   // d is locked
d.lock();   // d is still locked (deadlock)

这将导致最后的 d.lock()死锁。

解决方案＃2通过重用互斥体 m确保从信令线程到唤醒线程的过渡来解决此问题。我实现了这个版本 here。

在此解决方案中， d.unlock()之后， m保持锁定，这意味着后续 post()操作将被阻止，直到 m解锁。然后 d.lock()是
在 m.unlock()之后调用，确保 d在之前处于锁定状态
允许随后的 post()操作运行。

尽管我了解此解决方案如何解决该问题，但是我很难在其他潜在问题上争论其正确性。我们是否可以遵循任何一般性规则和指南来确保，辩论甚至证明此类程序的正确性？

我想问这个问题，因为注释中的下2个解决方案。我实现了 solution #3和 solution #4，但是经过多次测试，它们都具有冻结线程。我不确定这是我的实现问题还是解决方案本身不正确。

如果您能分析这些解决方案的正确性，将不胜感激，但我比以往任何时候都更愿意学习一种推理此类算法并验证其正确性的方法。

Answer 1

多次运行您的代码并希望进行一些任意的交织以发现与并发相关的错误不是一个好的方法，但是对于某些初始测试很有用。否则，有更好的方法。

如果您使用的是C或C++，则可以查看GCC和Clang中提供的ThreadSanitizer，它将帮助您在运行时检测死锁和其他与并发相关的错误。

更详尽的方法是系统并发测试，该测试将枚举可能的交错并执行它们。您应该 check out 诸如无状态和有状态模型检查之类的不同技术。

Spin是可用于形式验证的模型检查工具。您可以在Promela中编写模型，并使用LTL进行断言。

最后，这是Wikipedia的list of model checkers，适用于多种语言。