C C-atomic-00 (* Allowed, as atomic_inc does not return a value *) { atomic_t x = ATOMIC_INIT(0); atomic_t y = ATOMIC_INIT(0); } P0(atomic_t *x,atomic_t *y) { int r0; atomic_inc(x) ; r0 = atomic_read(y); } P1(atomic_t *x,atomic_t *y) { int r1; atomic_inc(y) ; r1 = atomic_read(x); } P2(atomic_t *x,atomic_t *y) { atomic_add(2,x) ; atomic_add(2,y) ; } Observed y=3; x=3; 1:r1=2; 0:r0=2; and y=3; x=3; 1:r1=1; 0:r0=2; and y=3; x=3; 1:r1=0; 0:r0=2; and y=3; x=3; 1:r1=2; 0:r0=0; and y=3; x=3; 1:r1=0; 0:r0=0;