`__CPROVER_fence()` arguments

Question

I see code like __CPROVER_fence("RRfence", "RWfence"); being using in projects like the Linux RCU testing and pthread wrappers for CBMC analysis. I looked at the online documentation, but found no text on the strings sent to this CBMC function.

What are the available parameters to __CPROVER_fence?

My take is that it is an annotation/function to denote barriers/fences performed by the real implementation. Ie, it is an analysis stub for the real functionality. Obviously the parameters denote types of barriers, but I have not found a reference to the actual parameters and corresponding barrier types. Ie, "RRFence" is a read fence, meaning reads before this point will complete before reads after this point (as a guess).

Answer 1

Use the source Luke.

All notation are 'fences' to say that some CPU barrier primitive has prevented the hazard type from occurring. So, it is all prior "read/write" will be committed to cache before the subsequent "read/write". The 'function' can accept any combination/permutation of these values.

'cumul' versions are documented in section 4.4.2 of Herding cats..., they are 'transitive' fences which show that all threads/cores will see the ordering.

---

Indeed as Hasturkun has pointed out, there are eight annotations accepted by CPROVER_fence(). See wikipedia hazards for details as well as other cited papers.

• RRFence, not a specific hazard but could cause events to cascade
• RWFence, this is an anti-dependency which could be problematic for dependent items.
• WRFence, a specific hazard only involving one variable
• WWFence, an output hazard could result with only one 'variable'.
• WWcumul
• RRcumul
• RWcumul
• WRcumul

The 'cumul' versions are similar to the normal 'fence' with the addition that order is preserved to all cores. For instance, on the ARM CPU, all fences are the 'cumul' type. The straight 'fence' is only for out-of-order issues, such as pipeline and/or write buffers for a single core.

All notation are 'fences' to say that some CPU barrier primitive has prevented the hazard type from occurring. So, it is all prior "read/write" will be committed before the subsequent "read/write". The 'function' can accept any permutation of these values.

Some things like a counter that are not dependent on other consistent values can be fine with only some fences. However, other values/tuples/structs are multi-address (non-atomic to load/store) and could require that multiple value are read/written in a consistent way. A taxonomy of interdependent accesses Table III. Glossary of litmus tests names of Herding cats....

The page, Software Verification for Weak Memory, at CProver is a Rosetta stone for this topic. It refers mainly to the tool 'musketeer', but further reading will show that many concepts are incorporated into the CBMC tool. Even the URL for the page contains 'wmm' which is also in the 'goto-instrument' directory as 'wmm' where this functionality is implemented.

• Paper on weak memory - end of section 1 (pg A:5) details incorporation of these models into CBMC. The models are TSO, PSO, RMO, and Power. These can be found in 'cbmc/src/goto-instrument/wmm/wmm.h'.
• Software Verification for Weak Memory via Program Transformation describes a fix to PostgreSQL and the instrumentation of the Linux RCU code; ergo the cited open source project probably derived from CBMC weak memory implementors, lending to the possibility there is no online documentation.

---

The directory cbmc-concurrency and ansi-c have many examples of use of the CPROVER_fence() and other memory modelling primitives.

Sample C prover code to implement pthread_mutex_lock() for analysis,

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
}

My understanding is that it is checking for,

• only a single lock
• lock is initialized before call
• lock is not destroyed while held
• lock is not re-initialized while held
• all weak ordering memory items are resolved (all caches flushed) after the call.

Interestingly, man pthread_mutex_lock() doesn't say anything about CPU synchronization or fences. We have priority inversion, dead lock, etc with mutex/lock programing, but also it has a price on pipeline performance. Indeed on ARM/Linux/glibc, kuser_cmpxchg32_fixup call smp_dmb arm to fulfill this requirement. A similar regression test shows failures of pthread_create() where a write buffer could leave a value in indeterminate state on the initial thread startup, unless a barrier is inserted as pthread_create() doesn't have this synchronization.

It seems this work is fairly recent (by some standards), with papers dated 2013 and Linux RCU commit in 2016. It is possible the authors wish to keep the API fluid. Probably they are more concentrated on the more enjoyable task of proving the provers and didn't have time to document this interface.

---

• Doug Lea's cook book - helpful for memory ordering types versus concrete CPU types.
• C++ mapping to CPU - CPU instructions used by C++ memory order types.

Note: Earlier versions of the answer assumed that cache synchronization with non-cached bus masters was covered by this API. That is not the case. System programmers trying to use cbmc need to use other mechanics, if this is of concern.