Blame view
tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
465 Bytes
1c27b644c Automate memory-b... |
1 |
C WRC+poonceonces+Once |
8f32543b6 EXP litmus_tests:... |
2 3 4 5 6 7 8 |
(* * Result: Sometimes * * This litmus test is an extension of the message-passing pattern, * where the first write is moved to a separate process. Note that this * test has no ordering at all. *) |
1c27b644c Automate memory-b... |
9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 |
{} P0(int *x) { WRITE_ONCE(*x, 1); } P1(int *x, int *y) { int r0; r0 = READ_ONCE(*x); WRITE_ONCE(*y, 1); } P2(int *x, int *y) { int r0; int r1; r0 = READ_ONCE(*y); r1 = READ_ONCE(*x); } exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0) |