Tue Dec 22 19:35: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 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 (77 states)
3 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
6 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
4 :>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;
3 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
1365 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
3897 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
3276 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
2283 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
4336 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
5339 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
1540 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
7740 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
1689 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
37612 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
4253 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
10234 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
42891 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
39567 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
98215 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
82447 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
26333 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
1285342:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
835938:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
2158095:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
3094123:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
4358027:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
679310:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
125108:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
1366317:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
2311479:>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
175157:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
2794085:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
714046:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
19732991:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
98640 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
111170:>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
4285338:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
172884:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
3748740:>1:r1=2; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
78635 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
1186910:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
4549096:>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
4863168:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
660380:>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
2439439:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
1382828:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
4897855:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
2264924:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
27472 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
3163825:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
523997:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
4144104:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
10617847:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
1991270:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
731692:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
2761932:>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
830058:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
3884904:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
1282890:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
19789217:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
10699374:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
4596168:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
2543197:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
40119524:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
1173354:>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
3519585:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
527456:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
19474496:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
19573426:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
3541967:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
4178419:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
14243692:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
14437309:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
2263739:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
1960632:>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
56655394:>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 96.60
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
3 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
9 :>1:r1=1; 1:r4=0; 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;
1719 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
2080 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
9375 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
1552 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
1392 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
3926 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
3398 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
28837 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
503908:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
17247 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
47554 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
1182794:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
141392:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
42496 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
123841:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
32620 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
531162:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
74704 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
196704:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
1294975:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
613384:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
752210:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
2277212:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
2867543:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
2713314:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
81481 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
2074151:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
320123:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
828334:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
1074433:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
578139:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
167382:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
1323241:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
14927 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
236255:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
2024660:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
274043:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
3701034:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
4106902:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
706567:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
2257679:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
895329:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
2423157:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
4597505:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
594406:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
2132167:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
3743636:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
3534868:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
1875058:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
16979271:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
13542861:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
2334012:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
1160280:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
2813974:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
3308123:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
2647956:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
4916178:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
390556:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
3769758:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
4494380:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
17641101:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
3441984:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
14006388:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
5878956:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
18648876:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
18731571:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
5131795:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
10359894:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
35456607:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
1466958:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
21433541:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
58414147:>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.99
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (77 states)
1 :>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
1 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
2 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
3 :>1:r1=1; 1:r4=0; 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;
1735 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
1939 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
3520 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
1381 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
13783 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
55817 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
1625 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
10639 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
384806:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
27308 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
46142 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
37320 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
113215:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
249482:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
195139:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
38240 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
826942:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
87896 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
4698 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
180686:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
2392898:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
2232689:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
1995284:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
876414:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
12984 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
149776:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
552405:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
611258:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
317335:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
1484628:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
4100571:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
1254581:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
159563:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
2719295:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
995469:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
719324:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
2442653:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
1188875:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
3061594:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
2856283:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
380602:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
590053:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
1127398:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
2464411:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
3685199:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
2598260:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
535256:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
4011504:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
3752446:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
5155888:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
1453933:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
17164070:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
5225040:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
2070204:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
4600867:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
3770535:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
4394007:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
1900910:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
13383603:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
16560606:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
18803106:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
12695234:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
34573844:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
3270214:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
5584506:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
10219699:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
2938172:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
3541189:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
19397133:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
1492523:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
20797750:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
59455634:>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.58
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
5 :>0:r3=1; 2:r1=2; x=2; y=2;
17 :>0:r3=0; 2:r1=1; x=2; y=2;
291686:>0:r3=1; 2:r1=0; x=1; y=2;
171467:>0:r3=2; 2:r1=0; x=1; y=2;
1812290:>0:r3=2; 2:r1=1; x=1; y=2;
3079323:>0:r3=1; 2:r1=2; x=1; y=2;
1395405:>0:r3=1; 2:r1=1; x=1; y=2;
160575:>0:r3=1; 2:r1=1; x=2; y=2;
7126108:>0:r3=2; 2:r1=1; x=2; y=2;
17838752:>0:r3=0; 2:r1=1; x=1; y=2;
53279123:>0:r3=0; 2:r1=0; x=2; y=2;
41323550:>0:r3=0; 2:r1=2; x=1; y=2;
17169009:>0:r3=1; 2:r1=0; x=2; y=2;
36317008:>0:r3=2; 2:r1=2; x=2; y=2;
87619904:>0:r3=2; 2:r1=2; x=1; y=2;
71655435:>0:r3=0; 2:r1=0; x=1; y=2;
60760343:>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 78.55
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
3176804:>0:r3=1; 2:r1=2; x=1; y=2;
143749:>0:r3=1; 2:r1=1; x=2; y=2;
457733:>0:r3=1; 2:r1=0; x=1; y=2;
728834:>0:r3=2; 2:r1=0; x=1; y=2;
2207555:>0:r3=1; 2:r1=1; x=1; y=2;
6327343:>0:r3=2; 2:r1=1; x=2; y=2;
3873194:>0:r3=2; 2:r1=1; x=1; y=2;
18041696:>0:r3=1; 2:r1=0; x=2; y=2;
17242297:>0:r3=0; 2:r1=1; x=1; y=2;
91228450:>0:r3=2; 2:r1=2; x=1; y=2;
42680558:>0:r3=0; 2:r1=0; x=2; y=2;
37732437:>0:r3=0; 2:r1=2; x=1; y=2;
29696590:>0:r3=2; 2:r1=2; x=2; y=2;
60671920:>0:r3=2; 2:r1=0; x=2; y=2;
85790840:>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=4a84f5a0d5b5b42156717d2ee2b4312f
Cycle=SyncdRW Wse SyncdWR Fre SyncsWW Rfe
Relax bcssww004 No BCSyncsWW
Safe=Fre Wse SyncdWR SyncdRW
Time bcssww004 77.52
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (17 states)
1 :>0:r3=1; 2:r1=2; x=2; y=2;
2 :>0:r3=0; 2:r1=1; x=2; y=2;
413121:>0:r3=2; 2:r1=0; x=1; y=2;
526708:>0:r3=1; 2:r1=0; x=1; y=2;
174106:>0:r3=1; 2:r1=1; x=2; y=2;
3694366:>0:r3=1; 2:r1=2; x=1; y=2;
7707715:>0:r3=2; 2:r1=1; x=2; y=2;
2339683:>0:r3=1; 2:r1=1; x=1; y=2;
3915511:>0:r3=2; 2:r1=1; x=1; y=2;
78720151:>0:r3=0; 2:r1=0; x=1; y=2;
31073256:>0:r3=2; 2:r1=2; x=2; y=2;
62179179:>0:r3=2; 2:r1=0; x=2; y=2;
16777324:>0:r3=0; 2:r1=1; x=1; y=2;
49360777:>0:r3=0; 2:r1=0; x=2; y=2;
18156138:>0:r3=1; 2:r1=0; x=2; y=2;
36520853:>0:r3=0; 2:r1=2; x=1; y=2;
88441109:>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 76.88
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
35 :>0:r3=1; 2:r1=2; 2:r4=0; y=2;
42 :>0:r3=0; 2:r1=1; 2:r4=0; y=2;
282654:>0:r3=1; 2:r1=0; 2:r4=1; y=2;
3796440:>0:r3=1; 2:r1=2; 2:r4=1; y=2;
90440 :>0:r3=2; 2:r1=0; 2:r4=1; y=2;
291934:>0:r3=1; 2:r1=1; 2:r4=0; y=2;
756011:>0:r3=2; 2:r1=1; 2:r4=1; y=2;
1267210:>0:r3=1; 2:r1=1; 2:r4=1; y=2;
16766577:>0:r3=1; 2:r1=0; 2:r4=0; y=2;
7557049:>0:r3=2; 2:r1=1; 2:r4=0; y=2;
72614181:>0:r3=0; 2:r1=0; 2:r4=1; y=2;
80335101:>0:r3=2; 2:r1=2; 2:r4=1; y=2;
16816897:>0:r3=0; 2:r1=1; 2:r4=1; y=2;
54852059:>0:r3=0; 2:r1=0; 2:r4=0; y=2;
43635953:>0:r3=2; 2:r1=2; 2:r4=0; y=2;
61335226:>0:r3=2; 2:r1=0; 2:r4=0; y=2;
39602191:>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 80.29
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
3 :>0:r3=1; 2:r1=2; 2:r3=0; y=2;
2 :>0:r3=0; 2:r1=1; 2:r3=0; y=2;
226125:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
2897884:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
266295:>0:r3=1; 2:r1=1; 2:r3=0; y=2;
3233892:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
283236:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
7495767:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
2219116:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
16751674:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
36520589:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
18053288:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
37969487:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
60928019:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
83951739:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
77228932:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
51973952:>0:r3=0; 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.02
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
20 :>0:r3=1; 2:r1=2; 2:r3=0; y=2;
54 :>0:r3=0; 2:r1=1; 2:r3=0; y=2;
307852:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
3423776:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
245417:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
2249412:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
280623:>0:r3=1; 2:r1=1; 2:r3=0; y=2;
2799616:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
18445479:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
76607179:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
8864321:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
60995236:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
16921608:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
82574396:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
52588449:>0:r3=0; 2:r1=0; 2:r3=0; y=2;
36985185:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
36711377:>0:r3=2; 2:r1=2; 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 78.00
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1190 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1562 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2034 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
7980 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2450 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1549 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
1298 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
904484:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
949766:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
50842 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
32445 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
339749:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
336687:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
50846 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
134788:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
802581:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
276159:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
296760:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1773193:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
336991:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
754550:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
326574:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
2585294:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
128346:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2105097:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2142826:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
218765:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
2860120:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
215106:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
74291 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
2098721:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1129822:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
556916:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
3652825:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
341806:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
590702:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
2388994:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
260461:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
289150:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
767203:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1199100:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
3802870:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1695198:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1656445:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
2681152:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
699556:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
2162762:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
764626:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1599506:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1328008:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
779201:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1289825:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
19988742:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
4133371:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
20326658:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
2703309:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
4493088:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
13637228:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
5839781:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
4158246:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
5978970:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
13854679:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
4442649:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
4169265:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
4209916:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
57726982:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
16660066:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
17199428:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
17345359:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
17442690:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
33287166:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
2953235:>1:r1=0; 1:r3=0; 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=ac99317f895df8ed08197fb9ed0e136a
Cycle=SyncdRR Fre SyncsWW Rfe SyncdRR Fre SyncsWW Rfe
Relax bcssww009 No BCSyncsWW
Safe=Fre SyncdRR
Time bcssww009 94.65
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/bcssww010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww010
"LwSyncdRR Fre SyncsWW Rfe SyncdRR Fre SyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | lwsync ;
sync | lwz r3,0(r4) | sync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww010 Allowed
Histogram (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;
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;
1471 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
1496 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1302 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
2820 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
3258 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
8274 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
30675 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
305194:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
47203 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1167 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
355963:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2079313:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
331269:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
848295:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
2250519:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1301976:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
958272:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1693711:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
119355:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
74288 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
714297:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2769000:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
1021064:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
270161:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
20874 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
812426:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1690630:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
221401:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
208648:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
2900756:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
280293:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
2100918:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
1220813:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
329836:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
280119:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1657076:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
818135:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1283666:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
130093:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
247567:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
591451:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
747202:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
2173862:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
315230:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
4137712:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
2621650:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
3133173:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
4283160:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
594529:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
6174329:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
5553409:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
739436:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
3987666:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1782080:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
4418297:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
2653478:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
4034223:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1253671:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
58555146:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
3785715:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
4580133:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
3840711:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
32901206:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
3161272:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
16420584:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
16884590:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
16277863:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
17965098:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
13056853:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
19519922:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
13583226:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
20879522:>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 94.79
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (76 states)
2 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
4 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
4 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
4 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
1887 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1609 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
1473 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
3022 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1280 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
11655 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2999 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1022291:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
318696:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
290362:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
26494 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1682816:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
125203:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
25026 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
123172:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
939069:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
265786:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
11638 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
72888 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
804713:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
309022:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1592786:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
848684:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
601296:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
712021:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
815393:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
242041:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
318742:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
582190:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
215959:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
2089720:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2640237:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
3458766:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
317652:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2792122:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
2213853:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
806594:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
3832935:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1276392:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
715429:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
211966:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
308738:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1711490:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
4002405:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1343222:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
2840325:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
5469760:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
227743:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
3421735:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
4043504:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
3712137:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
4202892:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
1352024:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
5677862:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
2184963:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2215229:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
15743198:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
13197054:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
17347075:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
13025413:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
4237404:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
4383110:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
16194778:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1212247:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1786323:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
2870401:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
32562775:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
4209127:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
17615253:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
20461058:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
20124007:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
59990855:>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 94.35
$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=
Tue Dec 22 19:52:28 GMT 2009