Merge tag 'block-5.9-2020-08-14' of git://git.kernel.dk/linux-block
[linux/fpc-iii.git] / tools / memory-model / litmus-tests / MP+pooncerelease+poacquireonce.litmus
blobd52c68429722646edf72e8aebf7723cfb6c4323d
1 C MP+pooncerelease+poacquireonce
3 (*
4  * Result: Never
5  *
6  * This litmus test demonstrates that smp_store_release() and
7  * smp_load_acquire() provide sufficient ordering for the message-passing
8  * pattern.
9  *)
13 P0(int *x, int *y)
15         WRITE_ONCE(*x, 1);
16         smp_store_release(y, 1);
19 P1(int *x, int *y)
21         int r0;
22         int r1;
24         r0 = smp_load_acquire(y);
25         r1 = READ_ONCE(*x);
28 exists (1:r0=1 /\ 1:r1=0)