linux/tools/memory-model/litmus-tests/R+fencembonceonces.litmus
<<
>>
Prefs
   1C R+fencembonceonces
   2
   3(*
   4 * Result: Never
   5 *
   6 * This is the fully ordered (via smp_mb()) version of one of the classic
   7 * counterintuitive litmus tests that illustrates the effects of store
   8 * propagation delays.  Note that weakening either of the barriers would
   9 * cause the resulting test to be allowed.
  10 *)
  11
  12{}
  13
  14P0(int *x, int *y)
  15{
  16        WRITE_ONCE(*x, 1);
  17        smp_mb();
  18        WRITE_ONCE(*y, 1);
  19}
  20
  21P1(int *x, int *y)
  22{
  23        int r0;
  24
  25        WRITE_ONCE(*y, 2);
  26        smp_mb();
  27        r0 = READ_ONCE(*x);
  28}
  29
  30exists (y=2 /\ 1:r0=0)
  31