Wed Dec 30 17:21:03 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)
3 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
6 :>1:r1=1; 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;
1341 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
1591 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
1376 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
4704 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
4390 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
10665 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
6222 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
4440 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
39536 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
1438 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
3339 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
60751 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
44369 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
40079 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
28649 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
23529 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
5723 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
545116:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
89403 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
718047:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
1397025:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
971628:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
941887:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
632890:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
2742241:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
3871855:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
2232915:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
94354 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
771308:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
88620 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
1390434:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
211032:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
120204:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
3090230:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
678649:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
683295:>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
2540011:>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
1401731:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
2021769:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
4824533:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
126823:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
160347:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
1450140:>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
3042902:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
4644009:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
14154069:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
2532320:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
1162449:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
5188095:>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
4258020:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
2160121:>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
2623658:>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
3106502:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
5239708:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
3913371:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
2563480:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
1241277:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
3682672:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
4009250:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
4775027:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
4251088:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
10643291:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
19016664:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
2536747:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
10606790:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
13889943:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
18840880:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
38278076:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
3301346:>1:r1=2; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
19297494:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
19718315:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
57243795:>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 100.29
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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=1; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
1 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
1 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
1 :>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
1209 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
2240 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
1223 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
1047 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
1170 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
14585 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
15052 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
7649 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
21238 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
44453 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
2521 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
408631:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
25607 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
154097:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
665356:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
92282 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
271879:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
192657:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
375845:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
119464:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
45828 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
3294641:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
269142:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
708194:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
1169443:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
377710:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
3686794:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
1446681:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
846099:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
5080956:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
1115238:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
713376:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
251517:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
2322874:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
614297:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
4219640:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
820151:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
6038605:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
4594612:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
1824453:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
2046541:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
2566761:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
64502 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
2944991:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
1357645:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
4950989:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
3798734:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
2910996:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
10822520:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
2043730:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
2365188:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
3827156:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
1292220:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
4897732:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
1238191:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
2036422:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
816424:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
13376424:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
13240900:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
18012104:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
2424343:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
3216786:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
16834284:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
2955114:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
17785900:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
3832166:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
21376378:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
57784540:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
35179629:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
19162007:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
587289:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
2392934:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=c19feeb22b3e4fe95d3ae9cd399e4667
Cycle=SyncdRR Fre SyncsWW Rfe DpdR Fre SyncsWW Rfe
Relax bcssww001 No BCSyncsWW
Safe=Fre SyncdRR DpdR
Time bcssww001 101.64
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (74 states)
2 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
2 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
1426 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
1404 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
2573 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
1449 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
2310 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
1009 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
9400 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
45426 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
18581 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
54387 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
45393 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
161927:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
1347529:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
757274:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
178122:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
38568 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
1195404:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
28918 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
573622:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
217016:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
1455888:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
350114:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
15654 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
652001:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
250667:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
2375141:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
89193 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
691279:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
107107:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
369278:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
2008911:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
910118:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
2192869:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
859483:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
2549462:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
784672:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
1603455:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
4118654:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
689458:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
2308520:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
1154696:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
1318695:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
3429295:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
5209189:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
3699384:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
4319702:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
1693657:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
4854575:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
243404:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
2208961:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
2428831:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
3354856:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
3741335:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
2443055:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
3053549:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
5047268:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
20992684:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
2866741:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
881644:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
5923170:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
3155508:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
19427507:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
12801865:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
18271212:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
34422635:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
12590017:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
58477250:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
4006912:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
17824236:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
3868958:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
16420812:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
10804731:>1:r1=0; 1:r4=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: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 100.81
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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;
23 :>0:r3=0; 2:r1=1; x=2; y=2;
266666:>0:r3=1; 2:r1=1; x=2; y=2;
144664:>0:r3=2; 2:r1=0; x=1; y=2;
217947:>0:r3=1; 2:r1=0; x=1; y=2;
2683194:>0:r3=1; 2:r1=2; x=1; y=2;
1547788:>0:r3=2; 2:r1=1; x=1; y=2;
5538837:>0:r3=2; 2:r1=1; x=2; y=2;
1738992:>0:r3=1; 2:r1=1; x=1; y=2;
16902138:>0:r3=1; 2:r1=0; x=2; y=2;
16414343:>0:r3=0; 2:r1=1; x=1; y=2;
55813489:>0:r3=0; 2:r1=0; x=2; y=2;
87740259:>0:r3=2; 2:r1=2; x=1; y=2;
40405133:>0:r3=0; 2:r1=2; x=1; y=2;
36316913:>0:r3=2; 2:r1=2; x=2; y=2;
60001071:>0:r3=2; 2:r1=0; x=2; y=2;
74268529:>0:r3=0; 2:r1=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2) is NOT validated
Hash=316a93ca86d6e131419704cdf84a4e06
Cycle=DpdW Wse SyncdWR Fre SyncsWW Rfe
Relax bcssww003 No BCSyncsWW
Safe=Fre Wse SyncdWR DpdW
Time bcssww003 65.04
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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;
901390:>0:r3=2; 2:r1=0; x=1; y=2;
113737:>0:r3=1; 2:r1=1; x=2; y=2;
720022:>0:r3=1; 2:r1=0; x=1; y=2;
4094740:>0:r3=1; 2:r1=2; x=1; y=2;
3986478:>0:r3=2; 2:r1=1; x=1; y=2;
7234648:>0:r3=2; 2:r1=1; x=2; y=2;
2383985:>0:r3=1; 2:r1=1; x=1; y=2;
16987823:>0:r3=1; 2:r1=0; x=2; y=2;
16207830:>0:r3=0; 2:r1=1; x=1; y=2;
88395665:>0:r3=0; 2:r1=0; x=1; y=2;
90562068:>0:r3=2; 2:r1=2; x=1; y=2;
62191538:>0:r3=2; 2:r1=0; x=2; y=2;
37044477:>0:r3=0; 2:r1=2; x=1; y=2;
29478163:>0:r3=2; 2:r1=2; x=2; y=2;
39697435:>0:r3=0; 2:r1=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2) is NOT validated
Hash=4a84f5a0d5b5b42156717d2ee2b4312f
Cycle=SyncdRW Wse SyncdWR Fre SyncsWW Rfe
Relax bcssww004 No BCSyncsWW
Safe=Fre Wse SyncdWR SyncdRW
Time bcssww004 65.21
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (15 states)
428473:>0:r3=1; 2:r1=0; x=1; y=2;
2893680:>0:r3=1; 2:r1=2; x=1; y=2;
398089:>0:r3=2; 2:r1=0; x=1; y=2;
201792:>0:r3=1; 2:r1=1; x=2; y=2;
6026589:>0:r3=2; 2:r1=1; x=2; y=2;
2334712:>0:r3=1; 2:r1=1; x=1; y=2;
3402951:>0:r3=2; 2:r1=1; x=1; y=2;
16853920:>0:r3=0; 2:r1=1; x=1; y=2;
62549740:>0:r3=2; 2:r1=0; x=2; y=2;
80861294:>0:r3=0; 2:r1=0; x=1; y=2;
89076728:>0:r3=2; 2:r1=2; x=1; y=2;
18052607:>0:r3=1; 2:r1=0; x=2; y=2;
32349175:>0:r3=2; 2:r1=2; x=2; y=2;
46364202:>0:r3=0; 2:r1=0; x=2; y=2;
38206048:>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 64.23
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
45 :>0:r3=0; 2:r1=1; 2:r4=0; y=2;
23 :>0:r3=1; 2:r1=2; 2:r4=0; y=2;
86989 :>0:r3=2; 2:r1=0; 2:r4=1; y=2;
284532:>0:r3=1; 2:r1=0; 2:r4=1; y=2;
290853:>0:r3=1; 2:r1=1; 2:r4=0; y=2;
1351774:>0:r3=1; 2:r1=1; 2:r4=1; y=2;
2631754:>0:r3=1; 2:r1=2; 2:r4=1; y=2;
8065261:>0:r3=2; 2:r1=1; 2:r4=0; y=2;
996776:>0:r3=2; 2:r1=1; 2:r4=1; y=2;
16799241:>0:r3=1; 2:r1=0; 2:r4=0; y=2;
61975681:>0:r3=2; 2:r1=0; 2:r4=0; y=2;
70530604:>0:r3=0; 2:r1=0; 2:r4=1; y=2;
42074129:>0:r3=0; 2:r1=2; 2:r4=1; y=2;
83991446:>0:r3=2; 2:r1=2; 2:r4=1; y=2;
53215467:>0:r3=0; 2:r1=0; 2:r4=0; y=2;
17659590:>0:r3=0; 2:r1=1; 2:r4=1; y=2;
40045835:>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 63.60
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (16 states)
2 :>0:r3=0; 2:r1=1; 2:r3=0; y=2;
194610:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
217765:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
2548306:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
231510:>0:r3=1; 2:r1=1; 2:r3=0; y=2;
1885529:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
2813126:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
6486421:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
61571669:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
16855764:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
84705872:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
17184063:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
75366936:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
37606723:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
52364428:>0:r3=0; 2:r1=0; 2:r3=0; y=2;
39967276:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=66d340e023bd1d1ae19ed5903eb5d2ea
Cycle=SyncdRR Fre SyncdWR Fre SyncsWW Rfe
Relax bcssww007 No BCSyncsWW
Safe=Fre SyncdWR SyncdRR
Time bcssww007 62.98
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
37 :>0:r3=1; 2:r1=2; 2:r3=0; y=2;
77 :>0:r3=0; 2:r1=1; 2:r3=0; y=2;
2927622:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
236297:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
284669:>0:r3=1; 2:r1=1; 2:r3=0; y=2;
260294:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
8358445:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
2158038:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
2704890:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
17348481:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
16736105:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
75427976:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
62390022:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
37273292:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
52305526:>0:r3=0; 2:r1=0; 2:r3=0; y=2;
38572868:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
83015361:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=d19882d97477fc15c9e4fbc588dc8a96
Cycle=LwSyncdRR Fre SyncdWR Fre SyncsWW Rfe
Relax bcssww008 No BCSyncsWW
Safe=Fre SyncdWR LwSyncdRR
Time bcssww008 63.84
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (74 states)
1 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
1 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
2117 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1405 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
916 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
1671 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1342 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
64600 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
464818:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
7992 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
66525 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
77198 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1091038:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1053 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
391190:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
359372:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
290465:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
232843:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
68794 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
805387:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
156118:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1340276:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
339837:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
830807:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
2183161:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2579680:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
623471:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
262120:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
2115712:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
161247:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1082210:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
1687610:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1928047:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2149630:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
758801:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
644777:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
2183230:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
456490:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
1234612:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
2629584:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
4234108:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
4192546:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
2093774:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1173669:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
1564023:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
792697:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
2417190:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
751830:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
2709479:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
2302782:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
344316:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
3936131:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
360692:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
4108993:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
6350565:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
4664126:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
4369675:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
31752889:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
4472771:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1358150:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
6331187:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
2461025:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
4396141:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
14189266:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
394161:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
58236084:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
19755523:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
13655524:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
19703098:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
939173:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
16167051:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
17617717:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
16792990:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
16134506:>1:r1=0; 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=ac99317f895df8ed08197fb9ed0e136a
Cycle=SyncdRR Fre SyncsWW Rfe SyncdRR Fre SyncsWW Rfe
Relax bcssww009 No BCSyncsWW
Safe=Fre SyncdRR
Time bcssww009 100.28
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww010
"LwSyncdRR Fre SyncsWW Rfe SyncdRR Fre SyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | lwsync ;
sync | lwz r3,0(r4) | sync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 30,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 30,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww010 Allowed
Histogram (75 states)
1 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
1 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
2 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
1866 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
2826 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
11023 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1644 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
35598 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
2524 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1115 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1041 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
161178:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
244470:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
48435 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
348596:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
56500 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
914434:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
506316:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
234546:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
323715:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1180774:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
317134:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1296539:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
1359626:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
2726120:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
339901:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
684335:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1353014:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
2320323:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
368854:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1427783:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1443346:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
651164:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
935909:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
2263233:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2758503:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
2503491:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
2217059:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
260457:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1631391:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
4703569:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
747891:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
2475383:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
80205 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
858065:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
790461:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
162393:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
2653519:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
4825096:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
3951057:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
4544604:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
6383636:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
2111303:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
4564080:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
58980602:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
739646:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
2323900:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
6021293:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
825952:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
2338887:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
16867959:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
4369554:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1851511:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
303497:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
4285993:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
4410314:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
31333567:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
2357477:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
15391793:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
16694115:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
15104166:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
13207195:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
18818845:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
14255373:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
19732312:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1: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 100.45
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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=0; 3:r1=2; 3:r3=1; 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=1; 3:r3=0; x=2; y=2;
3 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
1178 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
2426 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1566 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
2252 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1534 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1065 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
1334319:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
80900 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
20559 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
308828:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
15181 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2230101:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
340188:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
31506 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
232350:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
157943:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
46939 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
580248:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
380486:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
648847:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
3044375:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
717667:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1393888:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1229195:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
2324735:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
924276:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
678239:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
2622854:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
247987:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
3962173:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
2728233:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1656050:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1770053:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
2583427:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
4249589:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
4434411:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
937764:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
254507:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
485995:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
6129996:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
350484:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
946663:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
4380269:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1340176:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
165367:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2295817:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
311649:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
304344:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
4126220:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
4247193:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
13539749:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
16533634:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
1429860:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
4206236:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
2183656:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
4346769:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
3080360:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
2473278:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
1176280:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
1890725:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
856228:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
30892865:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
19646060:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
16558909:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
16205860:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
920837:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
2291823:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
13232834:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
6146406:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
15142167:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
19779518:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
60203927:>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 100.67
$Revision: 3163 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 2000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 20000
#endif
#ifndef N_EXE
#define N_EXE (32 < N ? 1 : 32 / N)
#endif
/* gcc options: -Wall -std=gnu99 -O -pthread */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: true */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 32 */
GCCOPTS="-Wall -std=gnu99 -O -pthread"
LITMUSOPTS=
Wed Dec 30 17:37:33 GMT 2009