1C dep+plain 2 3(* 4 * Result: Never 5 * 6 * This litmus test demonstrates that in LKMM, plain accesses 7 * carry dependencies much like accesses to registers: 8 * The data stored to *z1 and *z2 by P0() originates from P0()'s 9 * READ_ONCE(), and therefore using that data to compute the 10 * conditional of P0()'s if-statement creates a control dependency 11 * 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