Thu Dec 24 10:09:19 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 (79 states)
2 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
1 :>1:r1=2; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
6 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
2 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
2 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
6 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
3 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
1595 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
1806 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
4215 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
3486 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
3379 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
8873 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
1888 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
4151 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
6931 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
39470 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
1492 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
3543 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
36664 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
43315 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
25993 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
26426 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
80396 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
78983 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
96364 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
96669 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
903021:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
189387:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
907969:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
113016:>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
393575:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
194316:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
2223613:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
114736:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
737712:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
627988:>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
3194305:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
1103207:>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
2275057:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
2840397:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
390336:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
728401:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
3377584:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
1435462:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
2165665:>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
2445056:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
1119902:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
1450394:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
2335395:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
642944:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
3377116:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
2454378:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
4467888:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
4380700:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
5127685:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
2740126:>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
14450835:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
1426905:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
1469763:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
4820342:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
10484050:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
4538302:>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
4322460:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
3776563:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
4828736:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
2276093:>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
2127061:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
3322372:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
10420403:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
19553681:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
3632863:>1:r1=2; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
19470592:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
19815535:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
14253207:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
4144396:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
39819575:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
19685267:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
56338007:>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 94.56
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (75 states)
2 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
2 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
1 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
3991 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
8057 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
1549 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
1821 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
1582 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
3298 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
1341 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
43054 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
50133 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
155436:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
402167:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
1155314:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
63594 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
197112:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
234654:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
551283:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
18318 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
126675:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
573970:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
32512 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
309283:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
1065818:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
2621848:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
3444737:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
557866:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
653771:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
2298035:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
272267:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
1268090:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
1862528:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
1512017:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
2118259:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
2867353:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
3691372:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
21526640:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
3469975:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
2910934:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
4621476:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
14247682:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
2167227:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
3750397:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
84062 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
921878:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
5242574:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
2075693:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
3774332:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
916915:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
18788626:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
834287:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
26113 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
145939:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
5942244:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
13304 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
2701769:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
306259:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
1134803:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
4515503:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
2313699:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
3924360:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
422965:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
10191645:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
18889327:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
3328790:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
1957154:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
1243422:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
17723893:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
17204782:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
4945319:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
2216707:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
13484165:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
35363211:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
58502819:>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 93.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 (75 states)
4 :>1:r1=1; 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;
3 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
1522 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
1271 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
1222 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
3372 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
4868 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
10497 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
14109 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
374988:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
1752 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
54421 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
154454:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
44539 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
12741 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
148437:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
28854 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
36122 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
522725:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
37325 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
1233824:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
100784:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
190661:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
1970428:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
889865:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
745833:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
82341 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
1098275:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
2773030:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
609448:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
2311127:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
3663616:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
601652:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
244983:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
2245141:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
2358461:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
4694392:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
1895558:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
193465:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
3751317:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
1485387:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
378309:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
962528:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
557888:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
5621908:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
2631680:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
853224:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
3522363:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
3989109:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
2860203:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
2423151:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
4500014:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
3723937:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
2986307:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
3995271:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
315615:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
1156108:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
13488347:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
5248885:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
18941149:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
16729590:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
5208533:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
10199606:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
3309564:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
3059089:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
1494734:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
2051228:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
17081029:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
19371952:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
1436354:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
12668656:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
34099378:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
21062866:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
59478609:>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=a2812688a109c131b01004a694cfdd81
Cycle=LwSyncdRR Fre SyncsWW Rfe DpdR Fre SyncsWW Rfe
Relax bcssww002 No BCSyncsWW
Safe=Fre LwSyncdRR DpdR
Time bcssww002 92.55
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (17 states)
7 :>0:r3=1; 2:r1=2; x=2; y=2;
35 :>0:r3=0; 2:r1=1; x=2; y=2;
305903:>0:r3=1; 2:r1=0; x=1; y=2;
3035475:>0:r3=1; 2:r1=2; x=1; y=2;
1892424:>0:r3=2; 2:r1=1; x=1; y=2;
7019638:>0:r3=2; 2:r1=1; x=2; y=2;
183730:>0:r3=1; 2:r1=1; x=2; y=2;
17220800:>0:r3=1; 2:r1=0; x=2; y=2;
17639770:>0:r3=0; 2:r1=1; x=1; y=2;
177898:>0:r3=2; 2:r1=0; x=1; y=2;
1590815:>0:r3=1; 2:r1=1; x=1; y=2;
41689531:>0:r3=0; 2:r1=2; x=1; y=2;
87463622:>0:r3=2; 2:r1=2; x=1; y=2;
53341853:>0:r3=0; 2:r1=0; x=2; y=2;
71557768:>0:r3=0; 2:r1=0; x=1; y=2;
36138739:>0:r3=2; 2:r1=2; x=2; y=2;
60741992:>0:r3=2; 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 77.03
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
125684:>0:r3=1; 2:r1=1; x=2; y=2;
6253802:>0:r3=2; 2:r1=1; x=2; y=2;
3819166:>0:r3=2; 2:r1=1; x=1; y=2;
725362:>0:r3=2; 2:r1=0; x=1; y=2;
16538582:>0:r3=0; 2:r1=1; x=1; y=2;
448619:>0:r3=1; 2:r1=0; x=1; y=2;
30400537:>0:r3=2; 2:r1=2; x=2; y=2;
17327418:>0:r3=1; 2:r1=0; x=2; y=2;
2087078:>0:r3=1; 2:r1=1; x=1; y=2;
3184265:>0:r3=1; 2:r1=2; x=1; y=2;
38482395:>0:r3=0; 2:r1=2; x=1; y=2;
42453578:>0:r3=0; 2:r1=0; x=2; y=2;
90898823:>0:r3=2; 2:r1=2; x=1; y=2;
85932267:>0:r3=0; 2:r1=0; x=1; y=2;
61322424:>0:r3=2; 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=4a84f5a0d5b5b42156717d2ee2b4312f
Cycle=SyncdRW Wse SyncdWR Fre SyncsWW Rfe
Relax bcssww004 No BCSyncsWW
Safe=Fre Wse SyncdWR SyncdRW
Time bcssww004 76.46
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (16 states)
2 :>0:r3=0; 2:r1=1; x=2; y=2;
184154:>0:r3=1; 2:r1=1; x=2; y=2;
412675:>0:r3=2; 2:r1=0; x=1; y=2;
7431665:>0:r3=2; 2:r1=1; x=2; y=2;
3993942:>0:r3=2; 2:r1=1; x=1; y=2;
516916:>0:r3=1; 2:r1=0; x=1; y=2;
31249075:>0:r3=2; 2:r1=2; x=2; y=2;
49026772:>0:r3=0; 2:r1=0; x=2; y=2;
78450756:>0:r3=0; 2:r1=0; x=1; y=2;
2323080:>0:r3=1; 2:r1=1; x=1; y=2;
16866611:>0:r3=0; 2:r1=1; x=1; y=2;
62243427:>0:r3=2; 2:r1=0; x=2; y=2;
3464798:>0:r3=1; 2:r1=2; x=1; y=2;
18395112:>0:r3=1; 2:r1=0; x=2; y=2;
36888670:>0:r3=0; 2:r1=2; x=1; y=2;
88552345:>0:r3=2; 2:r1=2; 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 75.31
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (17 states)
38 :>0:r3=1; 2:r1=2; 2:r4=0; y=2;
51 :>0:r3=0; 2:r1=1; 2:r4=0; y=2;
319925:>0:r3=1; 2:r1=0; 2:r4=1; y=2;
306269:>0:r3=1; 2:r1=1; 2:r4=0; y=2;
95445 :>0:r3=2; 2:r1=0; 2:r4=1; y=2;
847246:>0:r3=2; 2:r1=1; 2:r4=1; y=2;
3713558:>0:r3=1; 2:r1=2; 2:r4=1; y=2;
1336681:>0:r3=1; 2:r1=1; 2:r4=1; y=2;
7605910:>0:r3=2; 2:r1=1; 2:r4=0; y=2;
17557892:>0:r3=1; 2:r1=0; 2:r4=0; y=2;
17753807:>0:r3=0; 2:r1=1; 2:r4=1; y=2;
60786180:>0:r3=2; 2:r1=0; 2:r4=0; y=2;
43017802:>0:r3=2; 2:r1=2; 2:r4=0; y=2;
72466459:>0:r3=0; 2:r1=0; 2:r4=1; y=2;
54625111:>0:r3=0; 2:r1=0; 2:r4=0; y=2;
80663435:>0:r3=2; 2:r1=2; 2:r4=1; y=2;
38904191:>0:r3=0; 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 77.99
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (17 states)
2 :>0:r3=0; 2:r1=1; 2:r3=0; y=2;
3 :>0:r3=1; 2:r1=2; 2:r3=0; y=2;
354459:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
256903:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
3543315:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
2304790:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
3028612:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
244752:>0:r3=1; 2:r1=1; 2:r3=0; y=2;
8128461:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
18509579:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
84183902:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
77740492:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
16992629:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
51043565:>0:r3=0; 2:r1=0; 2:r3=0; y=2;
36927653:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
35720558:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
61020325:>0:r3=2; 2:r1=0; 2:r3=0; 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 79.70
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (17 states)
23 :>0:r3=0; 2:r1=1; 2:r3=0; y=2;
23 :>0:r3=1; 2:r1=2; 2:r3=0; y=2;
216527:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
280575:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
294861:>0:r3=1; 2:r1=1; 2:r3=0; y=2;
8635797:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
37444788:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
15980776:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
76554853:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
2311553:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
61433802:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
2618816:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
52954472:>0:r3=0; 2:r1=0; 2:r3=0; y=2;
38014087:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
17690654:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
82078850:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
3489543:>0:r3=1; 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=d19882d97477fc15c9e4fbc588dc8a96
Cycle=LwSyncdRR Fre SyncdWR Fre SyncsWW Rfe
Relax bcssww008 No BCSyncsWW
Safe=Fre SyncdWR LwSyncdRR
Time bcssww008 79.07
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1395 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
2165 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1818 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2087 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
976 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
8412 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1095 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
676418:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
144237:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
702931:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1238768:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
723840:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1626158:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
220642:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1677157:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
270123:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
2454983:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
4068421:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
345717:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2750178:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
146283:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2479311:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1293398:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
2676568:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
2656705:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
718048:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
373424:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
336093:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
57487 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
75548 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
792333:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
4000993:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
484328:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
2320265:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
778996:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
19769282:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
2146020:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
4476097:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
6309507:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1291787:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1137227:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
16944348:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
1307565:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1991122:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
831518:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
2133574:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
256588:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
4488003:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
40689 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
217634:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
57303 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
4549019:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
339541:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
4700707:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
16830041:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
4371494:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
308785:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
482649:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
774142:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
2389676:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
4417626:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
19441100:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
6201434:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
16493969:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1070202:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
13668164:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
2025025:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
16934131:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
13589702:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
32453819:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
2497760:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
56955449:>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 92.39
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (75 states)
1 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
1 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
2 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
1150 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
1090 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
2052 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1302 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
2196 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
20244 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
40775 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
27441 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1091 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
7819 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
334353:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
268427:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
325914:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
960921:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
212137:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
604556:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
243690:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
70765 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
600019:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
706102:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
242896:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1268247:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
320246:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
713728:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
284629:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1738788:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
195562:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1901213:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1168616:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
4170003:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
4433801:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2751125:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
1215555:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1705388:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
3037952:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
2748487:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
3708956:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
120488:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1666500:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
326605:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
258440:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
4308355:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
3262256:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
740531:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
21014485:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
735172:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
17112592:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
3672632:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
2059225:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
19673257:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
5970418:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
852990:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
33857948:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
757804:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
13644199:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
767608:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
4294732:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
2178253:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
112910:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
13139865:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1297047:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
3211860:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
2004295:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
3968678:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
16421327:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
16300624:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
5279919:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
2564234:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1544939:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
3985097:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
58771793:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
18085682:>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=fdf7665f1e0ce0f0c6d4d353ee548d9e
Cycle=LwSyncdRR Fre SyncsWW Rfe SyncdRR Fre SyncsWW Rfe
Relax bcssww010 No BCSyncsWW
Safe=Fre SyncdRR LwSyncdRR
Time bcssww010 92.51
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (77 states)
2 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
2 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
5 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
6 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
2 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1653 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
3150 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1445 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2745 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1407 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1687 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
24399 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
11233 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
23591 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
444219:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
114387:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
921619:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
240794:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
119360:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
490903:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
209734:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
648031:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1004097:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
311392:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2326297:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
248448:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
252105:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
818250:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
685793:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1608577:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
208446:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1715608:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
302021:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1186604:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
10591 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
3385178:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
841675:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
2711234:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
3467788:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
799836:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
699178:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
682203:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
4326273:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
3748630:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
2552513:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
2901683:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
226585:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1276039:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
71881 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1359204:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
3845061:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
4348993:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
5325117:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1997506:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1751396:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
763427:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
4131280:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
4121166:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1410407:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
15548886:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
4184066:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
4292976:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1802702:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
13207436:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
16042369:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
2346346:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
293130:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
5642238:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
2072262:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
17344184:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
17218426:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
32853206:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
2901723:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
13093789:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
20459681:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
19941612:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
60072112:>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=7c8f7188794f6e0c8b799c86369a2299
Cycle=LwSyncdRR Fre SyncsWW Rfe LwSyncdRR Fre SyncsWW Rfe
Relax bcssww011 No BCSyncsWW
Safe=Fre LwSyncdRR
Time bcssww011 92.32
$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: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 32 */
GCCOPTS="-Wall -std=gnu99 -O -pthread"
LITMUSOPTS=
Thu Dec 24 10:26:23 GMT 2009