Wed Dec 30 09:38:57 GMT 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww000
"DpdR Fre SyncsWW Rfe DpdR Fre SyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r5=y; 2:r2=y; 3:r2=y; 3:r5=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwzx r4,r3,r5 | sync | lwzx r4,r3,r5 ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 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_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: 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_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww000 Allowed
Histogram (77 states)
1 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
3 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
7 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
4 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
8 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
3004 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
1781 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
1390 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
4376 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
4170 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
1546 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
35304 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
1456 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
22789 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
12276 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
6176 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
4834 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
3951 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
35990 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
85695 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
92276 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
26555 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
152353:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
130399:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
210662:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
1204846:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
1321813:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
638091:>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
80564 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
56324 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
39819 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
497885:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
579573:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
1394140:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
2437150:>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
4902943:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
924758:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
2081398:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
112277:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
672381:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
861808:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
2977641:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
10535447:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
747782:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
2143095:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
1092804:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
3783192:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
2300171:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
1374460:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
2722328:>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
3472688:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
704410:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
2239488:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
2467859:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
4253574:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
2561255:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
3124544:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
14427446:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
4940445:>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
1377539:>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
4636707:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
5260740:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
4150029:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
2014967:>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
10442370:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
4655992:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
3172493:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
14115593:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
3456318:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
3375574:>1:r1=2; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
19716465:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
4340168:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
19442917:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
20074359:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
19451585:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
38671704:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
57133075:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r4=0) is NOT validated
Hash=9fe623fb41a5ce2e4216ef423b67f696
Cycle=DpdR Fre SyncsWW Rfe DpdR Fre SyncsWW Rfe
Relax bcssww000 No BCSyncsWW
Safe=Fre DpdR
Time bcssww000 103.39
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww001
"SyncdRR Fre SyncsWW Rfe DpdR Fre SyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r5=y; 2:r2=y; 3:r2=y; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | sync ;
sync | lwzx r4,r3,r5 | sync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 30,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: 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_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww001 Allowed
Histogram (77 states)
1 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
3 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
6 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
1 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
2 :>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
1572 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
2955 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
1232 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
2680 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
1375 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
1407 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
16709 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
121816:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
69349 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
46304 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
8488 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
15011 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
24550 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
26735 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
393418:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
455830:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
208722:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
258773:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
882917:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
91700 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
679567:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
242493:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
164753:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
836457:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
602122:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
1358398:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
700717:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
722522:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
47631 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
274202:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
2081655:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
1123127:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
4983313:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
2011723:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
2083618:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
386845:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
1216765:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
2504216:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
2908797:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
6110289:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
1288713:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
4577270:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
4197968:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
4862308:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
843152:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
687043:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
2916168:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
3843351:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
2349413:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
3787604:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
1162576:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
2341796:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
3184209:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
1779723:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
10861165:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
13365776:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
2426552:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
3845554:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
1426128:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
2424600:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
16829939:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
17741470:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
21371299:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
5105004:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
3746090:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
2942966:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
13106417:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
17997499:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
19121915:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
3366142:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
35189595:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
57639829:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=c19feeb22b3e4fe95d3ae9cd399e4667
Cycle=SyncdRR Fre SyncsWW Rfe DpdR Fre SyncsWW Rfe
Relax bcssww001 No BCSyncsWW
Safe=Fre SyncdRR DpdR
Time bcssww001 101.97
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww002
"LwSyncdRR Fre SyncsWW Rfe DpdR Fre SyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r5=y; 2:r2=y; 3:r2=y; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ;
sync | lwzx r4,r3,r5 | sync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 30,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: 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_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww002 Allowed
Histogram (79 states)
1 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
1 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
2 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
3 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
2 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
1 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
6 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
2075 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
3532 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
2961 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
14572 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
1950 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
48375 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
12720 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
1895 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
1165 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
27939 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
583926:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
47337 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
835562:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
1434303:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
183434:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
1994313:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
2371987:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
39625 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
237734:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
1289471:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
3853840:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
104519:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
426561:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
63377 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
608116:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
2436916:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
260867:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
2122834:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
920002:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
377394:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
19742 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
182220:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
2184981:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
1181590:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
141598:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
702225:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
1699172:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
722716:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
2381407:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
2578590:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
1579871:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
404391:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
1193935:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
4171389:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
5083527:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
5227284:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
3328651:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
1292983:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
248343:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
3569176:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
931853:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
4008155:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
3113340:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
3190640:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
3411705:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
2860210:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
694312:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
5965760:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
3792667:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
2312550:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
4786530:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
19551958:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
58726474:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
34299427:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
16491878:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
17943996:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
4020197:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
12697727:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
12744832:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
21147689:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
10737045:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
18367946:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=a2812688a109c131b01004a694cfdd81
Cycle=LwSyncdRR Fre SyncsWW Rfe DpdR Fre SyncsWW Rfe
Relax bcssww002 No BCSyncsWW
Safe=Fre LwSyncdRR DpdR
Time bcssww002 101.26
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww003
"DpdW Wse SyncdWR Fre SyncsWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r5=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
sync | sync | li r4,1 ;
lwz r3,0(r4) | li r3,2 | stwx r4,r3,r5 ;
| stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 0:r3=0 /\ 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_: li 5,1
_litmus_P1_1_: stw 5,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 30,2
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww003 Allowed
Histogram (17 states)
6 :>0:r3=1; 2:r1=2; x=2; y=2;
19 :>0:r3=0; 2:r1=1; x=2; y=2;
294489:>0:r3=1; 2:r1=0; x=1; y=2;
137024:>0:r3=2; 2:r1=0; x=1; y=2;
3169975:>0:r3=1; 2:r1=2; x=1; y=2;
244552:>0:r3=1; 2:r1=1; x=2; y=2;
1451793:>0:r3=2; 2:r1=1; x=1; y=2;
1621012:>0:r3=1; 2:r1=1; x=1; y=2;
6293816:>0:r3=2; 2:r1=1; x=2; y=2;
18314874:>0:r3=1; 2:r1=0; x=2; y=2;
75054129:>0:r3=0; 2:r1=0; x=1; y=2;
18175201:>0:r3=0; 2:r1=1; x=1; y=2;
88632786:>0:r3=2; 2:r1=2; x=1; y=2;
60060716:>0:r3=2; 2:r1=0; x=2; y=2;
37400982:>0:r3=0; 2:r1=2; x=1; y=2;
34989013:>0:r3=2; 2:r1=2; x=2; y=2;
54159613:>0:r3=0; 2:r1=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2) is NOT validated
Hash=316a93ca86d6e131419704cdf84a4e06
Cycle=DpdW Wse SyncdWR Fre SyncsWW Rfe
Relax bcssww003 No BCSyncsWW
Safe=Fre Wse SyncdWR DpdW
Time bcssww003 62.47
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww004
"SyncdRW Wse SyncdWR Fre SyncsWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | li r3,1 ;
lwz r3,0(r4) | li r3,2 | stw r3,0(r4) ;
| stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 0:r3=0 /\ 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_: li 5,1
_litmus_P1_1_: stw 5,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 30,2
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww004 Allowed
Histogram (15 states)
130032:>0:r3=1; 2:r1=1; x=2; y=2;
815136:>0:r3=2; 2:r1=0; x=1; y=2;
3158600:>0:r3=1; 2:r1=2; x=1; y=2;
6093416:>0:r3=2; 2:r1=1; x=2; y=2;
576377:>0:r3=1; 2:r1=0; x=1; y=2;
3835980:>0:r3=2; 2:r1=1; x=1; y=2;
2138782:>0:r3=1; 2:r1=1; x=1; y=2;
16807764:>0:r3=1; 2:r1=0; x=2; y=2;
88132131:>0:r3=0; 2:r1=0; x=1; y=2;
16299102:>0:r3=0; 2:r1=1; x=1; y=2;
61563230:>0:r3=2; 2:r1=0; x=2; y=2;
90697302:>0:r3=2; 2:r1=2; x=1; y=2;
40541810:>0:r3=0; 2:r1=0; x=2; y=2;
38519302:>0:r3=0; 2:r1=2; x=1; y=2;
30691036:>0:r3=2; 2:r1=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2) is NOT validated
Hash=4a84f5a0d5b5b42156717d2ee2b4312f
Cycle=SyncdRW Wse SyncdWR Fre SyncsWW Rfe
Relax bcssww004 No BCSyncsWW
Safe=Fre Wse SyncdWR SyncdRW
Time bcssww004 63.33
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww005
"LwSyncdRW Wse SyncdWR Fre SyncsWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | li r3,1 ;
lwz r3,0(r4) | li r3,2 | stw r3,0(r4) ;
| stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 0:r3=0 /\ 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_: li 5,1
_litmus_P1_1_: stw 5,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 30,2
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww005 Allowed
Histogram (17 states)
1 :>0:r3=1; 2:r1=2; x=2; y=2;
1 :>0:r3=0; 2:r1=1; x=2; y=2;
181739:>0:r3=1; 2:r1=1; x=2; y=2;
410217:>0:r3=2; 2:r1=0; x=1; y=2;
3255191:>0:r3=1; 2:r1=2; x=1; y=2;
2239050:>0:r3=1; 2:r1=1; x=1; y=2;
507690:>0:r3=1; 2:r1=0; x=1; y=2;
3600788:>0:r3=2; 2:r1=1; x=1; y=2;
6575728:>0:r3=2; 2:r1=1; x=2; y=2;
16847908:>0:r3=0; 2:r1=1; x=1; y=2;
62493685:>0:r3=2; 2:r1=0; x=2; y=2;
37006052:>0:r3=0; 2:r1=2; x=1; y=2;
18156524:>0:r3=1; 2:r1=0; x=2; y=2;
88961040:>0:r3=2; 2:r1=2; x=1; y=2;
31964298:>0:r3=2; 2:r1=2; x=2; y=2;
46518102:>0:r3=0; 2:r1=0; x=2; y=2;
81281986:>0:r3=0; 2:r1=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2) is NOT validated
Hash=585ce030a2274090c0b4fa0251d7b3ad
Cycle=LwSyncdRW Wse SyncdWR Fre SyncsWW Rfe
Relax bcssww005 No BCSyncsWW
Safe=Fre Wse SyncdWR LwSyncdRW
Time bcssww005 63.96
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww006
"DpdR Fre SyncdWR Fre SyncsWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r5=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
sync | sync | lwzx r4,r3,r5 ;
lwz r3,0(r4) | li r3,2 | ;
| stw r3,0(r2) | ;
exists (y=2 /\ 0:r3=0 /\ 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_: li 5,1
_litmus_P1_1_: stw 5,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 30,1
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww006 Allowed
Histogram (17 states)
26 :>0:r3=0; 2:r1=1; 2:r4=0; y=2;
6 :>0:r3=1; 2:r1=2; 2:r4=0; y=2;
203648:>0:r3=1; 2:r1=0; 2:r4=1; y=2;
80300 :>0:r3=2; 2:r1=0; 2:r4=1; y=2;
2027747:>0:r3=1; 2:r1=2; 2:r4=1; y=2;
303442:>0:r3=1; 2:r1=1; 2:r4=0; y=2;
901361:>0:r3=2; 2:r1=1; 2:r4=1; y=2;
1286424:>0:r3=1; 2:r1=1; 2:r4=1; y=2;
17258635:>0:r3=0; 2:r1=1; 2:r4=1; y=2;
16300219:>0:r3=1; 2:r1=0; 2:r4=0; y=2;
6427733:>0:r3=2; 2:r1=1; 2:r4=0; y=2;
61724899:>0:r3=2; 2:r1=0; 2:r4=0; y=2;
41446458:>0:r3=2; 2:r1=2; 2:r4=0; y=2;
70085152:>0:r3=0; 2:r1=0; 2:r4=1; y=2;
54332573:>0:r3=0; 2:r1=0; 2:r4=0; y=2;
43694866:>0:r3=0; 2:r1=2; 2:r4=1; y=2;
83926511:>0:r3=2; 2:r1=2; 2:r4=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r4=0) is NOT validated
Hash=eea77ff32793e8bed4abb1ad0c914c0d
Cycle=DpdR Fre SyncdWR Fre SyncsWW Rfe
Relax bcssww006 No BCSyncsWW
Safe=Fre SyncdWR DpdR
Time bcssww006 63.27
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww007
"SyncdRR Fre SyncdWR Fre SyncsWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | lwz r3,0(r4) ;
lwz r3,0(r4) | li r3,2 | ;
| stw r3,0(r2) | ;
exists (y=2 /\ 0:r3=0 /\ 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_: li 5,1
_litmus_P1_1_: stw 5,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 30,1
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww007 Allowed
Histogram (17 states)
1 :>0:r3=1; 2:r1=2; 2:r3=0; y=2;
2 :>0:r3=0; 2:r1=1; 2:r3=0; y=2;
272687:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
232703:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
213955:>0:r3=1; 2:r1=1; 2:r3=0; y=2;
2002624:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
3149269:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
17053811:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
2693165:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
7630053:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
16698908:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
62236624:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
76412768:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
36397730:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
51262539:>0:r3=0; 2:r1=0; 2:r3=0; y=2;
38712196:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
85030965:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=66d340e023bd1d1ae19ed5903eb5d2ea
Cycle=SyncdRR Fre SyncdWR Fre SyncsWW Rfe
Relax bcssww007 No BCSyncsWW
Safe=Fre SyncdWR SyncdRR
Time bcssww007 63.96
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww008.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww008
"LwSyncdRR Fre SyncdWR Fre SyncsWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | lwz r3,0(r4) ;
lwz r3,0(r4) | li r3,2 | ;
| stw r3,0(r2) | ;
exists (y=2 /\ 0:r3=0 /\ 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_: li 5,1
_litmus_P1_1_: stw 5,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 30,1
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww008 Allowed
Histogram (17 states)
24 :>0:r3=1; 2:r1=2; 2:r3=0; y=2;
65 :>0:r3=0; 2:r1=1; 2:r3=0; y=2;
370431:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
278322:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
243343:>0:r3=1; 2:r1=1; 2:r3=0; y=2;
2905666:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
3296550:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
9196669:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
2269375:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
17147731:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
51611025:>0:r3=0; 2:r1=0; 2:r3=0; y=2;
36406185:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
17860877:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
37169991:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
62341731:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
83345395:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
75556620:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=d19882d97477fc15c9e4fbc588dc8a96
Cycle=LwSyncdRR Fre SyncdWR Fre SyncsWW Rfe
Relax bcssww008 No BCSyncsWW
Safe=Fre SyncdWR LwSyncdRR
Time bcssww008 65.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww009.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww009
"SyncdRR Fre SyncsWW Rfe SyncdRR Fre SyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | sync ;
sync | lwz r3,0(r4) | sync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 30,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 30,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww009 Allowed
Histogram (72 states)
1440 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1761 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
961 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1078 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
2508 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1770 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
9909 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
50181 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
63797 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
707628:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
63711 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
329372:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1197724:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
73963 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
172116:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
166888:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
732358:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
272211:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
2102285:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
754773:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1166542:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
928937:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
890637:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
2248591:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
2264899:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
742560:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
2253243:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
231840:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
2606199:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
2380750:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
2278646:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1615072:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
356132:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1205270:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
336055:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1763014:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
758276:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
2507856:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
4053227:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
2487780:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
2305641:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
740823:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1220357:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1434094:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2357464:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
6350206:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
333121:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
767980:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
2267900:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
908821:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
13567014:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
4226753:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
17133889:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
4383193:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
4825787:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1450567:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
15824672:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
6392445:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
382566:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
4857932:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
394630:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
15751252:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
257714:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
4498840:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
4452924:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
31736606:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
16472657:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
4596497:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
14078210:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
19299204:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
19115789:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
57832492:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=ac99317f895df8ed08197fb9ed0e136a
Cycle=SyncdRR Fre SyncsWW Rfe SyncdRR Fre SyncsWW Rfe
Relax bcssww009 No BCSyncsWW
Safe=Fre SyncdRR
Time bcssww009 101.04
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww010
"LwSyncdRR Fre SyncsWW Rfe SyncdRR Fre SyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | lwsync ;
sync | lwz r3,0(r4) | sync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 30,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 30,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww010 Allowed
Histogram (75 states)
2 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
1 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
2 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
1409 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
2139 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1014 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
2093 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1165 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
8236 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1314 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
46680 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
138256:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
623715:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
81235 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
51408 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
139961:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
37597 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1067471:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
798356:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
289793:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1330148:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
354892:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
352449:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
234214:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
788929:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1308048:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
263838:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
4104929:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1607322:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
216744:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1991120:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
886482:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
806616:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
554232:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
322615:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2960374:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
3618612:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
306872:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1809062:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1098510:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
2476699:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
4491798:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
767549:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
2575669:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
2963842:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
13360999:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
4273075:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
2952136:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
14418979:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
1264818:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
324071:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1791145:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
3898397:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
4157025:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
2096730:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
347253:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
4147224:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
2132330:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
781555:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
2102781:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
4093263:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
431122:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
16155370:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
15501739:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
2353991:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
6038102:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
20449416:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
19737903:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
5679454:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
32454000:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
17389224:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
17507795:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
2035517:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1126787:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
59514387:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=fdf7665f1e0ce0f0c6d4d353ee548d9e
Cycle=LwSyncdRR Fre SyncsWW Rfe SyncdRR Fre SyncsWW Rfe
Relax bcssww010 No BCSyncsWW
Safe=Fre SyncdRR LwSyncdRR
Time bcssww010 102.41
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww011.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww011
"LwSyncdRR Fre SyncsWW Rfe LwSyncdRR Fre SyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
sync | lwz r3,0(r4) | sync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 30,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 30,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww011 Allowed
Histogram (74 states)
1 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
1 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
1568 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2098 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1137 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
2556 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1672 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
22292 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1191 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
30027 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
519859:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
351143:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
47098 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
231586:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1316769:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
82490 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
354709:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
10012 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
838009:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
310363:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
2265219:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1300588:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
206518:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
295168:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
3073318:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1362618:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2575658:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
2370821:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
139191:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
4377649:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2586019:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
1206938:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
591413:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
2244803:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
859848:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
850649:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
308408:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2746310:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1401287:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
141077:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1863826:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
823691:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
2492442:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
300388:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
4480963:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
3110546:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
2275400:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
31002400:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
16184052:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
2334256:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1206853:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
230332:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
4313048:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
715813:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
850137:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1667641:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
4250228:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
5906179:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
4205212:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
642330:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
15042882:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
4108553:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
60516746:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
683814:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1797325:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
3875526:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
16499097:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
4201856:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
6012707:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
13703212:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
19930821:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
19919803:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
13315377:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
16508463:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=7c8f7188794f6e0c8b799c86369a2299
Cycle=LwSyncdRR Fre SyncsWW Rfe LwSyncdRR Fre SyncsWW Rfe
Relax bcssww011 No BCSyncsWW
Safe=Fre LwSyncdRR
Time bcssww011 103.81
$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 09:55:34 GMT 2009