时间戳

首页 > 解决方案 > 如何推理互斥体组合的正确性？

multithreading - 如何推理互斥体组合的正确性？

问题描述

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

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

解决方案 #1 在第 9 页被标记为“不正确”。我在这里实现了算法。多次运行此程序可能会导致线程冻结。我做了一些分析并意识到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 通过重用 mutex 来保护从信号线程到唤醒线程的转换，从而解决了这个问题m。我在这里实现了这个版本。

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

尽管我了解此解决方案如何解决该问题，但我很难就其他潜在问题证明其正确性。有没有我们可以遵循的一般规则和指导方针来确保、争论甚至证明这样的程序的正确性？

我想问这个问题是因为注释中的下两个解决方案。我实现了解决方案 #3和解决方案 #4，但是在多次测试时，两者都有冻结的线程。我不确定这是我的实施问题还是解决方案本身不正确。

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

标签： multithreadingconcurrencymutexsemaphorecorrectness

解决方案

多次运行您的代码并希望通过一些任意交错来发现与并发相关的错误并不是一种很好的处理方式，但它对于一些初始测试很有用。否则，有更好的方法。

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

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

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

最后，这里是维基百科的各种语言模型检查器列表。

推荐阅读