Blame view
tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
598 Bytes
1c27b644c Automate memory-b... |
1 |
C ISA2+poonceonces |
8f32543b6 EXP litmus_tests:... |
2 3 4 5 6 7 8 9 |
(* * Result: Sometimes * * Given a release-acquire chain ordering the first process's store * against the last process's load, is ordering preserved if all of the * smp_store_release() invocations are replaced by WRITE_ONCE() and all * of the smp_load_acquire() invocations are replaced by READ_ONCE()? *) |
1c27b644c Automate memory-b... |
10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 |
{} P0(int *x, int *y) { WRITE_ONCE(*x, 1); WRITE_ONCE(*y, 1); } P1(int *y, int *z) { int r0; r0 = READ_ONCE(*y); WRITE_ONCE(*z, 1); } P2(int *x, int *z) { int r0; int r1; r0 = READ_ONCE(*z); r1 = READ_ONCE(*x); } exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0) |