concurrency - 实验弱序并发的工具

Question

有哪些工具可以帮助人们尝试弱序并发？ 也就是说，在自学部分围栏、弱原子、获取/使用/释放语义、无锁算法等方面可以玩什么沙盒？

一个人想要的工具或沙箱将锻炼和强调一个弱有序的线程算法，暴露出算法理论上可能失败的各种方式。例如，在 x86 上物理运行，该工具仍然能够暴露 ARM 类型的故障。

一个开源工具会更好。请指教。

参考：

• C++11 标准草案（PDF，见第 1、29 和 30 条）；
• 汉斯-J。Boehm 的主题概述；
• McKenney、Boehm 和 Crowl 关于这个主题；
• GCC 关于该主题的发展说明；
• Linux 内核关于该主题的注释；
• Stackoverflow 上的相关问题和答案
• 另一个问题，这个比较栅栏和原子的问题；
• Cppmem（根据@KerrekSB 的建议）；
• Cppmem 的帮助页面；
• Spin（根据@JohnZwinck 的建议，用于分析并发系统的逻辑一致性的工具）。

（这些参考文献面向 C++11，因为这正是我接触该主题的方式。但是，据我所知，非 C++ 的答案可能是最好的，因此请随意将您的答案扩展到 C++ 之外，如您所见合身。）

Answer 1

这比您直接提出的问题要笼统得多，但请看一下“Spin”，它是并发系统的“模型检查器”。在线手册在这里：http ://spinroot.com/spin/Man/Manual.html

你可能会觉得它有点“老派”的感觉，但我看不出它为什么不适合你感兴趣的工作。但是，由于它很一般，你可能需要做一些工作来教工具有关问题空间的知识。好消息是它独立于平台。坏消息是您可能需要明确地对每个计算机体系结构进行建模（例如，Spin 本质上并不知道 ARM 与 x86 的保证）。但也许其中一些工作已经在其他地方完成（我没有检查），和/或您可以分享您所做的部分工作，以便其他人可能受益。毕竟，该工具是开源的。

Answer 2

您可能有兴趣查看http://www.cprover.org/wmm/并点击那里的链接，指向有关弱内存的工具和相应论文，特别是 CAV 2013 论文Partial Orders for Efficient BMC of Concurrent Software和 CAV 2014 论文不要坐在栅栏上：自动栅栏插入的静态分析方法可能是很好的起点。您还将在那里找到许多真实世界的示例代码和基准测试。