32 lines · plain
1C dep+plain2 3(*4 * Result: Never5 *6 * This litmus test demonstrates that in LKMM, plain accesses7 * carry dependencies much like accesses to registers:8 * The data stored to *z1 and *z2 by P0() originates from P0()'s9 * READ_ONCE(), and therefore using that data to compute the10 * conditional of P0()'s if-statement creates a control dependency11 * from that READ_ONCE() to P0()'s WRITE_ONCE().12 *)13 14{}15 16P0(int *x, int *y, int *z1, int *z2)17{18 int a = READ_ONCE(*x);19 *z1 = a;20 *z2 = *z1;21 if (*z2 == 1)22 WRITE_ONCE(*y, 1);23}24 25P1(int *x, int *y)26{27 int r = smp_load_acquire(y);28 smp_store_release(x, r);29}30 31exists (x=1 /\ y=1)32