CBMC工具中__CPROVER_fence函数的可用参数及对应含义是什么？

__CPROVER_fence是CBMC内置的用于显式建模内存序约束的原语，传入的字符串参数对应要生效的屏障重排序禁止规则，所有合法可选参数及含义如下：

• RRfence：读-读屏障，禁止屏障前的读操作和屏障后的读操作发生重排序，仅当该点之前的所有读操作完成后，才会执行后续的读操作
• RWfence：读-写屏障，禁止屏障前的读操作和屏障后的写操作发生重排序，仅当该点之前的所有读操作完成后，才会执行后续的写操作
• WRfence：写-读屏障，禁止屏障前的写操作和屏障后的读操作发生重排序，仅当该点之前的所有写操作完成后，才会执行后续的读操作
• WWfence：写-写屏障，禁止屏障前的写操作和屏障后的写操作发生重排序，仅当该点之前的所有写操作完成后，才会执行后续的写操作
• acquire：Acquire内存语义，等价于同时传入RRfence+RWfence，仅当该点之前的所有读操作完成后，才会执行后续的所有内存操作
• release：Release内存语义，等价于同时传入WRfence+WWfence，仅当该点之前的所有内存操作完成后，才会执行后续的所有写操作
• RCpc：模拟C/C++标准定义的consume内存序约束
• rmb：全读屏障，仅当该点之前的所有读操作完成后，才会执行后续的所有内存操作
• wmb：全写屏障，仅当该点之前的所有内存操作完成后，才会执行后续的所有写操作
• mb：全内存屏障，等价于同时传入四个基础单向屏障参数，禁止所有跨越该点的内存操作重排序

调用时支持同时传入多个参数，你遇到的__CPROVER_fence("RRfence", "RWfence");写法就是同时生效两种屏障规则，和直接传acquire效果完全一致。

内容的提问来源于stack exchange，提问作者artless-noise-bye-due2AI