Mon Dec 28 13:14:13 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 3,0(11)
_litmus_P3_1_: xor 10,3,3
_litmus_P3_2_: lwzx 31,10,9
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,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_: xor 10,3,3
_litmus_P1_2_: lwzx 31,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 (72 states)
342 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
302 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
201 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
235 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
2675 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
3700 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
3373 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
211 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
232 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
5194 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
153503:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
29276 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
35045 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
1279 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
179305:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
77277 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
115420:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
66299 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
175530:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
404805:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
42899 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
88673 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
48922 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
80018 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
70777 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
30924 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
43781 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
42879 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
133791:>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
472419:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
1897890:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
1574278:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
2216290:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
71657 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
261792:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
122012:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
655620:>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
1203700:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
1161931:>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
211622:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
424631:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
1381343:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
935402:>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
643168:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
1342765:>1:r1=2; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
1098800:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
773662:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
250919:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
276107:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
422860:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
11296440:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
2079342:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
787319:>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
1878257:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
1316046:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
8278386:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
1686187:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
2000291:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
2150838:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
1710911:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
755935:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
2570369:>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
7802087:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
907532:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
8351406:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
7704911:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
9985696:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
21913870:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
2278886:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
10694641:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
10632724:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
23982190:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 160000000
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 83.95
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,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_: xor 10,3,3
_litmus_P1_2_: lwzx 31,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 (72 states)
206 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
158 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
103 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
261 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
1234 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
198 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
202 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
1972 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
5717 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
23101 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
3771 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
116941:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
32491 :>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
36152 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
237790:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
64970 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
186790:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
12626 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
65172 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
177603:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
109802:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
253588:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
660721:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
121422:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
444263:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
147166:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
92695 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
21722 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
30535 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
78967 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
761984:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
91281 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
72860 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
872405:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
2870708:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
258641:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
1399082:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
1697610:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
22394 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
1164005:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
1531205:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
95159 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
277021:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
1673895:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
1103072:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
576036:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
325128:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
1854607:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
1569977:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
11823951:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
2398131:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
1141301:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
1026584:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
2168932:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
235010:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
1153702:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
1376449:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
676599:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
7071930:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
10645500:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
1254883:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
598522:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
10347487:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
217462:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
10262440:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
7984494:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
23784486:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
6464930:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
8208016:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
2208620:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
26228179:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
1576983:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 160000000
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 84.22
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,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_: xor 10,3,3
_litmus_P1_2_: lwzx 31,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 (72 states)
146 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
310 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
230 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
233 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
202 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
3772 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
253 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
127931:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
4063 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
36669 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
8996 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
58060 :>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
5669 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
191981:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
43978 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
102038:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
149159:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
47099 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
453984:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
48999 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
43545 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
72391 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
1473 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
97965 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
1449622:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
412029:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
210261:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
267340:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
701520:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
198567:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
327896:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
2088001:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
842092:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
1735970:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
293805:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
680625:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
710686:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
1672591:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
780519:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
141789:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
1771028:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
359854:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
1225549:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
2344524:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
884055:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
353939:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
1104068:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
1847396:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
1109638:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
232024:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
106858:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
2854289:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
1334789:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
130629:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
32299 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
593291:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
1240330:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
1940105:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
7549886:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
10863423:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
1847156:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
8469121:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
6702181:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
10782137:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
1382382:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
2345755:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
21681729:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
24507180:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
10232455:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
10902024:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
2168413:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
7089034:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 160000000
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 83.25
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P2_1_: xor 31,3,3
_litmus_P2_2_: li 10,1
_litmus_P2_3_: stwx 10,31,9
_litmus_P1_0_: li 6,1
_litmus_P1_1_: stw 6,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww003 Allowed
Histogram (15 states)
33648 :>0:r3=1; 2:r1=1; x=2; y=2;
7232442:>0:r3=1; 2:r1=0; x=2; y=2;
168432:>0:r3=1; 2:r1=0; x=1; y=2;
1386748:>0:r3=1; 2:r1=2; x=1; y=2;
128460:>0:r3=2; 2:r1=0; x=1; y=2;
34701154:>0:r3=0; 2:r1=0; x=1; y=2;
1359556:>0:r3=1; 2:r1=1; x=1; y=2;
1884673:>0:r3=2; 2:r1=1; x=1; y=2;
9401449:>0:r3=0; 2:r1=1; x=1; y=2;
20085263:>0:r3=0; 2:r1=2; x=1; y=2;
2735812:>0:r3=2; 2:r1=1; x=2; y=2;
27716859:>0:r3=0; 2:r1=0; x=2; y=2;
47918805:>0:r3=2; 2:r1=2; x=1; y=2;
14547442:>0:r3=2; 2:r1=2; x=2; y=2;
30699257:>0:r3=2; 2:r1=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 200000000
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 48.53
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,1
_litmus_P2_3_: stw 4,0(9)
_litmus_P1_0_: li 6,1
_litmus_P1_1_: stw 6,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww004 Allowed
Histogram (15 states)
28625 :>0:r3=1; 2:r1=1; x=2; y=2;
2753008:>0:r3=2; 2:r1=1; x=2; y=2;
388640:>0:r3=1; 2:r1=0; x=1; y=2;
6743040:>0:r3=1; 2:r1=0; x=2; y=2;
990453:>0:r3=1; 2:r1=2; x=1; y=2;
1835116:>0:r3=1; 2:r1=1; x=1; y=2;
10002503:>0:r3=0; 2:r1=1; x=1; y=2;
3339245:>0:r3=2; 2:r1=1; x=1; y=2;
921495:>0:r3=2; 2:r1=0; x=1; y=2;
11689055:>0:r3=2; 2:r1=2; x=2; y=2;
30660093:>0:r3=2; 2:r1=0; x=2; y=2;
19164974:>0:r3=0; 2:r1=2; x=1; y=2;
48185581:>0:r3=2; 2:r1=2; x=1; y=2;
20960310:>0:r3=0; 2:r1=0; x=2; y=2;
42337862:>0:r3=0; 2:r1=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 200000000
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 49.25
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,1
_litmus_P2_3_: stw 4,0(9)
_litmus_P1_0_: li 6,1
_litmus_P1_1_: stw 6,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww005 Allowed
Histogram (15 states)
37417 :>0:r3=1; 2:r1=1; x=2; y=2;
304963:>0:r3=1; 2:r1=0; x=1; y=2;
1008801:>0:r3=1; 2:r1=2; x=1; y=2;
369325:>0:r3=2; 2:r1=0; x=1; y=2;
2407921:>0:r3=2; 2:r1=1; x=1; y=2;
15709070:>0:r3=2; 2:r1=2; x=2; y=2;
1544091:>0:r3=1; 2:r1=1; x=1; y=2;
6241352:>0:r3=1; 2:r1=0; x=2; y=2;
8943288:>0:r3=0; 2:r1=1; x=1; y=2;
29028068:>0:r3=2; 2:r1=0; x=2; y=2;
45753519:>0:r3=2; 2:r1=2; x=1; y=2;
38637037:>0:r3=0; 2:r1=0; x=1; y=2;
2675177:>0:r3=2; 2:r1=1; x=2; y=2;
26286017:>0:r3=0; 2:r1=0; x=2; y=2;
21053954:>0:r3=0; 2:r1=2; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 200000000
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 49.71
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,0(11)
_litmus_P2_1_: xor 10,30,30
_litmus_P2_2_: lwzx 31,10,9
_litmus_P1_0_: li 6,1
_litmus_P1_1_: stw 6,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww006 Allowed
Histogram (15 states)
173036:>0:r3=1; 2:r1=0; 2:r4=1; y=2;
151988:>0:r3=2; 2:r1=0; 2:r4=1; y=2;
51304 :>0:r3=1; 2:r1=1; 2:r4=0; y=2;
2080620:>0:r3=2; 2:r1=1; 2:r4=1; y=2;
44785528:>0:r3=2; 2:r1=2; 2:r4=1; y=2;
6398341:>0:r3=1; 2:r1=0; 2:r4=0; y=2;
1589753:>0:r3=1; 2:r1=2; 2:r4=1; y=2;
20644881:>0:r3=0; 2:r1=2; 2:r4=1; y=2;
2065445:>0:r3=1; 2:r1=1; 2:r4=1; y=2;
23469436:>0:r3=0; 2:r1=0; 2:r4=0; y=2;
3520637:>0:r3=2; 2:r1=1; 2:r4=0; y=2;
8087020:>0:r3=0; 2:r1=1; 2:r4=1; y=2;
15810086:>0:r3=2; 2:r1=2; 2:r4=0; y=2;
36558455:>0:r3=2; 2:r1=0; 2:r4=0; y=2;
34613470:>0:r3=0; 2:r1=0; 2:r4=1; y=2;
No
Witnesses
Positive: 0, Negative: 200000000
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 48.89
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: li 6,1
_litmus_P1_1_: stw 6,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww007 Allowed
Histogram (15 states)
175651:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
50317 :>0:r3=1; 2:r1=1; 2:r3=0; y=2;
323709:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
1023780:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
2423378:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
2082743:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
3554103:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
9047703:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
36508999:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
15544175:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
21615714:>0:r3=0; 2:r1=0; 2:r3=0; y=2;
6881926:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
44273211:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
36656150:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
19838441:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 200000000
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 47.59
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: li 6,1
_litmus_P1_1_: stw 6,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww008 Allowed
Histogram (15 states)
70046 :>0:r3=1; 2:r1=1; 2:r3=0; y=2;
287140:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
1049702:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
1018978:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
2375766:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
9354119:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
3229687:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
16532953:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
7024790:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
21040071:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
34946426:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
41785600:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
4401355:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
22710908:>0:r3=0; 2:r1=0; 2:r3=0; y=2;
34172459:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 200000000
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 47.50
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,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 4,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)
284 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
296 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
91 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
182 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
165 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
108 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1315 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
28294 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
35305 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
8012 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
313249:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
42898 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
29008 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
94540 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
16428 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
161264:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
303062:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
832941:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
142403:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
249081:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
131349:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
300503:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
145661:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1718540:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
937920:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
253839:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
136012:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
123585:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
611491:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1305400:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
281386:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
2439365:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1780340:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
128112:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
834333:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
98513 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
110651:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
820638:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
1315524:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
23745 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
2000114:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
940186:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
2142204:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
8751729:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
282544:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
316253:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
306573:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
310903:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
462092:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
358529:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
586214:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
10674575:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
733987:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
38066 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2280260:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
1009915:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
951998:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
565780:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1764111:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
10481203:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
7586777:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
8344736:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
7686056:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
840989:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1519781:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
2113752:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2335893:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
23655006:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
111109:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
7793307:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
28259320:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
9040205:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 160000000
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 83.65
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,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 4,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 (72 states)
212 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1409 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
216 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
176 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1014 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
11088 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
182 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
104680:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1698 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
38351 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
86133 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
35146 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
25929 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
214573:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
113547:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
43646 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
222372:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
221824:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
104373:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
181213:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
12169 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
21328 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
394567:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
133894:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
971462:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
395801:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
187107:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
270615:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
118991:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
540711:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
826562:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
151852:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
2662434:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
581476:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
2549822:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1085701:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
209993:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1207478:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
370851:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
174721:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
237375:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
71060 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
763992:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
814757:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2246956:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1704793:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1807952:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1063236:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1709606:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
977236:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
8084657:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1756717:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
275883:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
736597:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
341036:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
251189:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1427784:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
1922408:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1235204:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
2421342:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
9871253:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
7937751:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
2796958:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
9880063:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
2129717:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
7935789:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
11046366:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
7481667:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
24314736:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
21478892:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
990178:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
10011533:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 160000000
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 82.77
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,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 4,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 (72 states)
183 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
172 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
117 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
201 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
180 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
171 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1391 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
42241 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
30170 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
312323:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
32330 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
40986 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
22893 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
7786 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
191329:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
278479:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
259350:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
103168:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
70431 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
121080:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
348014:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
128776:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
155061:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
510527:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1424112:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1046239:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
165622:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
346115:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
108275:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1064661:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
16551 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
106564:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
258237:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
825990:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
1111229:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
1736074:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
122179:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
4568 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
488105:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1041865:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
111948:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
719626:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
9393 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1442915:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
1664997:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
2326286:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
160623:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
9030944:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
697868:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2311289:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
659351:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2487279:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2066040:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
445377:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
7788124:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
74452 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
2436043:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1835229:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
237747:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
9678832:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
561788:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
8496030:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
2545772:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
2238581:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
10611438:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
8302622:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
366888:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
10303529:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
25390241:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
22896738:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
943158:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
8635107:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 160000000
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 83.82
$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 (16 < N ? 1 : 16 / N)
#endif
/* gcc options: -Wall -std=gnu99 -O -pthread */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 16 */
GCCOPTS="-Wall -std=gnu99 -O -pthread"
LITMUSOPTS=-s 1000000 -r 40
Mon Dec 28 13:27:29 GMT 2009