使用来源卢克。
所有符号都是“栅栏”，表示某些 CPU 屏障原语已阻止危险类型的发生。因此，所有先前的“读/写”都将在后续“读/写”之前提交到缓存。 “函数”可以接受这些值的任意组合/排列。
'cumul'版本记录在第 4.4.2 节中放牧猫... http://www0.cs.ucl.ac.uk/staff/j.alglave/papers/toplas14.pdf，它们是“传递”栅栏，表明所有线程/核心都会看到顺序。
确实如哈斯图尔昆 https://stackoverflow.com/users/20270/hasturkun已经指出，有八个注释被接受CPROVER_fence(). See 维基百科危险 https://en.wikipedia.org/wiki/Hazard_(computer_architecture)了解详细信息以及其他引用的论文。
- RRFence，不是特定危险，但可能导致事件级联
- RWFence，这是一种反依赖关系，对于依赖项可能会出现问题。
- WRFence，仅涉及一个变量的特定危险
- WWFence 指出，仅一个“变量”就可能导致输出危险。
- WWcumul
- RRcumul
- RWcumul
- WRcumul
“cumul”版本与普通的“fence”类似，但所有核心的顺序都保留。例如，在 ARM CPU 上，所有栅栏都是“cumul”类型。直“栅栏”仅适用于无序问题，例如单个核心的管道和/或写入缓冲区。
所有符号都是“栅栏”，表示某些 CPU 屏障原语已阻止危险类型的发生。因此，所有先前的“读/写”都将在后续的“读/写”之前提交。 “函数”可以接受这些值的任何排列。
有些东西（例如不依赖于其他一致值的计数器）只需使用一些栅栏就可以了。然而，其他值/元组/结构是多地址的（非原子加载/存储），并且可能需要以一致的方式读取/写入多个值。相互依赖访问的分类表三。石蕊测试名称词汇表 of 放牧猫... http://www0.cs.ucl.ac.uk/staff/j.alglave/papers/toplas14.pdf.
这一页，弱内存的软件验证 http://www.cprover.org/wmm/，CProver 是针对该主题的罗塞塔石碑。它主要指“火枪手”工具，但进一步阅读会发现 CBMC 工具中融入了许多概念。甚至页面的 URL 也包含“wmm”，它也在“goto-instrument”目录中作为“wmm”实现了此功能。
-
关于弱记忆力的论文 http://www0.cs.ucl.ac.uk/staff/j.alglave/papers/toplas14.pdf- 第 1 节末尾（第 A:5 页）详细说明了将这些模型纳入 CBMC。这些模型包括 TSO、PSO、RMO 和 Power。这些可以在“cbmc/src/goto-instrument/wmm/wmm.h”中找到。
-
通过程序转换对弱内存进行软件验证 http://www.cprover.org/etaps/esop.pdf描述了对 PostgreSQL 的修复以及 Linux RCU 代码的检测；因此，所引用的开源项目可能源自 CBMC 弱内存实现者，因此可能没有在线文档。
目录CBMC并发 https://github.com/diffblue/cbmc/tree/develop/regression/cbmc-concurrency and ansi-c https://github.com/diffblue/cbmc/blob/develop/src/ansi-c有很多使用的例子CPROVER_fence()和其他内存建模原语。
要实现的示例 C 验证器代码pthread_mutex_lock() https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/library/pthread_lib.c#L110进行分析，
inline int pthread_mutex_lock(pthread_mutex_t *mutex)
{
__CPROVER_HIDE:;
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
__CPROVER_assert(__CPROVER_get_must(mutex, "mutex-init"),
"mutex must be initialized");
__CPROVER_assert(!__CPROVER_get_may(mutex, "mutex-destroyed"),
"mutex must not be destroyed");
__CPROVER_assert(__CPROVER_get_must(mutex, "mutex-recursive") ||
!__CPROVER_get_may(mutex, "mutex-locked"),
"attempt to lock non-recurisive locked mutex");
__CPROVER_set_must(mutex, "mutex-locked");
__CPROVER_set_may(mutex, "mutex-locked");
__CPROVER_assert(*((__CPROVER_mutex_t *)mutex)!=-1,
"mutex not initialised or destroyed");
#else
__CPROVER_atomic_begin();
__CPROVER_assume(!*((__CPROVER_mutex_t *)mutex));
*((__CPROVER_mutex_t *)mutex)=1;
__CPROVER_atomic_end();
__CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence",
"WWcumul", "RRcumul", "RWcumul", "WRcumul");
#endif
return 0; // we never fail
}
我的理解是它正在检查，
- 只有一把锁
- 锁在调用之前初始化
- 锁在持有时不会被破坏
- 持有锁时不会重新初始化
- 调用后，所有弱排序内存项都会被解析（所有缓存都被刷新）。
有趣的是，man pthread_mutex_lock()没有提及任何有关 CPU 同步或栅栏的信息。我们通过互斥/锁编程实现了优先级反转、死锁等，但它也会以管道性能为代价。确实在 ARM/Linux/glibc 上，kuser_cmpxchg32_fixup https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/tree/arch/arm/kernel/entry-armv.S?h=v5.16-rc4#n929 call smp_dmb arm来满足这个要求。类似的回归测试显示失败pthread_create()其中写入缓冲区可能会在初始线程启动时将值保留为不确定状态，除非插入屏障作为pthread_create()没有这个同步功能。
看来这项工作是最近才完成的（按照某些标准），论文日期为 2013 年，Linux RCU 提交日期为 2016 年。作者可能希望保持 API 的流畅性。可能他们更专注于证明证明者这一更有趣的任务，而没有时间记录这个接口。
-
道格·李的烹饪书 http://gee.cs.oswego.edu/dl/jmm/cookbook.html- 有助于内存排序类型与具体 CPU 类型的比较。
-
C++ 映射到 CPU https://www.cl.cam.ac.uk/%7Epes20/cpp/cpp0xmappings.html- C++ 内存顺序类型使用的 CPU 指令。
Note:答案的早期版本假设此 API 涵盖了与非缓存总线主控的缓存同步。事实并非如此。系统程序员尝试使用cbmc如果担心的话，需要使用其他机制。
