Wed Dec 30 09:55:49 GMT 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw000
"DpdR SyncsRW Rfe SyncsRW Rfe DpdR SyncsRW Rfe SyncsRW Rfe"
{0:r2=x; 1:r2=x; 1:r5=y; 2:r2=y; 3:r2=y; 3:r5=x;}
P0 | P1 | P2 | P3 ;
lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
sync | xor r3,r1,r1 | sync | xor r3,r1,r1 ;
li r3,2 | lwzx r4,r3,r5 | li r3,2 | lwzx r4,r3,r5 ;
stw r3,0(r2) | sync | stw r3,0(r2) | sync ;
| li r6,1 | | li r6,1 ;
| stw r6,0(r5) | | stw r6,0(r5) ;
exists (x=2 /\ y=2 /\ 0:r1=1 /\ 1:r1=2 /\ 1:r4=0 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r4=0)
Generated assembler
_litmus_P3_0_: lwz 28,0(11)
_litmus_P3_1_: xor 10,28,28
_litmus_P3_2_: lwzx 30,10,9
_litmus_P3_3_: sync
_litmus_P3_4_: li 8,1
_litmus_P3_5_: stw 8,0(9)
_litmus_P2_0_: lwz 5,0(9)
_litmus_P2_1_: sync
_litmus_P2_2_: li 11,2
_litmus_P2_3_: stw 11,0(9)
_litmus_P1_0_: lwz 28,0(11)
_litmus_P1_1_: xor 10,28,28
_litmus_P1_2_: lwzx 30,10,9
_litmus_P1_3_: sync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: lwz 5,0(9)
_litmus_P0_1_: sync
_litmus_P0_2_: li 11,2
_litmus_P0_3_: stw 11,0(9)
Test bcssrw000 Allowed
Histogram (100 states)
2 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=1; y=2;
1 :>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
1 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
1 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=2;
3 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
326086:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=2; x=1; y=2;
168629:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
350861:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
626369:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
375146:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
1385315:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
307912:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
393802:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=2;
778275:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
239767:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=2;
402052:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
655633:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=1;
235323:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=1; y=2;
1532575:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=2; y=2;
277467:>0:r1=1; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
489361:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
271535:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=2;
477234:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
585917:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
1012474:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
436800:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
4035663:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
867569:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=2;
252448:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
223671:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
178137:>0:r1=1; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
5007794:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=2;
2026282:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=1;
1229331:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=2;
339949:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
558635:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=2;
4325965:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=2; x=1; y=2;
2026052:>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
6845955:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
6807081:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
2200840:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
3928004:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
752351:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
3043229:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=2; x=1; y=2;
255476:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
2459300:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=2; y=2;
407413:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=2; x=1; y=2;
7254999:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=1; y=2;
3103972:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=2;
468847:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=2;
4007103:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=1; y=2;
645955:>0:r1=1; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
6577979:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
351950:>0:r1=1; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
219637:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=1; y=2;
1108104:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
6392442:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
204401:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
2423965:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
404733:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
4136781:>0:r1=1; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
518256:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=2;
15956700:>0:r1=1; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
14304293:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=2; x=1; y=2;
13239653:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
3059676:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
13490354:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
7396481:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
3978366:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=2;
221158:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=2;
5057056:>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
700122:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=2; x=1; y=2;
7166209:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
7862897:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
3355410:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
304433:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=2;
3680046:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
2674469:>0:r1=1; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
294116:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=2;
470940:>0:r1=1; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
2268751:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
6180712:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
9053413:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
2102155:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
4618935:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
143183:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=0; x=2; y=2;
6549038:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
3219184:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
1033938:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=0; x=1; y=2;
1809060:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=2;
1294339:>0:r1=1; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
6665575:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
8739709:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=2;
3142346:>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
18634576:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
10385662:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=2; x=1; y=2;
14573415:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
7469082:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
389672:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=0; x=2; y=2;
11596066:>0:r1=1; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 0:r1=1 /\ 1:r1=2 /\ 1:r4=0 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r4=0) is NOT validated
Hash=b7e6e6df4355fb418bf475952119efba
Cycle=DpdR SyncsRW Rfe SyncsRW Rfe DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw000 No BCSyncsRW
Safe=DpdR
Time bcssrw000 113.14
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw001
"DpdR SyncsRW Rfe DpdR SyncsRW Rfe SyncsRW Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 2:r2=y; 2:r5=x;}
P0 | P1 | P2 ;
lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | sync | xor r3,r1,r1 ;
lwzx r4,r3,r5 | li r3,2 | lwzx r4,r3,r5 ;
sync | stw r3,0(r2) | sync ;
li r6,1 | | li r6,1 ;
stw r6,0(r5) | | stw r6,0(r5) ;
exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r4=0)
Generated assembler
_litmus_P2_0_: lwz 27,0(11)
_litmus_P2_1_: xor 10,27,27
_litmus_P2_2_: lwzx 28,10,9
_litmus_P2_3_: sync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 27,0(11)
_litmus_P0_1_: xor 10,27,27
_litmus_P0_2_: lwzx 28,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw001 Allowed
Histogram (18 states)
4 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
13166891:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
4006512:>0:r1=1; 0:r4=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
9927730:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
7206989:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
3488654:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r4=0; y=2;
9616542:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
18513467:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
22477064:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
19392734:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=2; 2:r4=0; y=2;
4477473:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
36702803:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r4=0; y=2;
35407740:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
13783010:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
36222910:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
55231087:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
43181637:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
67196753:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r4=0) is NOT validated
Hash=0b5e63c8ef234eb2e941f5c51f0aef20
Cycle=DpdR SyncsRW Rfe DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw001 No BCSyncsRW
Safe=DpdR
Time bcssrw001 65.05
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw002
"SyncsRR DpdR SyncsRW Rfe DpdR SyncsRW Rfe SyncsRW Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 2:r2=y; 2:r6=x;}
P0 | P1 | P2 ;
lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | sync | sync ;
lwzx r4,r3,r5 | li r3,2 | lwz r3,0(r2) ;
sync | stw r3,0(r2) | xor r4,r3,r3 ;
li r6,1 | | lwzx r5,r4,r6 ;
stw r6,0(r5) | | sync ;
| | li r7,1 ;
| | stw r7,0(r6) ;
exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=2 /\ 2:r5=0)
Generated assembler
_litmus_P2_0_: lwz 25,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 26,0(11)
_litmus_P2_3_: xor 8,26,26
_litmus_P2_4_: lwzx 10,8,9
_litmus_P2_5_: sync
_litmus_P2_6_: li 7,1
_litmus_P2_7_: stw 7,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 27,0(11)
_litmus_P0_1_: xor 10,27,27
_litmus_P0_2_: lwzx 28,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw002 Allowed
Histogram (33 states)
1 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
1 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
1 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
536253:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
588219:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
2755479:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
5858762:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
2457579:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
9388245:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
1893798:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
31328751:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
10901142:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
16325151:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
44737601:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
3506884:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
16032587:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
4942055:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
2087381:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
2270792:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
14886172:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
1150104:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
3437827:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
2903348:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
1853657:>0:r1=1; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
14294572:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
31943657:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
3406157:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
29610273:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
54153826:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
15379686:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
3067845:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
37457061:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
30845133:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=2 /\ 2:r5=0) is NOT validated
Hash=11796ca5759756e415169a54d5d677e2
Cycle=SyncsRR DpdR SyncsRW Rfe DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw002 No BCSyncsRW
Safe=SyncsRR DpdR
Time bcssrw002 71.79
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw003
"LwSyncsRR DpdR SyncsRW Rfe DpdR SyncsRW Rfe SyncsRW Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 2:r2=y; 2:r6=x;}
P0 | P1 | P2 ;
lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | sync | lwsync ;
lwzx r4,r3,r5 | li r3,2 | lwz r3,0(r2) ;
sync | stw r3,0(r2) | xor r4,r3,r3 ;
li r6,1 | | lwzx r5,r4,r6 ;
stw r6,0(r5) | | sync ;
| | li r7,1 ;
| | stw r7,0(r6) ;
exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=2 /\ 2:r5=0)
Generated assembler
_litmus_P2_0_: lwz 25,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 26,0(11)
_litmus_P2_3_: xor 8,26,26
_litmus_P2_4_: lwzx 10,8,9
_litmus_P2_5_: sync
_litmus_P2_6_: li 7,1
_litmus_P2_7_: stw 7,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 27,0(11)
_litmus_P0_1_: xor 10,27,27
_litmus_P0_2_: lwzx 28,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw003 Allowed
Histogram (33 states)
1 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
3 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
1 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
25414 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
57671 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
270463:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
824435:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
574507:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
1228389:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
722703:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
1134217:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
136092:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
1994865:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
1179936:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
4895488:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
3701687:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
3767748:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
56581258:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
34573336:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
2338232:>0:r1=1; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
41526232:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
3379189:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
29205972:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
7164191:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
13382883:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
4480540:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
32387693:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
58119336:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
40189498:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
18810186:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
11786167:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
15724431:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
9837236:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=2 /\ 2:r5=0) is NOT validated
Hash=f0d60999a697d3eb825e725dab825965
Cycle=LwSyncsRR DpdR SyncsRW Rfe DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw003 No BCSyncsRW
Safe=LwSyncsRR DpdR
Time bcssrw003 75.48
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw004
"DpdW Wse SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r5=x;}
P0 | P1 | P2 ;
li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | xor r3,r1,r1 ;
sync | li r3,2 | li r4,1 ;
lwz r3,0(r2) | stw r3,0(r2) | stwx r4,r3,r5 ;
xor r4,r3,r3 | | ;
lwzx r5,r4,r6 | | ;
sync | | ;
li r7,1 | | ;
stw r7,0(r6) | | ;
exists (x=2 /\ y=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2)
Generated assembler
_litmus_P2_0_: lwz 28,0(11)
_litmus_P2_1_: xor 30,28,28
_litmus_P2_2_: li 10,1
_litmus_P2_3_: stwx 10,30,9
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 26,0(11)
_litmus_P0_4_: xor 8,26,26
_litmus_P0_5_: lwzx 27,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw004 Allowed
Histogram (24 states)
5 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=2; y=2;
13 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=2; y=1;
1821577:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
1129438:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
713982:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
25883618:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=1; x=1; y=1;
15511422:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
1707948:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
13145568:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
29130908:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=1; x=1; y=2;
53928968:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
3336976:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
9440609:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=2; x=1; y=2;
783224:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
4356122:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=2; y=2;
6227891:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=2;
24090791:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
31150707:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=1;
9056783:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=1;
29567526:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=2; y=1;
5152346:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
100294693:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=2; y=1;
12942629:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=2;
20626256:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2) is NOT validated
Hash=2b45cfbf06c32c061b1ef2291b80e3a8
Cycle=DpdW Wse SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw004 No BCSyncsRW
Safe=Wse SyncsWR DpdW DpdR
Time bcssrw004 71.91
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw005
"SyncdRW Wse SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | sync ;
sync | li r3,2 | li r3,1 ;
lwz r3,0(r2) | stw r3,0(r2) | stw r3,0(r4) ;
xor r4,r3,r3 | | ;
lwzx r5,r4,r6 | | ;
sync | | ;
li r7,1 | | ;
stw r7,0(r6) | | ;
exists (x=2 /\ y=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: li 30,1
_litmus_P2_3_: stw 30,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 26,0(11)
_litmus_P0_4_: xor 8,26,26
_litmus_P0_5_: lwzx 27,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw005 Allowed
Histogram (23 states)
1 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=2; y=1;
1532976:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
1395638:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
640164:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
16181849:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
4397157:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=2; y=2;
7147011:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
14820908:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
4651904:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=2;
962533:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
3136498:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
2067225:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
23049025:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=1;
26984488:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
21742970:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=2; y=1;
11768551:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=2;
25298185:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=1; x=1; y=2;
11922672:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=2; x=1; y=2;
58772929:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
33394847:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
99899344:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=2; y=1;
23986777:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=1; x=1; y=1;
6246348:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2) is NOT validated
Hash=921da9ec68c9cae42224f4aee8da9e15
Cycle=SyncdRW Wse SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw005 No BCSyncsRW
Safe=Wse SyncsWR SyncdRW DpdR
Time bcssrw005 68.40
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw006
"LwSyncdRW Wse SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | lwsync ;
sync | li r3,2 | li r3,1 ;
lwz r3,0(r2) | stw r3,0(r2) | stw r3,0(r4) ;
xor r4,r3,r3 | | ;
lwzx r5,r4,r6 | | ;
sync | | ;
li r7,1 | | ;
stw r7,0(r6) | | ;
exists (x=2 /\ y=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: li 30,1
_litmus_P2_3_: stw 30,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 26,0(11)
_litmus_P0_4_: xor 8,26,26
_litmus_P0_5_: lwzx 27,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw006 Allowed
Histogram (23 states)
1 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=2; y=1;
1673344:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
710529:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
663866:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
3362852:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
1148130:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
25422446:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=1; x=1; y=1;
1689424:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
4878965:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
6253988:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=1;
12438865:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
23833693:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
24217313:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=1; x=1; y=2;
26602609:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=1;
4878041:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=2;
103493274:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=2; y=1;
17181605:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
23124405:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=2; y=1;
14799477:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=2;
13352551:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=2; x=1; y=2;
54198997:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
4235377:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=2; y=2;
31840248:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2) is NOT validated
Hash=ec356be30e18f54ebeedc96f10f9b03d
Cycle=LwSyncdRW Wse SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw006 No BCSyncsRW
Safe=Wse SyncsWR LwSyncdRW DpdR
Time bcssrw006 69.62
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw007
"DpdR Fre SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r5=x;}
P0 | P1 | P2 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | xor r3,r1,r1 ;
sync | li r3,2 | lwzx r4,r3,r5 ;
lwz r3,0(r2) | stw r3,0(r2) | ;
xor r4,r3,r3 | | ;
lwzx r5,r4,r6 | | ;
sync | | ;
li r7,1 | | ;
stw r7,0(r6) | | ;
exists (y=2 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r4=0)
Generated assembler
_litmus_P2_0_: lwz 28,0(11)
_litmus_P2_1_: xor 10,28,28
_litmus_P2_2_: lwzx 30,10,9
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 26,0(11)
_litmus_P0_4_: xor 8,26,26
_litmus_P0_5_: lwzx 27,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw007 Allowed
Histogram (19 states)
14 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
10 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
6642840:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=1; y=1;
22405317:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=1; y=2;
25313200:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=1; 2:r4=1; y=2;
10931036:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=1; y=1;
6440765:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=1; y=2;
33859420:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
15898969:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=1; y=1;
4388782:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
20186781:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=1; y=2;
33107586:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
3764150:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=1; y=1;
100873423:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
17502308:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=1; y=2;
49032046:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=1; y=1;
13703098:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
9679141:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=2; 2:r4=1; y=2;
26271114:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=1; 2:r4=1; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r4=0) is NOT validated
Hash=befe5b0646d37c624367af2f5d68102e
Cycle=DpdR Fre SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw007 No BCSyncsRW
Safe=Fre SyncsWR DpdR
Time bcssrw007 69.50
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw008.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw008
"SyncdRR Fre SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | sync ;
sync | li r3,2 | lwz r3,0(r4) ;
lwz r3,0(r2) | stw r3,0(r2) | ;
xor r4,r3,r3 | | ;
lwzx r5,r4,r6 | | ;
sync | | ;
li r7,1 | | ;
stw r7,0(r6) | | ;
exists (y=2 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 28,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 30,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 26,0(11)
_litmus_P0_4_: xor 8,26,26
_litmus_P0_5_: lwzx 27,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw008 Allowed
Histogram (18 states)
2 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
18908341:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=1; 2:r3=1; y=2;
24988114:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=2;
16280182:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
6063920:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
28098000:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=1; y=2;
4950910:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
7350637:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=2; 2:r3=1; y=2;
51276659:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
5376778:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=2;
26303398:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
4264248:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=0; y=2;
32292486:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
21564148:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=2;
104984229:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
13570523:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=2;
9318159:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
24409266:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=a20320b515d5d6be92359c592ff3a749
Cycle=SyncdRR Fre SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw008 No BCSyncsRW
Safe=Fre SyncsWR SyncdRR DpdR
Time bcssrw008 67.15
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw009.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw009
"LwSyncdRR Fre SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | lwsync ;
sync | li r3,2 | lwz r3,0(r4) ;
lwz r3,0(r2) | stw r3,0(r2) | ;
xor r4,r3,r3 | | ;
lwzx r5,r4,r6 | | ;
sync | | ;
li r7,1 | | ;
stw r7,0(r6) | | ;
exists (y=2 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 28,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 30,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 26,0(11)
_litmus_P0_4_: xor 8,26,26
_litmus_P0_5_: lwzx 27,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw009 Allowed
Histogram (19 states)
15 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=0; y=2;
11 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
4128410:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=0; y=2;
23833783:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
27479367:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=1; y=2;
5049015:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
19259847:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=1; 2:r3=1; y=2;
7862396:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=2; 2:r3=1; y=2;
9255462:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
5109561:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
5877301:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=2;
50939922:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
16008784:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
13481190:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=2;
21389541:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=2;
27347395:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
32327093:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
23730877:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=2;
106920030:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=b007f90666b53b8e1b409ebed80da9b2
Cycle=LwSyncdRR Fre SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw009 No BCSyncsRW
Safe=Fre SyncsWR LwSyncdRR DpdR
Time bcssrw009 66.94
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw010
"DpdR SyncsRW Rfe SyncsRR DpdR SyncsRW Rfe SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r5=x;}
P0 | P1 | P2 ;
lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
sync | sync | xor r3,r1,r1 ;
lwz r3,0(r2) | li r3,2 | lwzx r4,r3,r5 ;
xor r4,r3,r3 | stw r3,0(r2) | sync ;
lwzx r5,r4,r6 | | li r6,1 ;
sync | | stw r6,0(r5) ;
li r7,1 | | ;
stw r7,0(r6) | | ;
exists (y=2 /\ 0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r4=0)
Generated assembler
_litmus_P2_0_: lwz 27,0(11)
_litmus_P2_1_: xor 10,27,27
_litmus_P2_2_: lwzx 28,10,9
_litmus_P2_3_: sync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 25,0(11)
_litmus_P0_1_: sync
_litmus_P0_2_: lwz 26,0(11)
_litmus_P0_3_: xor 8,26,26
_litmus_P0_4_: lwzx 10,8,9
_litmus_P0_5_: sync
_litmus_P0_6_: li 7,1
_litmus_P0_7_: stw 7,0(9)
Test bcssrw010 Allowed
Histogram (22 states)
4139109:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
7054197:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
6468772:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
4349448:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
4054697:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
21714523:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
9049117:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
3996439:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=2;
38661690:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
39139949:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
57047822:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
1389584:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
39480651:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
6230583:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
12238447:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=2; 2:r4=0; y=2;
14122627:>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
17177320:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
5130823:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
15250984:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
2092060:>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
66081933:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
25129225:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=1; 2:r4=0; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r4=0) is NOT validated
Hash=2770695d9c722f87a04175621ac51ca6
Cycle=DpdR SyncsRW Rfe SyncsRR DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw010 No BCSyncsRW
Safe=SyncsRR DpdR
Time bcssrw010 67.05
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw011.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw011
"DpdR SyncsRW Rfe LwSyncsRR DpdR SyncsRW Rfe SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r5=x;}
P0 | P1 | P2 ;
lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
lwsync | sync | xor r3,r1,r1 ;
lwz r3,0(r2) | li r3,2 | lwzx r4,r3,r5 ;
xor r4,r3,r3 | stw r3,0(r2) | sync ;
lwzx r5,r4,r6 | | li r6,1 ;
sync | | stw r6,0(r5) ;
li r7,1 | | ;
stw r7,0(r6) | | ;
exists (y=2 /\ 0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r4=0)
Generated assembler
_litmus_P2_0_: lwz 27,0(11)
_litmus_P2_1_: xor 10,27,27
_litmus_P2_2_: lwzx 28,10,9
_litmus_P2_3_: sync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 25,0(11)
_litmus_P0_1_: lwsync
_litmus_P0_2_: lwz 26,0(11)
_litmus_P0_3_: xor 8,26,26
_litmus_P0_4_: lwzx 10,8,9
_litmus_P0_5_: sync
_litmus_P0_6_: li 7,1
_litmus_P0_7_: stw 7,0(9)
Test bcssrw011 Allowed
Histogram (23 states)
2 :>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
717819:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
4012815:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=2;
4705967:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
7552765:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
1239582:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
1371593:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
19357315:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
5776350:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
836901:>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
6815817:>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
1998915:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
41532978:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
40185332:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
24315818:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
9540013:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
16966536:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=2; 2:r4=0; y=2;
42508571:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
30460205:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=1; 2:r4=0; y=2;
57981079:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
64311180:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
13509565:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
4302882:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r4=0) is NOT validated
Hash=ae75e3d1140839ad4046415fb4f32715
Cycle=DpdR SyncsRW Rfe LwSyncsRR DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw011 No BCSyncsRW
Safe=LwSyncsRR DpdR
Time bcssrw011 68.06
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw012.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw012
"DpdR SyncsRW Rfe DpdR SyncsRW Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | xor r3,r1,r1 ;
lwzx r4,r3,r5 | lwzx r4,r3,r5 ;
sync | sync ;
li r6,1 | li r6,1 ;
stw r6,0(r5) | stw r6,0(r5) ;
exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r4=0)
Generated assembler
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 10,30,30
_litmus_P1_2_: lwzx 31,10,9
_litmus_P1_3_: sync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: lwz 30,0(11)
_litmus_P0_1_: xor 10,30,30
_litmus_P0_2_: lwzx 31,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw012 Allowed
Histogram (3 states)
193464956:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0;
273774955:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0;
172760089:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r4=0) is NOT validated
Hash=e494be0d2836eabb8ed392ae5713400a
Cycle=DpdR SyncsRW Rfe DpdR SyncsRW Rfe
Relax bcssrw012 No BCSyncsRW
Safe=DpdR
Time bcssrw012 78.13
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw013.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw013
"DpdR SyncsRW Rfe DpdR SyncsRW Rfe DpdR SyncsRW Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r5=x;}
P0 | P1 | P2 ;
lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | xor r3,r1,r1 | xor r3,r1,r1 ;
lwzx r4,r3,r5 | lwzx r4,r3,r5 | lwzx r4,r3,r5 ;
sync | sync | sync ;
li r6,1 | li r6,1 | li r6,1 ;
stw r6,0(r5) | stw r6,0(r5) | stw r6,0(r5) ;
exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r4=0 /\ 2:r1=1 /\ 2:r4=0)
Generated assembler
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: xor 10,30,30
_litmus_P2_2_: lwzx 31,10,9
_litmus_P2_3_: sync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 10,30,30
_litmus_P1_2_: lwzx 31,10,9
_litmus_P1_3_: sync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: lwz 30,0(11)
_litmus_P0_1_: xor 10,30,30
_litmus_P0_2_: lwzx 31,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw013 Allowed
Histogram (7 states)
3289704:>0:r1=1; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0;
3475126:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=1; 2:r4=0;
4910168:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=0;
107421149:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0;
96505297:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0;
99186122:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=0;
85212434:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r4=0 /\ 2:r1=1 /\ 2:r4=0) is NOT validated
Hash=873592e9aeb4eb41aabdf201c7c3fd2d
Cycle=DpdR SyncsRW Rfe DpdR SyncsRW Rfe DpdR SyncsRW Rfe
Relax bcssrw013 No BCSyncsRW
Safe=DpdR
Time bcssrw013 81.96
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw014.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw014
"DpsR SyncsRW Rfe DpdR SyncsRW Rfe DpdR SyncsRW Rfe"
{0:r2=y; 0:r5=x; 1:r2=x; 1:r5=y; 2:r2=y;}
P0 | P1 | P2 ;
lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | xor r3,r1,r1 | xor r3,r1,r1 ;
lwzx r4,r3,r5 | lwzx r4,r3,r5 | lwzx r4,r3,r2 ;
sync | sync | sync ;
li r6,1 | li r6,1 | li r5,2 ;
stw r6,0(r5) | stw r6,0(r5) | stw r5,0(r2) ;
exists (y=2 /\ 0:r1=2 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r4=0 /\ 2:r1=1 /\ 2:r4=1)
Generated assembler
_litmus_P2_0_: lwz 30,0(9)
_litmus_P2_1_: xor 10,30,30
_litmus_P2_2_: lwzx 11,10,9
_litmus_P2_3_: sync
_litmus_P2_4_: li 8,2
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 27,0(11)
_litmus_P1_1_: xor 10,27,27
_litmus_P1_2_: lwzx 28,10,9
_litmus_P1_3_: sync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: lwz 27,0(11)
_litmus_P0_1_: xor 10,27,27
_litmus_P0_2_: lwzx 28,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw014 Allowed
Histogram (22 states)
1 :>0:r1=2; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
122305:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
298575:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
1302660:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
536533:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
3844318:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
37393137:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
14198352:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
23185097:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
3284031:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
37118928:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
8003417:>0:r1=2; 0:r4=0; 1:r1=1; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
34801373:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
9927815:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
13045513:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
57300208:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
68239017:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
39449120:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
4833641:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
19004563:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
15111053:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
9000343:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r1=2 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r4=0 /\ 2:r1=1 /\ 2:r4=1) is NOT validated
Hash=7bfa463f7adb7b5e7778fa7badd28f31
Cycle=DpsR SyncsRW Rfe DpdR SyncsRW Rfe DpdR SyncsRW Rfe
Relax bcssrw014 No BCSyncsRW
Safe=DpsR DpdR
Time bcssrw014 67.09
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw015.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw015
"SyncsRR DpdR SyncsRW Rfe DpdR SyncsRW Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | sync ;
lwzx r4,r3,r5 | lwz r3,0(r2) ;
sync | xor r4,r3,r3 ;
li r6,1 | lwzx r5,r4,r6 ;
stw r6,0(r5) | sync ;
| li r7,1 ;
| stw r7,0(r6) ;
exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0)
Generated assembler
_litmus_P1_0_: lwz 27,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 30,0(11)
_litmus_P1_3_: xor 8,30,30
_litmus_P1_4_: lwzx 10,8,9
_litmus_P1_5_: sync
_litmus_P1_6_: li 7,1
_litmus_P1_7_: stw 7,0(9)
_litmus_P0_0_: lwz 30,0(11)
_litmus_P0_1_: xor 10,30,30
_litmus_P0_2_: lwzx 31,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw015 Allowed
Histogram (4 states)
73560358:>0:r1=0; 0:r4=0; 1:r1=0; 1:r3=1; 1:r5=0;
129275294:>0:r1=1; 0:r4=0; 1:r1=0; 1:r3=0; 1:r5=0;
255799984:>0:r1=0; 0:r4=0; 1:r1=0; 1:r3=0; 1:r5=0;
181364364:>0:r1=0; 0:r4=0; 1:r1=1; 1:r3=1; 1:r5=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=15f52564e04daa74ee8b809a62b31ce5
Cycle=SyncsRR DpdR SyncsRW Rfe DpdR SyncsRW Rfe
Relax bcssrw015 No BCSyncsRW
Safe=SyncsRR DpdR
Time bcssrw015 76.50
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw016.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw016
"LwSyncsRR DpdR SyncsRW Rfe DpdR SyncsRW Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | lwsync ;
lwzx r4,r3,r5 | lwz r3,0(r2) ;
sync | xor r4,r3,r3 ;
li r6,1 | lwzx r5,r4,r6 ;
stw r6,0(r5) | sync ;
| li r7,1 ;
| stw r7,0(r6) ;
exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0)
Generated assembler
_litmus_P1_0_: lwz 27,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 30,0(11)
_litmus_P1_3_: xor 8,30,30
_litmus_P1_4_: lwzx 10,8,9
_litmus_P1_5_: sync
_litmus_P1_6_: li 7,1
_litmus_P1_7_: stw 7,0(9)
_litmus_P0_0_: lwz 30,0(11)
_litmus_P0_1_: xor 10,30,30
_litmus_P0_2_: lwzx 31,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw016 Allowed
Histogram (4 states)
24438542:>0:r1=0; 0:r4=0; 1:r1=0; 1:r3=1; 1:r5=0;
171020966:>0:r1=1; 0:r4=0; 1:r1=0; 1:r3=0; 1:r5=0;
191882789:>0:r1=0; 0:r4=0; 1:r1=1; 1:r3=1; 1:r5=0;
252657703:>0:r1=0; 0:r4=0; 1:r1=0; 1:r3=0; 1:r5=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=da74259e4b84d84fe8b12e45af381e8e
Cycle=LwSyncsRR DpdR SyncsRW Rfe DpdR SyncsRW Rfe
Relax bcssrw016 No BCSyncsRW
Safe=LwSyncsRR DpdR
Time bcssrw016 74.64
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw017.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw017
"DpdW Wse SyncsWR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
sync | li r4,1 ;
lwz r3,0(r2) | stwx r4,r3,r5 ;
xor r4,r3,r3 | ;
lwzx r5,r4,r6 | ;
sync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1)
Generated assembler
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 30,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,30,9
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 27,0(11)
_litmus_P0_4_: xor 8,27,27
_litmus_P0_5_: lwzx 28,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw017 Allowed
Histogram (4 states)
12595560:>0:r3=1; 0:r5=0; 1:r1=0; x=1;
135787801:>0:r3=2; 0:r5=0; 1:r1=1; x=1;
194786938:>0:r3=2; 0:r5=0; 1:r1=0; x=1;
296829701:>0:r3=2; 0:r5=0; 1:r1=0; x=2;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1) is NOT validated
Hash=97b40d67b76129b3ab3e1a6a5f6305eb
Cycle=DpdW Wse SyncsWR DpdR SyncsRW Rfe
Relax bcssrw017 No BCSyncsRW
Safe=Wse SyncsWR DpdW DpdR
Time bcssrw017 65.31
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw018.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw018
"SyncdRW Wse SyncsWR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | sync ;
sync | li r3,1 ;
lwz r3,0(r2) | stw r3,0(r4) ;
xor r4,r3,r3 | ;
lwzx r5,r4,r6 | ;
sync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1)
Generated assembler
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 4,1
_litmus_P1_3_: stw 4,0(9)
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 27,0(11)
_litmus_P0_4_: xor 8,27,27
_litmus_P0_5_: lwzx 28,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw018 Allowed
Histogram (4 states)
12964049:>0:r3=1; 0:r5=0; 1:r1=0; x=1;
84859225:>0:r3=2; 0:r5=0; 1:r1=1; x=1;
274978545:>0:r3=2; 0:r5=0; 1:r1=0; x=2;
267198181:>0:r3=2; 0:r5=0; 1:r1=0; x=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1) is NOT validated
Hash=059b61899a92329ffeaf348803309697
Cycle=SyncdRW Wse SyncsWR DpdR SyncsRW Rfe
Relax bcssrw018 No BCSyncsRW
Safe=Wse SyncsWR SyncdRW DpdR
Time bcssrw018 64.26
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw019.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw019
"DpdR SyncsRW Wse SyncsWR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwzx r4,r3,r5 ;
lwz r3,0(r2) | sync ;
xor r4,r3,r3 | li r6,1 ;
lwzx r5,r4,r6 | stw r6,0(r5) ;
sync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0)
Generated assembler
_litmus_P1_0_: lwz 28,0(11)
_litmus_P1_1_: xor 10,28,28
_litmus_P1_2_: lwzx 30,10,9
_litmus_P1_3_: sync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 27,0(11)
_litmus_P0_4_: xor 8,27,27
_litmus_P0_5_: lwzx 28,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw019 Allowed
Histogram (6 states)
9707254:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; x=1;
2457817:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=2; x=1;
8151101:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=0; x=1;
190909315:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=2; x=1;
301094721:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=0; x=2;
127679792:>0:r3=2; 0:r5=0; 1:r1=1; 1:r4=2; x=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0) is NOT validated
Hash=ef298b82541a3b112e43ae882acb50a5
Cycle=DpdR SyncsRW Wse SyncsWR DpdR SyncsRW Rfe
Relax bcssrw019 No BCSyncsRW
Safe=Wse SyncsWR SyncsRW DpdR
Time bcssrw019 66.50
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw020.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw020
"LwSyncdRW Wse SyncsWR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync ;
sync | li r3,1 ;
lwz r3,0(r2) | stw r3,0(r4) ;
xor r4,r3,r3 | ;
lwzx r5,r4,r6 | ;
sync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1)
Generated assembler
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 4,1
_litmus_P1_3_: stw 4,0(9)
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 27,0(11)
_litmus_P0_4_: xor 8,27,27
_litmus_P0_5_: lwzx 28,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw020 Allowed
Histogram (4 states)
6932065:>0:r3=1; 0:r5=0; 1:r1=0; x=1;
265897268:>0:r3=2; 0:r5=0; 1:r1=0; x=1;
285565083:>0:r3=2; 0:r5=0; 1:r1=0; x=2;
81605584:>0:r3=2; 0:r5=0; 1:r1=1; x=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1) is NOT validated
Hash=7f2323c0dd7502796856c97da172b168
Cycle=LwSyncdRW Wse SyncsWR DpdR SyncsRW Rfe
Relax bcssrw020 No BCSyncsRW
Safe=Wse SyncsWR LwSyncdRW DpdR
Time bcssrw020 67.64
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw021.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw021
"DpdR LwSyncsRW Wse SyncsWR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwzx r4,r3,r5 ;
lwz r3,0(r2) | lwsync ;
xor r4,r3,r3 | li r6,1 ;
lwzx r5,r4,r6 | stw r6,0(r5) ;
sync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0)
Generated assembler
_litmus_P1_0_: lwz 28,0(11)
_litmus_P1_1_: xor 10,28,28
_litmus_P1_2_: lwzx 30,10,9
_litmus_P1_3_: lwsync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 27,0(11)
_litmus_P0_4_: xor 8,27,27
_litmus_P0_5_: lwzx 28,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw021 Allowed
Histogram (6 states)
699413:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; x=1;
3652136:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=2; x=1;
4925032:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=0; x=1;
195505954:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=2; x=1;
313052255:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=0; x=2;
122165210:>0:r3=2; 0:r5=0; 1:r1=1; 1:r4=2; x=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0) is NOT validated
Hash=3ac226fd1be7f310c6194b6c73f3c232
Cycle=DpdR LwSyncsRW Wse SyncsWR DpdR SyncsRW Rfe
Relax bcssrw021 No BCSyncsRW
Safe=Wse SyncsWR LwSyncsRW DpdR
Time bcssrw021 65.90
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw022.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw022
"DpdR Fre SyncsWR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwzx r4,r3,r5 ;
lwz r3,0(r2) | ;
xor r4,r3,r3 | ;
lwzx r5,r4,r6 | ;
sync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0)
Generated assembler
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 31,10,9
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw022 Allowed
Histogram (3 states)
176220072:>0:r3=1; 0:r5=0; 1:r1=1; 1:r4=1;
319980479:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0;
143799449:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0) is NOT validated
Hash=7ac3fafaae301cc73390972bbdd5c0f4
Cycle=DpdR Fre SyncsWR DpdR SyncsRW Rfe
Relax bcssrw022 No BCSyncsRW
Safe=Fre SyncsWR DpdR
Time bcssrw022 75.75
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw023.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw023
"SyncsRR DpdR Fre SyncsWR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | sync ;
sync | lwz r3,0(r2) ;
lwz r3,0(r2) | xor r4,r3,r3 ;
xor r4,r3,r3 | lwzx r5,r4,r6 ;
lwzx r5,r4,r6 | ;
sync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0)
Generated assembler
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 31,0(11)
_litmus_P1_3_: xor 8,31,31
_litmus_P1_4_: lwzx 10,8,9
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw023 Allowed
Histogram (4 states)
76365876:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=1;
124649054:>0:r3=1; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=1;
130503839:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=1;
308481231:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=c2c9c0359658b64e4185d23d932ca70a
Cycle=SyncsRR DpdR Fre SyncsWR DpdR SyncsRW Rfe
Relax bcssrw023 No BCSyncsRW
Safe=Fre SyncsWR SyncsRR DpdR
Time bcssrw023 78.06
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw024.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw024
"LwSyncsRR DpdR Fre SyncsWR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync ;
sync | lwz r3,0(r2) ;
lwz r3,0(r2) | xor r4,r3,r3 ;
xor r4,r3,r3 | lwzx r5,r4,r6 ;
lwzx r5,r4,r6 | ;
sync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0)
Generated assembler
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 31,0(11)
_litmus_P1_3_: xor 8,31,31
_litmus_P1_4_: lwzx 10,8,9
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw024 Allowed
Histogram (4 states)
21325646:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=1;
167197191:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=1;
319255890:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
132221273:>0:r3=1; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=dcde740d5eace2726b3b99bfd0448c43
Cycle=LwSyncsRR DpdR Fre SyncsWR DpdR SyncsRW Rfe
Relax bcssrw024 No BCSyncsRW
Safe=Fre SyncsWR LwSyncsRR DpdR
Time bcssrw024 77.63
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw025.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw025
"SyncdRR Fre SyncsWR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | sync ;
sync | lwz r3,0(r4) ;
lwz r3,0(r2) | ;
xor r4,r3,r3 | ;
lwzx r5,r4,r6 | ;
sync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=0)
Generated assembler
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw025 Allowed
Histogram (3 states)
133929131:>0:r3=1; 0:r5=0; 1:r1=1; 1:r3=1;
194648344:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=1;
311422525:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=0) is NOT validated
Hash=8047871ef7343012976d8a83d92f5d9f
Cycle=SyncdRR Fre SyncsWR DpdR SyncsRW Rfe
Relax bcssrw025 No BCSyncsRW
Safe=Fre SyncsWR SyncdRR DpdR
Time bcssrw025 75.74
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw026.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw026
"DpdR SyncsRR Fre SyncsWR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwzx r4,r3,r5 ;
lwz r3,0(r2) | sync ;
xor r4,r3,r3 | lwz r6,0(r5) ;
lwzx r5,r4,r6 | ;
sync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0 /\ 1:r6=0)
Generated assembler
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 8,30,30
_litmus_P1_2_: lwzx 31,8,9
_litmus_P1_3_: sync
_litmus_P1_4_: lwz 10,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw026 Allowed
Histogram (4 states)
11331065:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; 1:r6=1;
198300877:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=1; 1:r6=1;
307910837:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; 1:r6=0;
122457221:>0:r3=1; 0:r5=0; 1:r1=1; 1:r4=1; 1:r6=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0 /\ 1:r6=0) is NOT validated
Hash=e601791e1656e598fa3a9bacd4c2c5b2
Cycle=DpdR SyncsRR Fre SyncsWR DpdR SyncsRW Rfe
Relax bcssrw026 No BCSyncsRW
Safe=Fre SyncsWR SyncsRR DpdR
Time bcssrw026 75.90
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw027.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw027
"LwSyncdRR Fre SyncsWR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync ;
sync | lwz r3,0(r4) ;
lwz r3,0(r2) | ;
xor r4,r3,r3 | ;
lwzx r5,r4,r6 | ;
sync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=0)
Generated assembler
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw027 Allowed
Histogram (3 states)
129772069:>0:r3=1; 0:r5=0; 1:r1=1; 1:r3=1;
191170216:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=1;
319057715:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=0) is NOT validated
Hash=a9989a08ab5b3cfd8006a16e6ef9efd7
Cycle=LwSyncdRR Fre SyncsWR DpdR SyncsRW Rfe
Relax bcssrw027 No BCSyncsRW
Safe=Fre SyncsWR LwSyncdRR DpdR
Time bcssrw027 77.22
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw028.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw028
"DpdR LwSyncsRR Fre SyncsWR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwzx r4,r3,r5 ;
lwz r3,0(r2) | lwsync ;
xor r4,r3,r3 | lwz r6,0(r5) ;
lwzx r5,r4,r6 | ;
sync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0 /\ 1:r6=0)
Generated assembler
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 8,30,30
_litmus_P1_2_: lwzx 31,8,9
_litmus_P1_3_: lwsync
_litmus_P1_4_: lwz 10,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw028 Allowed
Histogram (4 states)
422362:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; 1:r6=1;
121410943:>0:r3=1; 0:r5=0; 1:r1=1; 1:r4=1; 1:r6=1;
318617910:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; 1:r6=0;
199548785:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=1; 1:r6=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0 /\ 1:r6=0) is NOT validated
Hash=f96ce8a4017924c7511ae42d30af7292
Cycle=DpdR LwSyncsRR Fre SyncsWR DpdR SyncsRW Rfe
Relax bcssrw028 No BCSyncsRW
Safe=Fre SyncsWR LwSyncsRR DpdR
Time bcssrw028 77.11
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw029.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw029
"SyncsRR DpdR SyncsRW Rfe SyncsRR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
lwz r1,0(r2) | lwz r1,0(r2) ;
sync | sync ;
lwz r3,0(r2) | lwz r3,0(r2) ;
xor r4,r3,r3 | xor r4,r3,r3 ;
lwzx r5,r4,r6 | lwzx r5,r4,r6 ;
sync | sync ;
li r7,1 | li r7,1 ;
stw r7,0(r6) | stw r7,0(r6) ;
exists (0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0)
Generated assembler
_litmus_P1_0_: lwz 27,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 30,0(11)
_litmus_P1_3_: xor 8,30,30
_litmus_P1_4_: lwzx 10,8,9
_litmus_P1_5_: sync
_litmus_P1_6_: li 7,1
_litmus_P1_7_: stw 7,0(9)
_litmus_P0_0_: lwz 27,0(11)
_litmus_P0_1_: sync
_litmus_P0_2_: lwz 30,0(11)
_litmus_P0_3_: xor 8,30,30
_litmus_P0_4_: lwzx 10,8,9
_litmus_P0_5_: sync
_litmus_P0_6_: li 7,1
_litmus_P0_7_: stw 7,0(9)
Test bcssrw029 Allowed
Histogram (5 states)
115655481:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
85333646:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
113648630:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=0;
79345799:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=0;
246016444:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=69e45967a3fe794a66d57ca3e640a326
Cycle=SyncsRR DpdR SyncsRW Rfe SyncsRR DpdR SyncsRW Rfe
Relax bcssrw029 No BCSyncsRW
Safe=SyncsRR DpdR
Time bcssrw029 78.37
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw030.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw030
"LwSyncsRR DpdR SyncsRW Rfe SyncsRR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
lwz r1,0(r2) | lwz r1,0(r2) ;
sync | lwsync ;
lwz r3,0(r2) | lwz r3,0(r2) ;
xor r4,r3,r3 | xor r4,r3,r3 ;
lwzx r5,r4,r6 | lwzx r5,r4,r6 ;
sync | sync ;
li r7,1 | li r7,1 ;
stw r7,0(r6) | stw r7,0(r6) ;
exists (0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0)
Generated assembler
_litmus_P1_0_: lwz 27,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 30,0(11)
_litmus_P1_3_: xor 8,30,30
_litmus_P1_4_: lwzx 10,8,9
_litmus_P1_5_: sync
_litmus_P1_6_: li 7,1
_litmus_P1_7_: stw 7,0(9)
_litmus_P0_0_: lwz 27,0(11)
_litmus_P0_1_: sync
_litmus_P0_2_: lwz 30,0(11)
_litmus_P0_3_: xor 8,30,30
_litmus_P0_4_: lwzx 10,8,9
_litmus_P0_5_: sync
_litmus_P0_6_: li 7,1
_litmus_P0_7_: stw 7,0(9)
Test bcssrw030 Allowed
Histogram (5 states)
19191340:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=0;
75208357:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
129379273:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=0;
169321662:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
246899368:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=ce33b1e1ca4525573eb6199b87f1a3d7
Cycle=LwSyncsRR DpdR SyncsRW Rfe SyncsRR DpdR SyncsRW Rfe
Relax bcssrw030 No BCSyncsRW
Safe=SyncsRR LwSyncsRR DpdR
Time bcssrw030 79.05
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw031.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw031
"LwSyncsRR DpdR SyncsRW Rfe LwSyncsRR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
lwz r1,0(r2) | lwz r1,0(r2) ;
lwsync | lwsync ;
lwz r3,0(r2) | lwz r3,0(r2) ;
xor r4,r3,r3 | xor r4,r3,r3 ;
lwzx r5,r4,r6 | lwzx r5,r4,r6 ;
sync | sync ;
li r7,1 | li r7,1 ;
stw r7,0(r6) | stw r7,0(r6) ;
exists (0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0)
Generated assembler
_litmus_P1_0_: lwz 27,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 30,0(11)
_litmus_P1_3_: xor 8,30,30
_litmus_P1_4_: lwzx 10,8,9
_litmus_P1_5_: sync
_litmus_P1_6_: li 7,1
_litmus_P1_7_: stw 7,0(9)
_litmus_P0_0_: lwz 27,0(11)
_litmus_P0_1_: lwsync
_litmus_P0_2_: lwz 30,0(11)
_litmus_P0_3_: xor 8,30,30
_litmus_P0_4_: lwzx 10,8,9
_litmus_P0_5_: sync
_litmus_P0_6_: li 7,1
_litmus_P0_7_: stw 7,0(9)
Test bcssrw031 Allowed
Histogram (5 states)
27636851:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
173260488:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=0;
181539702:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
24371889:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=0;
233191070:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=ae803005916745f384198d670ee29f6c
Cycle=LwSyncsRR DpdR SyncsRW Rfe LwSyncsRR DpdR SyncsRW Rfe
Relax bcssrw031 No BCSyncsRW
Safe=LwSyncsRR DpdR
Time bcssrw031 79.70
$Revision: 3163 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 2000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 20000
#endif
#ifndef N_EXE
#define N_EXE (32 < N ? 1 : 32 / N)
#endif
/* gcc options: -Wall -std=gnu99 -O -pthread */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: true */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 32 */
GCCOPTS="-Wall -std=gnu99 -O -pthread"
LITMUSOPTS=
Wed Dec 30 10:35:08 GMT 2009