Mon Dec 28 14:33:10 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 (75 states)
1 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
1 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
1 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
1458 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
1199 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
1682 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
3018 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
3096 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
4295 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
1464 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
9592 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
3556 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
5711 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
3902 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
33960 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
87160 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
85338 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
202129:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
153604:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
121877:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
40474 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
1345905:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
950729:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
358356:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
2149549:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
59276 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
2593024:>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
106365:>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
26127 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
134964:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
5291707:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
1141051:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
545662:>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
37200 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
645816:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
446926:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
2218392:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
22151 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
1372647:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
2032615:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
1360298:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
886733:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
10415743:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
4899177:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
1421357:>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
3530867:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
1199228:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
2824610:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
3163659:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
3221010:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
2344086:>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
2399377:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
4285217:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
735054:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
4637689:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
2304684:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
4149065:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
2494763:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
4780759:>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
680975:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
3447266:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
10579662:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
4536857:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
2040749:>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
19873414:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
14141469:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
38796524:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
57380711:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
20190094:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
4363712:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
14377122:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
3843072:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
19458976:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
3433754:>1:r1=2; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
19560287:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; 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 102.22
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (76 states)
1 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
4 :>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;
5 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
1957 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
1741 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
1114 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
16490 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
3029 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
1425 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
3125 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
25811 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
68058 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
10406 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
50218 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
19828 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
1164852:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
273166:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
122095:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
144646:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
422359:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
77475 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
2212207:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
221457:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
701821:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
644412:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
1247597:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
266588:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
1022508:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
209126:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
3651055:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
3827998:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
1964400:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
678723:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
2275420:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
5307095:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
937731:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
1431735:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
1366952:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
1257310:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
4924391:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
3082003:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
2148490:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
437119:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
683281:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
939508:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
4667436:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
421809:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
2895444:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
719901:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
2465713:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
26038 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
280867:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
6321637:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
1753819:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
3855587:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
2657377:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
1479652:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
4123496:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
2961269:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
2490588:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
2429728:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
3686529:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
13244505:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
18130973:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
4291397:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
5251287:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
2773561:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
10670127:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
17389995:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
18786397:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
16691639:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
13310712:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
33972096:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
21022522:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
57381166:>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 100.07
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (77 states)
2 :>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;
3 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
2 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
3 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
1083 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
1526 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
2786 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
20052 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
1440 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
1665 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
14601 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
2983 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
44745 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
19446 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
38246 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
820119:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
48591 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
63534 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
365977:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
1275264:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
917776:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
1441607:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
182451:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
2457366:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
2126857:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
2392553:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
93003 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
694001:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
2620124:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
4021417:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
3155794:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
492268:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
1716331:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
3193616:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
570546:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
2932537:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
1127431:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
111805:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
664074:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
3506843:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
248328:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
3122907:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
225181:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
686925:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
2018068:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
928167:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
2267883:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
1553050:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
28171 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
5905702:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
3761806:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
2335696:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
247181:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
3510795:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
2145992:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
4125634:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
1150341:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
187273:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
12740686:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
370817:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
1227846:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
4661824:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
3786947:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
34540069:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
12831404:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
3910098:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
5194085:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
377708:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
18013941:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
16713956:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
19742748:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
5059609:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
10758830:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
18487835:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
21242226:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
58749802:>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 99.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
14 :>0:r3=1; 2:r1=2; x=2; y=2;
58 :>0:r3=0; 2:r1=1; x=2; y=2;
228404:>0:r3=2; 2:r1=0; x=1; y=2;
613430:>0:r3=1; 2:r1=0; x=1; y=2;
2223103:>0:r3=2; 2:r1=1; x=1; y=2;
218936:>0:r3=1; 2:r1=1; x=2; y=2;
4032821:>0:r3=1; 2:r1=2; x=1; y=2;
8303287:>0:r3=2; 2:r1=1; x=2; y=2;
1778278:>0:r3=1; 2:r1=1; x=1; y=2;
15890015:>0:r3=0; 2:r1=1; x=1; y=2;
60881266:>0:r3=2; 2:r1=0; x=2; y=2;
75984113:>0:r3=0; 2:r1=0; x=1; y=2;
34572749:>0:r3=2; 2:r1=2; x=2; y=2;
53876966:>0:r3=0; 2:r1=0; x=2; y=2;
86783732:>0:r3=2; 2:r1=2; x=1; y=2;
17651638:>0:r3=1; 2:r1=0; x=2; y=2;
36961190:>0:r3=0; 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=316a93ca86d6e131419704cdf84a4e06
Cycle=DpdW Wse SyncdWR Fre SyncsWW Rfe
Relax bcssww003 No BCSyncsWW
Safe=Fre Wse SyncdWR DpdW
Time bcssww003 61.62
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (16 states)
1 :>0:r3=0; 2:r1=1; x=2; y=2;
132228:>0:r3=1; 2:r1=1; x=2; y=2;
3891374:>0:r3=2; 2:r1=1; x=1; y=2;
6528712:>0:r3=2; 2:r1=1; x=2; y=2;
40004530:>0:r3=0; 2:r1=0; x=2; y=2;
29450087:>0:r3=2; 2:r1=2; x=2; y=2;
2406808:>0:r3=1; 2:r1=1; x=1; y=2;
802731:>0:r3=2; 2:r1=0; x=1; y=2;
613171:>0:r3=1; 2:r1=0; x=1; y=2;
3442402:>0:r3=1; 2:r1=2; x=1; y=2;
17102194:>0:r3=0; 2:r1=1; x=1; y=2;
88343673:>0:r3=0; 2:r1=0; x=1; y=2;
17942845:>0:r3=1; 2:r1=0; x=2; y=2;
91158939:>0:r3=2; 2:r1=2; x=1; y=2;
60998990:>0:r3=2; 2:r1=0; x=2; y=2;
37181315:>0:r3=0; 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=4a84f5a0d5b5b42156717d2ee2b4312f
Cycle=SyncdRW Wse SyncdWR Fre SyncsWW Rfe
Relax bcssww004 No BCSyncsWW
Safe=Fre Wse SyncdWR SyncdRW
Time bcssww004 63.82
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (16 states)
1 :>0:r3=0; 2:r1=1; x=2; y=2;
475873:>0:r3=2; 2:r1=0; x=1; y=2;
729697:>0:r3=1; 2:r1=0; x=1; y=2;
4670334:>0:r3=2; 2:r1=1; x=1; y=2;
190350:>0:r3=1; 2:r1=1; x=2; y=2;
2734614:>0:r3=1; 2:r1=1; x=1; y=2;
16773816:>0:r3=0; 2:r1=1; x=1; y=2;
3527080:>0:r3=1; 2:r1=2; x=1; y=2;
7225345:>0:r3=2; 2:r1=1; x=2; y=2;
18892497:>0:r3=1; 2:r1=0; x=2; y=2;
30784120:>0:r3=2; 2:r1=2; x=2; y=2;
46301284:>0:r3=0; 2:r1=0; x=2; y=2;
81623384:>0:r3=0; 2:r1=0; x=1; y=2;
62147486:>0:r3=2; 2:r1=0; x=2; y=2;
87959404:>0:r3=2; 2:r1=2; x=1; y=2;
35964715:>0:r3=0; 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 61.58
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
20 :>0:r3=0; 2:r1=1; 2:r4=0; y=2;
10 :>0:r3=1; 2:r1=2; 2:r4=0; y=2;
67501 :>0:r3=2; 2:r1=0; 2:r4=1; y=2;
300302:>0:r3=1; 2:r1=1; 2:r4=0; y=2;
209502:>0:r3=1; 2:r1=0; 2:r4=1; y=2;
1181705:>0:r3=1; 2:r1=1; 2:r4=1; y=2;
2166191:>0:r3=1; 2:r1=2; 2:r4=1; y=2;
6849751:>0:r3=2; 2:r1=1; 2:r4=0; y=2;
16497986:>0:r3=1; 2:r1=0; 2:r4=0; y=2;
849984:>0:r3=2; 2:r1=1; 2:r4=1; y=2;
61657851:>0:r3=2; 2:r1=0; 2:r4=0; y=2;
70197655:>0:r3=0; 2:r1=0; 2:r4=1; y=2;
83654696:>0:r3=2; 2:r1=2; 2:r4=1; y=2;
43484185:>0:r3=0; 2:r1=2; 2:r4=1; y=2;
54155646:>0:r3=0; 2:r1=0; 2:r4=0; y=2;
17425801:>0:r3=0; 2:r1=1; 2:r4=1; y=2;
41301214:>0:r3=2; 2:r1=2; 2:r4=0; 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 64.52
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
2 :>0:r3=1; 2:r1=2; 2:r3=0; y=2;
2 :>0:r3=0; 2:r1=1; 2:r3=0; y=2;
246556:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
303651:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
2773975:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
205316:>0:r3=1; 2:r1=1; 2:r3=0; y=2;
8008787:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
2167701:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
3259511:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
16345147:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
84716742:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
16959133:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
76290877:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
50918312:>0:r3=0; 2:r1=0; 2:r3=0; y=2;
38961990:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
36357243:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
62485055:>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 61.60
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
16 :>0:r3=1; 2:r1=2; 2:r3=0; y=2;
29 :>0:r3=0; 2:r1=1; 2:r3=0; y=2;
227293:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
206456:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
2997120:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
8133770:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
248855:>0:r3=1; 2:r1=1; 2:r3=0; y=2;
2574390:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
2094470:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
17672434:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
74932885:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
17462161:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
83676567:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
52359951:>0:r3=0; 2:r1=0; 2:r3=0; y=2;
38340901:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
37119722:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
61952980:>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=d19882d97477fc15c9e4fbc588dc8a96
Cycle=LwSyncdRR Fre SyncdWR Fre SyncsWW Rfe
Relax bcssww008 No BCSyncsWW
Safe=Fre SyncdWR LwSyncdRR
Time bcssww008 62.66
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1475 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1899 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
946 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
892 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
2408 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
42653 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
519662:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
64789 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
9322 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
525706:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
764912:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1182864:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
345720:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
260724:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
2540707:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
2343657:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
933441:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
691727:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
684646:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
753064:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
4077851:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1186105:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
1629917:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
416885:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
2372809:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
2309238:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
2249734:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
791095:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
379529:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
4458183:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
17396173:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1758692:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
68081 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1215266:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
276168:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
2258551:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
71233 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
2429715:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1388070:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1232813:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
4560091:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
961835:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1635 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
13682402:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
241209:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
6465204:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
157212:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
14106496:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
2199076:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
4281160:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1442537:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
349237:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
4336838:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
4683507:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
4753747:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
2281963:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
6525298:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
364138:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
336463:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
19195406:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
2222057:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
16050302:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
900103:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2287457:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2467635:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
161553:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
4693112:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
15793919:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
16454490:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
31400053:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
19123116:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
57883427:>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.41
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (76 states)
1 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
1 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
3 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
6 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
938 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
2299 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1248 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1597 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1843 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1365 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
33453 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
52814 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
437207:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
8868 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
952473:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
526497:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
154987:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
60729 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
921779:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
2088221:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
340327:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1283611:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
324781:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1186840:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
278462:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
150413:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
242776:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
369803:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
751302:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
874960:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
2134803:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
1169973:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
1436017:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
667920:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
251346:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
79039 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
2264111:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2756463:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
4405421:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1372137:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2322512:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
401934:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
3890725:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
2213380:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
332099:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
615091:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
911937:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1731838:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
4292687:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
2196752:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
6619253:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
4372337:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
853492:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
13215178:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
6167066:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
4354143:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1359191:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
4600537:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1531791:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
358729:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
16921543:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
2514664:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
4038691:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
2455725:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
15657960:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
19074202:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
4495772:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
17250629:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
2759839:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
2792580:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
15494597:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
2411149:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
14166915:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
19963278:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
31141702:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
58933248:>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.27
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (76 states)
1 :>1:r1=2; 1:r3=1; 3:r1=2; 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=1; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
6 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
1702 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
2414 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1735 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2362 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1189 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
1145 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
29661 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1219983:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
44857 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1346905:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
83394 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
9818 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
129419:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
202076:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
20448 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
222131:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
2271406:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
2800985:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1791494:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1325406:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
302328:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
345936:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
2246587:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
134077:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1834517:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2261760:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
414173:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
505565:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
851197:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
302489:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
231326:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
2342395:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
662404:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
720988:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
306281:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1372839:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
3099934:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
293855:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
5963187:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
629779:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
349320:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2511776:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
1224571:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
4269712:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
4223309:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
850167:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
2640110:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
863769:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1667183:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
4147372:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
4348066:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
5964508:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
13256153:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
3851683:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
2611689:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
864046:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
3062534:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
4264181:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
16677889:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
4428513:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
13674868:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
16498144:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
4141826:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
2198385:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1334009:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
839819:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
15035415:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
16266480:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
19858540:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
20005429:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
60464164:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
31276213:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; 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 102.08
$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=
Mon Dec 28 14:49:34 GMT 2009