linux/tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus
<<
>>
Prefs
   1C S+fencewmbonceonce+poacquireonce
   2
   3(*
   4 * Result: Never
   5 *
   6 * Can a smp_wmb(), instead of a release, and an acquire order a prior
   7 * store against a subsequent store?
   8 *)
   9
  10{}
  11
  12P0(int *x, int *y)
  13{
  14        WRITE_ONCE(*x, 2);
  15        smp_wmb();
  16        WRITE_ONCE(*y, 1);
  17}
  18
  19P1(int *x, int *y)
  20{
  21        int r0;
  22
  23        r0 = smp_load_acquire(y);
  24        WRITE_ONCE(*x, 1);
  25}
  26
  27exists (x=2 /\ 1:r0=1)
  28