Tue Dec 22 17:59:42 GMT 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr000
"Fre SyncdWW Wse SyncdWW Wse Rfe SyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | | lwz r3,0(r4) ;
li r3,1 | li r3,1 | | ;
stw r3,0(r4) | stw r3,0(r4) | | ;
exists (x=2 /\ y=2 /\ 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,2
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test acsdrr000 Allowed
Histogram (21 states)
1003116:>3:r1=0; 3:r3=1; x=1; y=1;
3711741:>3:r1=1; 3:r3=0; x=1; y=1;
1310500:>3:r1=1; 3:r3=1; x=2; y=2;
11714362:>3:r1=0; 3:r3=1; x=2; y=2;
12026904:>3:r1=2; 3:r3=1; x=1; y=1;
4065801:>3:r1=2; 3:r3=0; x=1; y=2;
23799040:>3:r1=1; 3:r3=1; x=1; y=1;
7924368:>3:r1=0; 3:r3=1; x=1; y=2;
6885259:>3:r1=1; 3:r3=0; x=1; y=2;
1133527:>3:r1=0; 3:r3=0; x=2; y=2;
2277231:>3:r1=2; 3:r3=1; x=2; y=2;
11014640:>3:r1=1; 3:r3=1; x=2; y=1;
3718404:>3:r1=2; 3:r3=0; x=2; y=1;
20595170:>3:r1=0; 3:r3=0; x=2; y=1;
14661443:>3:r1=1; 3:r3=1; x=1; y=2;
39698962:>3:r1=2; 3:r3=1; x=2; y=1;
34913859:>3:r1=0; 3:r3=0; x=1; y=1;
23783106:>3:r1=2; 3:r3=0; x=1; y=1;
39022292:>3:r1=0; 3:r3=0; x=1; y=2;
27235855:>3:r1=2; 3:r3=1; x=1; y=2;
29504420:>3:r1=0; 3:r3=1; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=f4668bbb62f5902e918e1363d7dcdd40
Cycle=Fre SyncdWW Wse SyncdWW Wse Rfe SyncdRR
Relax acsdrr000 No ACSyncdRR
Safe=Fre Wse SyncdWW
Time acsdrr000 85.44
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr001
"Fre LwSyncdWW Wse SyncdWW Wse Rfe SyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | sync ;
lwsync | sync | | lwz r3,0(r4) ;
li r3,1 | li r3,1 | | ;
stw r3,0(r4) | stw r3,0(r4) | | ;
exists (x=2 /\ y=2 /\ 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,2
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test acsdrr001 Allowed
Histogram (21 states)
827487:>3:r1=0; 3:r3=1; x=1; y=1;
3421471:>3:r1=1; 3:r3=0; x=1; y=1;
6879494:>3:r1=0; 3:r3=1; x=1; y=2;
3010364:>3:r1=2; 3:r3=1; x=2; y=2;
1738549:>3:r1=1; 3:r3=1; x=2; y=2;
21488279:>3:r1=2; 3:r3=0; x=1; y=1;
10397159:>3:r1=2; 3:r3=1; x=1; y=1;
13165787:>3:r1=1; 3:r3=1; x=2; y=1;
6391712:>3:r1=1; 3:r3=0; x=1; y=2;
13698386:>3:r1=0; 3:r3=1; x=2; y=2;
14360910:>3:r1=1; 3:r3=1; x=1; y=2;
1666476:>3:r1=0; 3:r3=0; x=2; y=2;
38008391:>3:r1=0; 3:r3=0; x=1; y=2;
43810583:>3:r1=2; 3:r3=1; x=2; y=1;
4241569:>3:r1=2; 3:r3=0; x=2; y=1;
23476913:>3:r1=0; 3:r3=0; x=2; y=1;
26189793:>3:r1=2; 3:r3=1; x=1; y=2;
21956529:>3:r1=1; 3:r3=1; x=1; y=1;
29718065:>3:r1=0; 3:r3=1; x=2; y=1;
31736835:>3:r1=0; 3:r3=0; x=1; y=1;
3815248:>3:r1=2; 3:r3=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=5f45b9c3dbe15f0ee4cff2cdc24284ec
Cycle=Fre LwSyncdWW Wse SyncdWW Wse Rfe SyncdRR
Relax acsdrr001 No ACSyncdRR
Safe=Fre Wse SyncdWW LwSyncdWW
Time acsdrr001 86.93
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr002
"Fre SyncdWW Wse Rfe SyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | | lwz r3,0(r4) ;
li r3,1 | | ;
stw r3,0(r4) | | ;
exists (x=2 /\ 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,2
_litmus_P1_1_: stw 6,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test acsdrr002 Allowed
Histogram (9 states)
2903897:>2:r1=0; 2:r3=1; x=1;
50227597:>2:r1=1; 2:r3=1; x=1;
21658009:>2:r1=1; 2:r3=1; x=2;
40907384:>2:r1=2; 2:r3=1; x=2;
53610870:>2:r1=2; 2:r3=1; x=1;
99090512:>2:r1=0; 2:r3=0; x=1;
53616289:>2:r1=0; 2:r3=1; x=2;
46553956:>2:r1=2; 2:r3=0; x=1;
31431486:>2:r1=0; 2:r3=0; x=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=a261cdec98922b264d129a58ef893bdb
Cycle=Fre SyncdWW Wse Rfe SyncdRR
Relax acsdrr002 No ACSyncdRR
Safe=Fre Wse SyncdWW
Time acsdrr002 71.45
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr003
"Fre SyncdWR Fre SyncdWW Wse Rfe SyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | | lwz r3,0(r4) ;
lwz r3,0(r4) | li r3,1 | | ;
| stw r3,0(r4) | | ;
exists (y=2 /\ 0: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,2
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 4,0(9)
Test acsdrr003 Allowed
Histogram (21 states)
644054:>0:r3=1; 3:r1=0; 3:r3=1; y=1;
1874952:>0:r3=0; 3:r1=1; 3:r3=1; y=2;
5510766:>0:r3=1; 3:r1=0; 3:r3=1; y=2;
7270433:>0:r3=1; 3:r1=1; 3:r3=0; y=2;
29785038:>0:r3=0; 3:r1=0; 3:r3=1; y=1;
3810158:>0:r3=1; 3:r1=1; 3:r3=0; y=1;
8264173:>0:r3=1; 3:r1=2; 3:r3=1; y=1;
44827839:>0:r3=0; 3:r1=2; 3:r3=1; y=1;
13709904:>0:r3=1; 3:r1=1; 3:r3=1; y=2;
2910635:>0:r3=0; 3:r1=2; 3:r3=1; y=2;
28564593:>0:r3=1; 3:r1=0; 3:r3=0; y=1;
19878260:>0:r3=1; 3:r1=1; 3:r3=1; y=1;
28700017:>0:r3=0; 3:r1=0; 3:r3=0; y=1;
13597188:>0:r3=0; 3:r1=1; 3:r3=1; y=1;
25298407:>0:r3=1; 3:r1=2; 3:r3=1; y=2;
35798954:>0:r3=1; 3:r1=0; 3:r3=0; y=2;
22114563:>0:r3=1; 3:r1=2; 3:r3=0; y=1;
3018677:>0:r3=0; 3:r1=0; 3:r3=0; y=2;
14140821:>0:r3=0; 3:r1=0; 3:r3=1; y=2;
4207371:>0:r3=1; 3:r1=2; 3:r3=0; y=2;
6073197:>0:r3=0; 3:r1=2; 3:r3=0; y=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=b6db3fc589db44216c30ccbc4b5a9611
Cycle=Fre SyncdWR Fre SyncdWW Wse Rfe SyncdRR
Relax acsdrr003 No ACSyncdRR
Safe=Fre Wse SyncdWW SyncdWR
Time acsdrr003 85.01
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr004
"Fre SyncsWR Fre SyncdWW Wse Rfe SyncdRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | | lwz r3,0(r4) ;
lwz r3,0(r2) | li r3,1 | | ;
| stw r3,0(r4) | | ;
exists (x=2 /\ y=2 /\ 0:r3=1 /\ 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,2
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: li 6,2
_litmus_P1_1_: stw 6,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 5,1
_litmus_P1_4_: stw 5,0(9)
_litmus_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 6,0(9)
Test acsdrr004 Allowed
Histogram (39 states)
580659:>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1021357:>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
801493:>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
14511 :>0:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
54260 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
97249 :>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
583995:>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
97903 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2;
665922:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
1105496:>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
3294934:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
1466065:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
3072611:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1;
2999032:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
6447142:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
25454455:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
11968740:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
4151619:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
3220776:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
6402734:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
8616791:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1;
12642035:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
1300157:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2;
2817417:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
13610701:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
1803909:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
7045599:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
5786353:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1;
17528952:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
25405063:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
23844901:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
19639269:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2;
2597880:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
13317616:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
18723962:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
31427295:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
7344838:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2;
9877381:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
23168928:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=3e9c4d396fcad12ee5da6f76dcf812c7
Cycle=Fre SyncsWR Fre SyncdWW Wse Rfe SyncdRR
Relax acsdrr004 No ACSyncdRR
Safe=Fre Wse SyncsWR SyncdWW
Time acsdrr004 88.43
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr005
"Fre SyncdWW Wse LwSyncdWW Wse Rfe SyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | lwsync | | lwz r3,0(r4) ;
li r3,1 | li r3,1 | | ;
stw r3,0(r4) | stw r3,0(r4) | | ;
exists (x=2 /\ y=2 /\ 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,2
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test acsdrr005 Allowed
Histogram (21 states)
807495:>3:r1=0; 3:r3=1; x=1; y=1;
1304661:>3:r1=0; 3:r3=0; x=2; y=2;
1943364:>3:r1=1; 3:r3=1; x=2; y=2;
2944471:>3:r1=2; 3:r3=1; x=2; y=2;
35085159:>3:r1=2; 3:r3=1; x=2; y=1;
3416619:>3:r1=2; 3:r3=0; x=2; y=1;
6646895:>3:r1=0; 3:r3=1; x=1; y=2;
17892842:>3:r1=1; 3:r3=1; x=1; y=2;
32128647:>3:r1=2; 3:r3=1; x=1; y=2;
19064423:>3:r1=0; 3:r3=0; x=2; y=1;
23094450:>3:r1=1; 3:r3=1; x=1; y=1;
12665612:>3:r1=0; 3:r3=1; x=2; y=2;
11486239:>3:r1=1; 3:r3=0; x=1; y=2;
22039703:>3:r1=2; 3:r3=0; x=1; y=1;
10848550:>3:r1=2; 3:r3=1; x=1; y=1;
32592020:>3:r1=0; 3:r3=0; x=1; y=1;
27580251:>3:r1=0; 3:r3=1; x=2; y=1;
3996766:>3:r1=1; 3:r3=0; x=1; y=1;
5966634:>3:r1=2; 3:r3=0; x=1; y=2;
35757125:>3:r1=0; 3:r3=0; x=1; y=2;
12738074:>3:r1=1; 3:r3=1; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=b6e9fe2e5db536ad9a06213fb6ed8db9
Cycle=Fre SyncdWW Wse LwSyncdWW Wse Rfe SyncdRR
Relax acsdrr005 No ACSyncdRR
Safe=Fre Wse SyncdWW LwSyncdWW
Time acsdrr005 84.65
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr006
"Fre LwSyncdWW Wse LwSyncdWW Wse Rfe SyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | sync ;
lwsync | lwsync | | lwz r3,0(r4) ;
li r3,1 | li r3,1 | | ;
stw r3,0(r4) | stw r3,0(r4) | | ;
exists (x=2 /\ y=2 /\ 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,2
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test acsdrr006 Allowed
Histogram (21 states)
622989:>3:r1=0; 3:r3=1; x=1; y=1;
1854291:>3:r1=0; 3:r3=0; x=2; y=2;
3649296:>3:r1=1; 3:r3=0; x=1; y=1;
9755194:>3:r1=2; 3:r3=1; x=1; y=1;
2702375:>3:r1=1; 3:r3=1; x=2; y=2;
10651001:>3:r1=1; 3:r3=0; x=1; y=2;
5387760:>3:r1=2; 3:r3=0; x=1; y=2;
28063010:>3:r1=0; 3:r3=1; x=2; y=1;
17274928:>3:r1=1; 3:r3=1; x=1; y=2;
3767095:>3:r1=2; 3:r3=0; x=2; y=1;
4130712:>3:r1=2; 3:r3=1; x=2; y=2;
34825815:>3:r1=0; 3:r3=0; x=1; y=2;
19845796:>3:r1=2; 3:r3=0; x=1; y=1;
5846069:>3:r1=0; 3:r3=1; x=1; y=2;
29999692:>3:r1=0; 3:r3=0; x=1; y=1;
30752225:>3:r1=2; 3:r3=1; x=1; y=2;
38840320:>3:r1=2; 3:r3=1; x=2; y=1;
21391978:>3:r1=0; 3:r3=0; x=2; y=1;
14624957:>3:r1=0; 3:r3=1; x=2; y=2;
21395888:>3:r1=1; 3:r3=1; x=1; y=1;
14618609:>3:r1=1; 3:r3=1; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=04f3e54d9d70f9d6de8993f037ab8473
Cycle=Fre LwSyncdWW Wse LwSyncdWW Wse Rfe SyncdRR
Relax acsdrr006 No ACSyncdRR
Safe=Fre Wse LwSyncdWW
Time acsdrr006 87.34
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr007
"Fre LwSyncdWW Wse Rfe SyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
lwsync | | lwz r3,0(r4) ;
li r3,1 | | ;
stw r3,0(r4) | | ;
exists (x=2 /\ 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,2
_litmus_P1_1_: stw 6,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test acsdrr007 Allowed
Histogram (9 states)
1520561:>2:r1=0; 2:r3=1; x=1;
43045286:>2:r1=1; 2:r3=1; x=1;
40123158:>2:r1=0; 2:r3=1; x=2;
49562431:>2:r1=2; 2:r3=1; x=1;
34662196:>2:r1=0; 2:r3=0; x=2;
33979081:>2:r1=1; 2:r3=1; x=2;
57659505:>2:r1=2; 2:r3=1; x=2;
44038639:>2:r1=2; 2:r3=0; x=1;
95409143:>2:r1=0; 2:r3=0; x=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=64b08d9964a91d502b8b10812d9b32b9
Cycle=Fre LwSyncdWW Wse Rfe SyncdRR
Relax acsdrr007 No ACSyncdRR
Safe=Fre Wse LwSyncdWW
Time acsdrr007 71.73
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr008.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr008
"Fre SyncdWR Fre LwSyncdWW Wse Rfe SyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | lwsync | | lwz r3,0(r4) ;
lwz r3,0(r4) | li r3,1 | | ;
| stw r3,0(r4) | | ;
exists (y=2 /\ 0: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,2
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 4,0(9)
Test acsdrr008 Allowed
Histogram (21 states)
4418768:>0:r3=1; 3:r1=0; 3:r3=1; y=2;
3745307:>0:r3=0; 3:r1=2; 3:r3=1; y=2;
436577:>0:r3=1; 3:r1=0; 3:r3=1; y=1;
2637750:>0:r3=0; 3:r1=1; 3:r3=1; y=2;
4138416:>0:r3=1; 3:r1=1; 3:r3=0; y=1;
18896732:>0:r3=1; 3:r1=1; 3:r3=1; y=1;
6957289:>0:r3=1; 3:r1=2; 3:r3=1; y=1;
11715392:>0:r3=1; 3:r1=1; 3:r3=0; y=2;
16244783:>0:r3=1; 3:r1=1; 3:r3=1; y=2;
26265297:>0:r3=1; 3:r1=0; 3:r3=0; y=1;
15898375:>0:r3=0; 3:r1=1; 3:r3=1; y=1;
33351719:>0:r3=1; 3:r1=0; 3:r3=0; y=2;
39733139:>0:r3=0; 3:r1=2; 3:r3=1; y=1;
27103529:>0:r3=0; 3:r1=0; 3:r3=1; y=1;
3585810:>0:r3=0; 3:r1=0; 3:r3=0; y=2;
29210338:>0:r3=1; 3:r1=2; 3:r3=1; y=2;
5613505:>0:r3=0; 3:r1=2; 3:r3=0; y=1;
26996135:>0:r3=0; 3:r1=0; 3:r3=0; y=1;
16070037:>0:r3=0; 3:r1=0; 3:r3=1; y=2;
6210614:>0:r3=1; 3:r1=2; 3:r3=0; y=2;
20770488:>0:r3=1; 3:r1=2; 3:r3=0; y=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=78a292439dc422b6e8d30112bf3ced0e
Cycle=Fre SyncdWR Fre LwSyncdWW Wse Rfe SyncdRR
Relax acsdrr008 No ACSyncdRR
Safe=Fre Wse SyncdWR LwSyncdWW
Time acsdrr008 86.12
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr009.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr009
"Fre SyncsWR Fre LwSyncdWW Wse Rfe SyncdRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | lwsync | | lwz r3,0(r4) ;
lwz r3,0(r2) | li r3,1 | | ;
| stw r3,0(r4) | | ;
exists (x=2 /\ y=2 /\ 0:r3=1 /\ 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,2
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: li 6,2
_litmus_P1_1_: stw 6,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 5,1
_litmus_P1_4_: stw 5,0(9)
_litmus_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 6,0(9)
Test acsdrr009 Allowed
Histogram (39 states)
22763 :>0:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
756896:>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1029537:>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
533465:>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
88082 :>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
115581:>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2;
1346584:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
387048:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
1164711:>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
1363574:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2;
1224379:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
57532 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
1000107:>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
10389164:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
3448851:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
5140531:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
3400390:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1;
10925001:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1;
3934135:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
13149436:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
6471783:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
17153149:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2;
21988616:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
15546201:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
5025308:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
10889545:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
23267923:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
5792415:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
16604545:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
3574229:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
4951033:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
23499489:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
6379142:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2;
28332958:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
2792381:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
8415007:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1;
15834281:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
15475220:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
28529008:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=745664b5fbc00e7ca847ad37ec693890
Cycle=Fre SyncsWR Fre LwSyncdWW Wse Rfe SyncdRR
Relax acsdrr009 No ACSyncdRR
Safe=Fre Wse SyncsWR LwSyncdWW
Time acsdrr009 83.53
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr010
"Fre Rfe SyncdRR Fre Rfe SyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y;}
P0 | P1 | P2 | P3 ;
lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,1 ;
sync | stw r1,0(r2) | sync | stw r1,0(r2) ;
lwz r3,0(r4) | | lwz r3,0(r4) | ;
exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P3_0_: li 8,1
_litmus_P3_1_: stw 8,0(9)
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 4,0(9)
_litmus_P1_0_: li 7,1
_litmus_P1_1_: stw 7,0(9)
_litmus_P0_0_: lwz 3,0(11)
_litmus_P0_1_: sync
_litmus_P0_2_: lwz 4,0(9)
Test acsdrr010 Allowed
Histogram (15 states)
453039:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1;
5176719:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0;
54338084:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0;
21839246:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1;
6012484:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1;
22025069:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0;
20338750:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1;
26383751:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1;
25191034:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0;
5261368:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0;
5968078:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0;
26044882:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1;
20263145:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0;
25277555:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1;
55426796:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=636f71f6ac76c8070d3470d463d1e541
Cycle=Fre Rfe SyncdRR Fre Rfe SyncdRR
Relax acsdrr010 No ACSyncdRR
Safe=Fre
Time acsdrr010 75.85
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr011.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr011
"Fre SyncdWW Rfe SyncdRR Fre Rfe SyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
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) | | lwz r3,0(r4) ;
li r3,1 | | | ;
stw r3,0(r4) | | | ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 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_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 31,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test acsdrr011 Allowed
Histogram (15 states)
1855972:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
5608621:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
32160272:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
22100641:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
2182940:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
821647:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
27340175:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
12592485:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
11954073:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
31544809:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
41005245:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
59659456:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
2111066:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
31812702:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
37249896:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=9ba8d06082edddfad8113101654d0430
Cycle=Fre SyncdWW Rfe SyncdRR Fre Rfe SyncdRR
Relax acsdrr011 No ACSyncdRR
Safe=Fre SyncdWW
Time acsdrr011 83.89
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr012.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr012
"Fre SyncsWW Rfe SyncdRR Fre Rfe SyncdRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
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) | | lwz r3,0(r4) ;
li r3,2 | | | ;
stw r3,0(r2) | | | ;
exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 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_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 7,1
_litmus_P0_1_: stw 7,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test acsdrr012 Allowed
Histogram (35 states)
2 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
1 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
3254 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
220755:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
156395:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
1045615:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
531091:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
1023693:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
4182989:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
2176430:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
1968520:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
826701:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
5617831:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
3653410:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
2366392:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
2869432:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
1404881:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
2077183:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
2217262:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
4818755:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
21335613:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
2964571:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
5326525:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
22005202:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
6007908:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
21598175:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
20709469:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
4049719:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
5921079:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
19280652:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
26226927:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
12654130:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
40058950:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
17981978:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
56718510:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=36537b94a10ccfe23173e79705a28b83
Cycle=Fre SyncsWW Rfe SyncdRR Fre Rfe SyncdRR
Relax acsdrr012 No ACSyncdRR
Safe=Fre SyncsWW
Time acsdrr012 83.48
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr013.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr013
"Fre LwSyncdWW Rfe SyncdRR Fre Rfe SyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
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 ;
lwsync | lwz r3,0(r4) | | lwz r3,0(r4) ;
li r3,1 | | | ;
stw r3,0(r4) | | | ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 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_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 31,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test acsdrr013 Allowed
Histogram (15 states)
1216265:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
1677143:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
39109493:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
24003236:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
2440479:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
27272796:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
30454676:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
57483243:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
42460300:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
3951497:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
29149974:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
14381743:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
16528217:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
4974200:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
24896738:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=f7450a70568e1efcac71344b7c31e524
Cycle=Fre LwSyncdWW Rfe SyncdRR Fre Rfe SyncdRR
Relax acsdrr013 No ACSyncdRR
Safe=Fre LwSyncdWW
Time acsdrr013 83.13
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr014.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr014
"Fre LwSyncsWW Rfe SyncdRR Fre Rfe SyncdRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
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 ;
lwsync | lwz r3,0(r4) | | lwz r3,0(r4) ;
li r3,2 | | | ;
stw r3,0(r2) | | | ;
exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 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_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 7,1
_litmus_P0_1_: stw 7,0(9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test acsdrr014 Allowed
Histogram (33 states)
849 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
73618 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
136544:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
234345:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
488814:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
204288:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
1092893:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
128753:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
1876874:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
692249:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
1070970:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
2327824:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
1853276:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
811112:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
2785270:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
1697417:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
5526873:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
21690390:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
429303:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
1010621:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
22831572:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
17325400:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
1111613:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
24268098:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
5400234:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
23814611:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
20264573:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
23879939:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
5822354:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
23389091:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
48824863:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
54941107:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
3994262:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=b700f92a76eb70d8c18d53f7af0a21d5
Cycle=Fre LwSyncsWW Rfe SyncdRR Fre Rfe SyncdRR
Relax acsdrr014 No ACSyncdRR
Safe=Fre LwSyncsWW
Time acsdrr014 84.90
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr015.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr015
"Fre SyncdWW Wse SyncdWR Fre Rfe SyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | | lwz r3,0(r4) ;
li r3,1 | lwz r3,0(r4) | | ;
stw r3,0(r4) | | | ;
exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 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_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 3,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test acsdrr015 Allowed
Histogram (15 states)
2453159:>1:r3=0; 3:r1=0; 3:r3=0; x=2;
5097253:>1:r3=0; 3:r1=1; 3:r3=1; x=2;
3775013:>1:r3=1; 3:r1=1; 3:r3=0; x=2;
5651443:>1:r3=0; 3:r1=1; 3:r3=0; x=1;
23756661:>1:r3=1; 3:r1=0; 3:r3=1; x=2;
26452957:>1:r3=1; 3:r1=1; 3:r3=0; x=1;
18983219:>1:r3=1; 3:r1=0; 3:r3=0; x=2;
28319744:>1:r3=0; 3:r1=1; 3:r3=1; x=1;
31043277:>1:r3=1; 3:r1=1; 3:r3=1; x=1;
19393195:>1:r3=0; 3:r1=0; 3:r3=1; x=2;
516046:>1:r3=1; 3:r1=0; 3:r3=1; x=1;
27632734:>1:r3=1; 3:r1=0; 3:r3=0; x=1;
23228998:>1:r3=0; 3:r1=0; 3:r3=1; x=1;
47724175:>1:r3=1; 3:r1=1; 3:r3=1; x=2;
55972126:>1:r3=0; 3:r1=0; 3:r3=0; x=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=93405f0ed846673bae038ca9a3ad151b
Cycle=Fre SyncdWW Wse SyncdWR Fre Rfe SyncdRR
Relax acsdrr015 No ACSyncdRR
Safe=Fre Wse SyncdWW SyncdWR
Time acsdrr015 84.49
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr016.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr016
"Fre LwSyncdWW Wse SyncdWR Fre Rfe SyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | sync ;
lwsync | sync | | lwz r3,0(r4) ;
li r3,1 | lwz r3,0(r4) | | ;
stw r3,0(r4) | | | ;
exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 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_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 3,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test acsdrr016 Allowed
Histogram (15 states)
352739:>1:r3=1; 3:r1=0; 3:r3=1; x=1;
3414580:>1:r3=0; 3:r1=0; 3:r3=0; x=2;
5287263:>1:r3=0; 3:r1=1; 3:r3=0; x=1;
4214543:>1:r3=1; 3:r1=1; 3:r3=0; x=2;
23920468:>1:r3=1; 3:r1=0; 3:r3=1; x=2;
21315984:>1:r3=1; 3:r1=0; 3:r3=0; x=2;
23697873:>1:r3=1; 3:r1=1; 3:r3=0; x=1;
22239790:>1:r3=0; 3:r1=0; 3:r3=1; x=2;
21582560:>1:r3=0; 3:r1=0; 3:r3=1; x=1;
6356430:>1:r3=0; 3:r1=1; 3:r3=1; x=2;
26943469:>1:r3=0; 3:r1=1; 3:r3=1; x=1;
25190810:>1:r3=1; 3:r1=0; 3:r3=0; x=1;
28235169:>1:r3=1; 3:r1=1; 3:r3=1; x=1;
53209794:>1:r3=1; 3:r1=1; 3:r3=1; x=2;
54038528:>1:r3=0; 3:r1=0; 3:r3=0; x=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=8a3aeefda3b897535b28a928e24ffa41
Cycle=Fre LwSyncdWW Wse SyncdWR Fre Rfe SyncdRR
Relax acsdrr016 No ACSyncdRR
Safe=Fre Wse SyncdWR LwSyncdWW
Time acsdrr016 85.89
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr017.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr017
"Fre SyncdWR Fre Rfe SyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | | lwz r3,0(r4) ;
lwz r3,0(r4) | | ;
exists (0:r3=0 /\ 2:r1=1 /\ 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_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test acsdrr017 Allowed
Histogram (8 states)
2 :>0:r3=0; 2:r1=1; 2:r3=0;
713218:>0:r3=1; 2:r1=0; 2:r3=1;
50063347:>0:r3=0; 2:r1=0; 2:r3=0;
48142340:>0:r3=1; 2:r1=1; 2:r3=0;
54129425:>0:r3=0; 2:r1=1; 2:r3=1;
88532285:>0:r3=1; 2:r1=1; 2:r3=1;
77244022:>0:r3=0; 2:r1=0; 2:r3=1;
81175361:>0:r3=1; 2:r1=0; 2:r3=0;
Ok
Witnesses
Positive: 2, Negative: 399999998
Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is validated
Hash=594d010ae884a7901d60ab5268a95257
Cycle=Fre SyncdWR Fre Rfe SyncdRR
Relax acsdrr017 Ok ACSyncdRR
Safe=Fre SyncdWR
Time acsdrr017 74.50
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr018.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr018
"Fre SyncdWR Fre SyncdWR Fre Rfe SyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | | lwz r3,0(r4) ;
lwz r3,0(r4) | lwz r3,0(r4) | | ;
exists (0:r3=0 /\ 1:r3=0 /\ 3:r1=1 /\ 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_P1_0_: li 4,1
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 3,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 4,0(9)
Test acsdrr018 Allowed
Histogram (15 states)
5622784:>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=0;
6304099:>0:r3=0; 1:r3=0; 3:r1=1; 3:r3=1;
23412971:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1;
255473:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1;
22955068:>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=1;
19760590:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1;
6057682:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=0;
22225175:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0;
25699966:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0;
25453056:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1;
53088798:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1;
54004862:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0;
24994715:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1;
5414170:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=0;
24750591:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (0:r3=0 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=7694032af7eaa4c629a106dbe2fda3e2
Cycle=Fre SyncdWR Fre SyncdWR Fre Rfe SyncdRR
Relax acsdrr018 No ACSyncdRR
Safe=Fre SyncdWR
Time acsdrr018 83.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr019.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr019
"Fre SyncsWR Fre SyncdWR Fre Rfe SyncdRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | | lwz r3,0(r4) ;
lwz r3,0(r2) | lwz r3,0(r4) | | ;
exists (y=2 /\ 0:r3=1 /\ 1:r3=0 /\ 3:r1=1 /\ 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_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 4,0(9)
_litmus_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 6,0(9)
Test acsdrr019 Allowed
Histogram (32 states)
3 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
36071 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
43207 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
32888 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
1744178:>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
2102970:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
1023436:>0:r3=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
1465338:>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
103516:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
1428726:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
2545712:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
6255931:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
5723970:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
24862927:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; y=1;
27901561:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
185370:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=1;
4968633:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=1;
3278481:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
9100092:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=1;
7255277:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
678256:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=1;
34863975:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
18601502:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=1;
20165382:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=1;
22862978:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
19145041:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=1;
13525925:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=1;
14025835:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
29636265:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=1;
19394746:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
7865153:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
19176655:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (y=2 /\ 0:r3=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=a3b2b2fd87d8003094c276c1c7dc52d1
Cycle=Fre SyncsWR Fre SyncdWR Fre Rfe SyncdRR
Relax acsdrr019 No ACSyncdRR
Safe=Fre SyncsWR SyncdWR
Time acsdrr019 82.34
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr020.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr020
"Fre SyncdWR Fre SyncsWR Fre Rfe SyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 3:r2=x; 3:r4=y;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | | lwz r3,0(r4) ;
lwz r3,0(r4) | lwz r3,0(r2) | | ;
exists (x=2 /\ 0:r3=0 /\ 1:r3=1 /\ 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,2
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: li 11,1
_litmus_P1_1_: stw 11,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 5,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 4,0(9)
Test acsdrr020 Allowed
Histogram (48 states)
17 :>0:r3=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2;
111 :>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; x=1;
71 :>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2;
5850 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2;
6937 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
21925 :>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
82619 :>0:r3=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
70777 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
2304380:>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
116662:>0:r3=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
390692:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
123183:>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
203868:>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2;
132042:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
62427 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
628739:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
3075282:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
1161376:>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2;
2300857:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
171164:>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
1613605:>0:r3=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
9617226:>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
2259855:>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
1452352:>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
6597900:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=1;
3284055:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
10537360:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
10994535:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
15209518:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
19107636:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
9963654:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
7833931:>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
7277846:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
5358890:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2;
9132202:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
17943389:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
20608907:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
20871617:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
6587130:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
6529968:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2;
12164208:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
16661363:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=0; x=1;
17685826:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
18171824:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
15802977:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
5748967:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=1;
16299398:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2;
13824882:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ 0:r3=0 /\ 1:r3=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=364b008b4e827c7da8277245f7998211
Cycle=Fre SyncdWR Fre SyncsWR Fre Rfe SyncdRR
Relax acsdrr020 No ACSyncdRR
Safe=Fre SyncsWR SyncdWR
Time acsdrr020 89.49
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr021.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr021
"Fre SyncdWW Wse SyncdWW Rfe SyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | lwz r3,0(r4) ;
li r3,1 | li r3,1 | ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (x=2 /\ 2:r1=1 /\ 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 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test acsdrr021 Allowed
Histogram (7 states)
9660234:>2:r1=1; 2:r3=1; x=2;
14022182:>2:r1=0; 2:r3=1; x=1;
133533707:>2:r1=0; 2:r3=0; x=1;
15230227:>2:r1=1; 2:r3=0; x=1;
33335530:>2:r1=0; 2:r3=0; x=2;
109972100:>2:r1=0; 2:r3=1; x=2;
84246020:>2:r1=1; 2:r3=1; x=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=5d5c1aae91591f0f085c166e6ff700e6
Cycle=Fre SyncdWW Wse SyncdWW Rfe SyncdRR
Relax acsdrr021 No ACSyncdRR
Safe=Fre Wse SyncdWW
Time acsdrr021 72.88
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr022.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr022
"Fre LwSyncdWW Wse SyncdWW Rfe SyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
lwsync | sync | lwz r3,0(r4) ;
li r3,1 | li r3,1 | ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (x=2 /\ 2:r1=1 /\ 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 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test acsdrr022 Allowed
Histogram (7 states)
10800079:>2:r1=0; 2:r3=1; x=1;
12424286:>2:r1=1; 2:r3=1; x=2;
37939039:>2:r1=0; 2:r3=0; x=2;
14886321:>2:r1=1; 2:r3=0; x=1;
128887371:>2:r1=0; 2:r3=0; x=1;
78433092:>2:r1=1; 2:r3=1; x=1;
116629812:>2:r1=0; 2:r3=1; x=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=33d57db58ff4f0de2ca9b62adc3c44e3
Cycle=Fre LwSyncdWW Wse SyncdWW Rfe SyncdRR
Relax acsdrr022 No ACSyncdRR
Safe=Fre Wse SyncdWW LwSyncdWW
Time acsdrr022 75.52
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr023.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr023
"Fre SyncdWW Rfe SyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | sync ;
sync | lwz r3,0(r4) ;
li r3,1 | ;
stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0)
Generated assembler
_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(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test acsdrr023 Allowed
Histogram (3 states)
107909890:>1:r1=0; 1:r3=1;
308272964:>1:r1=0; 1:r3=0;
223817146:>1:r1=1; 1:r3=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (1:r1=1 /\ 1:r3=0) is NOT validated
Hash=e29ebb6e64fa9079ba348c5180003cc2
Cycle=Fre SyncdWW Rfe SyncdRR
Relax acsdrr023 No ACSyncdRR
Safe=Fre SyncdWW
Time acsdrr023 74.46
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr024.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr024
"Fre SyncdWW Rfe SyncdRR Fre SyncdWW Rfe SyncdRR"
{0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;}
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,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 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 6,1
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 31,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test acsdrr024 Allowed
Histogram (15 states)
5779043:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
478576:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
11872872:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
12736935:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
435931:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
48753630:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
13213050:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
34111959:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
726142:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
21014541:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
35004260:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
72251753:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
50138057:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
12836134:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
647117:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=6614bb5f345fce6def5659d5fa2123d7
Cycle=Fre SyncdWW Rfe SyncdRR Fre SyncdWW Rfe SyncdRR
Relax acsdrr024 No ACSyncdRR
Safe=Fre SyncdWW
Time acsdrr024 93.28
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr025.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr025
"Fre SyncsWW Rfe SyncdRR Fre SyncdWW Rfe SyncdRR"
{0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;}
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,1 | ;
stw r3,0(r2) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 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 5,1
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 7,1
_litmus_P0_1_: stw 7,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test acsdrr025 Allowed
Histogram (33 states)
545 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
857920:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
834379:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
587732:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
794924:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
972833:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
621715:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
723329:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
3565923:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
606395:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
4449203:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1999391:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
8198563:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
791861:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
1155662:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
7094069:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
2202417:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
32778553:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
3796297:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
1292195:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
29386922:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
18108293:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1037887:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
928936:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
2613027:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
22418470:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
21242284:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
10595663:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
4704625:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
13664961:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
63396645:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
24000560:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
34577821:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=54bc20dc4f311ade7a2f268864e2abfd
Cycle=Fre SyncsWW Rfe SyncdRR Fre SyncdWW Rfe SyncdRR
Relax acsdrr025 No ACSyncdRR
Safe=Fre SyncsWW SyncdWW
Time acsdrr025 92.13
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr026.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr026
"Fre LwSyncdWW Rfe SyncdRR Fre SyncdWW Rfe SyncdRR"
{0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;}
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 ;
lwsync | lwz r3,0(r4) | sync | lwz r3,0(r4) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 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 6,1
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 31,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test acsdrr026 Allowed
Histogram (15 states)
1155723:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
459925:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
15802946:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
4851189:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
10730640:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
11851528:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
24677657:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
1001088:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
37664278:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
32208261:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
19617157:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
47064722:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
42456476:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
69880071:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
578339:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=1e2ab3a033eb8d91c878eb2ef29c7240
Cycle=Fre LwSyncdWW Rfe SyncdRR Fre SyncdWW Rfe SyncdRR
Relax acsdrr026 No ACSyncdRR
Safe=Fre SyncdWW LwSyncdWW
Time acsdrr026 93.68
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr027.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr027
"Fre LwSyncsWW Rfe SyncdRR Fre SyncdWW Rfe SyncdRR"
{0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;}
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 ;
lwsync | lwz r3,0(r4) | sync | lwz r3,0(r4) ;
li r3,2 | | li r3,1 | ;
stw r3,0(r2) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 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 5,1
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 7,1
_litmus_P0_1_: stw 7,0(9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test acsdrr027 Allowed
Histogram (33 states)
224 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
134177:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
1121933:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
274414:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
104637:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
301864:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
198782:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
906005:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
1956064:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
2894418:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
2351115:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
299539:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
1582654:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
1537771:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
349954:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
248122:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
791479:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
2383133:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
464829:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
1525994:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
19708446:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
3465933:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
29112831:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
1644364:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
25422693:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
11027799:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
29648978:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
37960794:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
31076697:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
4313836:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
34174197:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
60761844:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
12254480:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=395dda6a76de9dcf7e101c7347e87098
Cycle=Fre LwSyncsWW Rfe SyncdRR Fre SyncdWW Rfe SyncdRR
Relax acsdrr027 No ACSyncdRR
Safe=Fre SyncdWW LwSyncsWW
Time acsdrr027 92.78
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr028.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr028
"Fre SyncdWR Fre SyncdWW Rfe SyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;}
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,1 | ;
| stw r3,0(r4) | ;
exists (0:r3=0 /\ 2:r1=1 /\ 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 4,1
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,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 acsdrr028 Allowed
Histogram (7 states)
7873340:>0:r3=1; 2:r1=0; 2:r3=1;
116171164:>0:r3=0; 2:r1=0; 2:r3=1;
51567686:>0:r3=0; 2:r1=0; 2:r3=0;
76249804:>0:r3=1; 2:r1=1; 2:r3=1;
16715558:>0:r3=0; 2:r1=1; 2:r3=1;
114892356:>0:r3=1; 2:r1=0; 2:r3=0;
16530092:>0:r3=1; 2:r1=1; 2:r3=0;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=253c3d0e979b12ac15c5e6729d565644
Cycle=Fre SyncdWR Fre SyncdWW Rfe SyncdRR
Relax acsdrr028 No ACSyncdRR
Safe=Fre SyncdWW SyncdWR
Time acsdrr028 78.07
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr029.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr029
"Fre SyncsWR Fre SyncdWW Rfe SyncdRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 2:r4=y;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | lwz r3,0(r4) ;
lwz r3,0(r2) | li r3,1 | ;
| stw r3,0(r4) | ;
exists (y=2 /\ 0:r3=1 /\ 2:r1=1 /\ 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 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 5,0(9)
Test acsdrr029 Allowed
Histogram (13 states)
110879:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
2157720:>0:r3=2; 2:r1=1; 2:r3=2; y=2;
8960806:>0:r3=1; 2:r1=0; 2:r3=1; y=1;
70108913:>0:r3=1; 2:r1=1; 2:r3=1; y=1;
1071430:>0:r3=2; 2:r1=0; 2:r3=2; y=2;
64303621:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
42233848:>0:r3=1; 2:r1=0; 2:r3=2; y=1;
8197924:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
62346512:>0:r3=1; 2:r1=0; 2:r3=0; y=1;
14219212:>0:r3=1; 2:r1=1; 2:r3=2; y=2;
56892505:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
54660486:>0:r3=1; 2:r1=0; 2:r3=2; y=2;
14736144:>0:r3=1; 2:r1=1; 2:r3=2; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=b11bf67f6ac9a0eb7e2bfc28b97cd05c
Cycle=Fre SyncsWR Fre SyncdWW Rfe SyncdRR
Relax acsdrr029 No ACSyncdRR
Safe=Fre SyncsWR SyncdWW
Time acsdrr029 76.68
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr030.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr030
"Fre SyncsWW Rfe SyncdRR Fre SyncsWW Rfe SyncdRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
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 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 4,0(9)
_litmus_P0_0_: li 7,1
_litmus_P0_1_: stw 7,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test acsdrr030 Allowed
Histogram (72 states)
1196 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1449 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
1729 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1393 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
46613 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
2396 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
73343 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1055 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
7602 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
285852:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
901746:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
757633:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
122825:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
270164:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1610243:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
3043387:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
210781:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
325471:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
263207:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
541799:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
3719630:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
762400:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
569264:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1876255:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
324903:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1240003:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1690817:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1217486:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
2591396:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
2800958:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
1655195:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
287856:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
28381 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
48062 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
691731:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
4166873:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
212819:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
13760252:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
4397431:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
288585:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
713077:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1142624:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
765149:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
116505:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2001818:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
4462331:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
751287:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
254252:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1751244:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
17672003:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
17130421:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
2782112:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
3603492:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1306974:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
316619:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
5741780:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
910242:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
4174829:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
2424452:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
20450680:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
34258274:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
3890370:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
2077792:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
2969792:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
5787724:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
17663614:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
3956666:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
20105715:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
13627749:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
1994669:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
16687098:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
57708465:>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=e437caed8f6d9647f946982642be159d
Cycle=Fre SyncsWW Rfe SyncdRR Fre SyncsWW Rfe SyncdRR
Relax acsdrr030 No ACSyncdRR
Safe=Fre SyncsWW
Time acsdrr030 95.17
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr031.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr031
"Fre LwSyncdWW Rfe SyncdRR Fre SyncsWW Rfe SyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
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 ;
lwsync | lwz r3,0(r4) | sync | lwz r3,0(r4) ;
li r3,1 | | li r3,2 | ;
stw r3,0(r4) | | stw r3,0(r2) | ;
exists (y=2 /\ 1:r1=1 /\ 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 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 31,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test acsdrr031 Allowed
Histogram (33 states)
669 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
1118917:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; y=2;
658642:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
2022033:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
2239928:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; y=2;
20441487:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; y=2;
1443321:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
18627668:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; y=2;
1997750:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; y=2;
929550:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; y=2;
8564818:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
946002:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
3928578:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; y=2;
5021010:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; y=2;
1931229:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; y=2;
582291:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
1015581:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
1240045:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; y=2;
4752975:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; y=2;
1102102:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
742640:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; y=2;
7340182:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
11342617:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; y=2;
1249602:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
18859653:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
4926800:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
33588950:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; y=2;
61404002:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
29856877:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
30973157:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; y=2;
1096341:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; y=2;
18875225:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; y=2;
21179358:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (y=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=a80182bdadf201f75f7bb65ee084fa69
Cycle=Fre LwSyncdWW Rfe SyncdRR Fre SyncsWW Rfe SyncdRR
Relax acsdrr031 No ACSyncdRR
Safe=Fre SyncsWW LwSyncdWW
Time acsdrr031 90.75
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr032.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr032
"Fre LwSyncsWW Rfe SyncdRR Fre SyncsWW Rfe SyncdRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
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 ;
lwsync | 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 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 4,0(9)
_litmus_P0_0_: li 7,1
_litmus_P0_1_: stw 7,0(9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test acsdrr032 Allowed
Histogram (72 states)
553 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
543 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1180 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1372 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2817 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
13242 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
460 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
2413 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
56277 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
141772:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
81413 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
41023 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
32469 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
23666 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
115575:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
362710:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
78531 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
102706:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
243476:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
271757:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
375809:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
181864:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
186836:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
55905 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
273361:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
111690:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
469326:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
1010502:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
694440:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
920758:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2286076:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1156853:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
893455:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
338963:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
121002:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
3553913:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
240238:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1915943:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
813468:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
2366448:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
355439:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
397072:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1228843:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1708307:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
2631002:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
2316293:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
695430:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
5079192:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
150408:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1703541:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1285069:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
2460769:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
5002190:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2769604:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
2093283:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1745631:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2506669:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
5304096:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
18406050:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
3563219:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
20859686:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
55195657:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
19381728:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
12477545:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
3356842:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
18354214:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
6009387:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
18342185:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
38553191:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
4509275:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
23614684:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
18402694:>1:r1=0; 1:r3=0; 3:r1=0; 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=5dbd213a60e04f42d1a6588419a502dc
Cycle=Fre LwSyncsWW Rfe SyncdRR Fre SyncsWW Rfe SyncdRR
Relax acsdrr032 No ACSyncdRR
Safe=Fre SyncsWW LwSyncsWW
Time acsdrr032 91.76
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr033.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr033
"Fre SyncdWR Fre SyncsWW Rfe SyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;}
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 (x=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 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 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test acsdrr033 Allowed
Histogram (15 states)
298284:>0:r3=1; 2:r1=0; 2:r3=1; x=2;
219679:>0:r3=2; 2:r1=0; 2:r3=1; x=2;
236159:>0:r3=1; 2:r1=1; 2:r3=0; x=2;
2830488:>0:r3=2; 2:r1=1; 2:r3=1; x=2;
2141766:>0:r3=1; 2:r1=1; 2:r3=1; x=2;
16543820:>0:r3=0; 2:r1=1; 2:r3=1; x=2;
7955000:>0:r3=2; 2:r1=1; 2:r3=0; x=2;
51378455:>0:r3=0; 2:r1=0; 2:r3=0; x=2;
37619429:>0:r3=0; 2:r1=2; 2:r3=1; x=2;
35907059:>0:r3=2; 2:r1=2; 2:r3=0; x=2;
3446830:>0:r3=1; 2:r1=2; 2:r3=1; x=2;
17950578:>0:r3=1; 2:r1=0; 2:r3=0; x=2;
84480521:>0:r3=2; 2:r1=2; 2:r3=1; x=2;
77746175:>0:r3=0; 2:r1=0; 2:r3=1; x=2;
61245757:>0:r3=2; 2:r1=0; 2:r3=0; x=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=9fee6cd32468b8b76fc6ca805e427cad
Cycle=Fre SyncdWR Fre SyncsWW Rfe SyncdRR
Relax acsdrr033 No ACSyncdRR
Safe=Fre SyncsWW SyncdWR
Time acsdrr033 78.76
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr034.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr034
"Fre SyncdWW Wse LwSyncdWW Rfe SyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | lwsync | lwz r3,0(r4) ;
li r3,1 | li r3,1 | ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (x=2 /\ 2:r1=1 /\ 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 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test acsdrr034 Allowed
Histogram (7 states)
8675554:>2:r1=0; 2:r3=1; x=1;
33964500:>2:r1=0; 2:r3=0; x=2;
105306412:>2:r1=0; 2:r3=1; x=2;
27191486:>2:r1=1; 2:r3=0; x=1;
12869541:>2:r1=1; 2:r3=1; x=2;
92423503:>2:r1=1; 2:r3=1; x=1;
119569004:>2:r1=0; 2:r3=0; x=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=27d7745baac632fe4aea9c285d538d4c
Cycle=Fre SyncdWW Wse LwSyncdWW Rfe SyncdRR
Relax acsdrr034 No ACSyncdRR
Safe=Fre Wse SyncdWW LwSyncdWW
Time acsdrr034 76.07
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr035.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr035
"Fre LwSyncdWW Wse LwSyncdWW Rfe SyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
lwsync | lwsync | lwz r3,0(r4) ;
li r3,1 | li r3,1 | ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (x=2 /\ 2:r1=1 /\ 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 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test acsdrr035 Allowed
Histogram (7 states)
5542407:>2:r1=0; 2:r3=1; x=1;
17021722:>2:r1=1; 2:r3=1; x=2;
37160750:>2:r1=0; 2:r3=0; x=2;
25906168:>2:r1=1; 2:r3=0; x=1;
115725501:>2:r1=0; 2:r3=0; x=1;
86658268:>2:r1=1; 2:r3=1; x=1;
111985184:>2:r1=0; 2:r3=1; x=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=9477b1b1723232b68b25f79dd7a2be1b
Cycle=Fre LwSyncdWW Wse LwSyncdWW Rfe SyncdRR
Relax acsdrr035 No ACSyncdRR
Safe=Fre Wse LwSyncdWW
Time acsdrr035 76.40
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr036.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr036
"Fre LwSyncdWW Rfe SyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | sync ;
lwsync | lwz r3,0(r4) ;
li r3,1 | ;
stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0)
Generated assembler
_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(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test acsdrr036 Allowed
Histogram (3 states)
285411902:>1:r1=1; 1:r3=1;
307248173:>1:r1=0; 1:r3=0;
47339925:>1:r1=0; 1:r3=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (1:r1=1 /\ 1:r3=0) is NOT validated
Hash=b45ef7dfb9b495b3b934e3202a3ae026
Cycle=Fre LwSyncdWW Rfe SyncdRR
Relax acsdrr036 No ACSyncdRR
Safe=Fre LwSyncdWW
Time acsdrr036 76.67
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr037.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr037
"Fre LwSyncdWW Rfe SyncdRR Fre LwSyncdWW Rfe SyncdRR"
{0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;}
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 ;
lwsync | lwz r3,0(r4) | lwsync | lwz r3,0(r4) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 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 6,1
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 31,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test acsdrr037 Allowed
Histogram (15 states)
877303:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
1167958:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
973276:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
1188566:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
13649919:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
4385281:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
14141571:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
35830138:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
17662559:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
16974610:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
36855900:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
40703227:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
27786492:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
66223039:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
41580161:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=3a636427bd7edc2c2ac8a1c2b3f4438b
Cycle=Fre LwSyncdWW Rfe SyncdRR Fre LwSyncdWW Rfe SyncdRR
Relax acsdrr037 No ACSyncdRR
Safe=Fre LwSyncdWW
Time acsdrr037 89.96
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr038.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr038
"Fre LwSyncsWW Rfe SyncdRR Fre LwSyncdWW Rfe SyncdRR"
{0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;}
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 ;
lwsync | lwz r3,0(r4) | lwsync | lwz r3,0(r4) ;
li r3,2 | | li r3,1 | ;
stw r3,0(r2) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 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 5,1
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 7,1
_litmus_P0_1_: stw 7,0(9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test acsdrr038 Allowed
Histogram (33 states)
396 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
157967:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
107950:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
380776:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
216568:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
3531708:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
726315:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
609187:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
307810:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
2051980:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
1830069:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
2979170:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
545684:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
3757282:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
1100522:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
623773:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
2252201:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
1860077:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
3186458:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
23319003:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
27192356:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
171475:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
26947753:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
1286039:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
2815783:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
16899191:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
1305452:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
20753372:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
58284652:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
38662992:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
35995237:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
27248933:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
12891869:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=321edf48bccde0acdebe52eab9a80f96
Cycle=Fre LwSyncsWW Rfe SyncdRR Fre LwSyncdWW Rfe SyncdRR
Relax acsdrr038 No ACSyncdRR
Safe=Fre LwSyncsWW LwSyncdWW
Time acsdrr038 92.94
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr039.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr039
"Fre SyncdWR Fre LwSyncdWW Rfe SyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | lwsync | lwz r3,0(r4) ;
lwz r3,0(r4) | li r3,1 | ;
| stw r3,0(r4) | ;
exists (0:r3=0 /\ 2:r1=1 /\ 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 4,1
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,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 acsdrr039 Allowed
Histogram (7 states)
3731598:>0:r3=1; 2:r1=0; 2:r3=1;
27210458:>0:r3=1; 2:r1=1; 2:r3=0;
51190605:>0:r3=0; 2:r1=0; 2:r3=0;
21644174:>0:r3=0; 2:r1=1; 2:r3=1;
111262369:>0:r3=0; 2:r1=0; 2:r3=1;
102919914:>0:r3=1; 2:r1=0; 2:r3=0;
82040882:>0:r3=1; 2:r1=1; 2:r3=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=4123ecd9a851b7f1f3f7bbe069dac98e
Cycle=Fre SyncdWR Fre LwSyncdWW Rfe SyncdRR
Relax acsdrr039 No ACSyncdRR
Safe=Fre SyncdWR LwSyncdWW
Time acsdrr039 77.30
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr040.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr040
"Fre SyncsWR Fre LwSyncdWW Rfe SyncdRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 2:r4=y;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | lwsync | lwz r3,0(r4) ;
lwz r3,0(r2) | li r3,1 | ;
| stw r3,0(r4) | ;
exists (y=2 /\ 0:r3=1 /\ 2:r1=1 /\ 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 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 5,0(9)
Test acsdrr040 Allowed
Histogram (13 states)
2400667:>0:r3=2; 2:r1=1; 2:r3=2; y=2;
125768:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
3275159:>0:r3=1; 2:r1=0; 2:r3=1; y=1;
1015012:>0:r3=2; 2:r1=0; 2:r3=2; y=2;
7923588:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
19842809:>0:r3=1; 2:r1=1; 2:r3=2; y=2;
29247710:>0:r3=1; 2:r1=0; 2:r3=2; y=1;
63255512:>0:r3=1; 2:r1=0; 2:r3=0; y=1;
62969052:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
77765400:>0:r3=1; 2:r1=1; 2:r3=1; y=1;
56172710:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
50003308:>0:r3=1; 2:r1=0; 2:r3=2; y=2;
26003305:>0:r3=1; 2:r1=1; 2:r3=2; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=69a9c426befcce92245a44ffe29944c4
Cycle=Fre SyncsWR Fre LwSyncdWW Rfe SyncdRR
Relax acsdrr040 No ACSyncdRR
Safe=Fre SyncsWR LwSyncdWW
Time acsdrr040 76.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr041.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr041
"Fre LwSyncsWW Rfe SyncdRR Fre LwSyncsWW Rfe SyncdRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
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 ;
lwsync | lwz r3,0(r4) | lwsync | 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 6,1
_litmus_P2_1_: stw 6,0(9)
_litmus_P2_2_: lwsync
_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 7,1
_litmus_P0_1_: stw 7,0(9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test acsdrr041 Allowed
Histogram (72 states)
338 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
344 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
9221 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
383 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
263 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
259 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
536 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
22874 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
17632 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
17738 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
22922 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
6599 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
243672:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
34685 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
50999 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
165019:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
191072:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
112714:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
103690:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
36168 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
92797 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
107880:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
468452:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
224021:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
95322 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1339255:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1277497:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
111788:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1312782:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
402898:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
104242:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
490561:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2648762:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1027780:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
3741241:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
4461185:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
409244:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1344275:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
3269223:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2457987:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
2666183:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
111298:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
103863:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
2343008:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
684830:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
3871354:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
47353 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1820316:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
2362287:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1116681:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
22245985:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
997927:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
138442:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
258935:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
21364907:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
107421:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1733067:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
2180891:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
43801553:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
635017:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
1180894:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
4546476:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
22219363:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
3030825:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
53182902:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1009343:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1298302:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
21589531:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
17159805:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
21302102:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
17247325:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
21217494:>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=16ba9e829ae27807908998bcbb8a074d
Cycle=Fre LwSyncsWW Rfe SyncdRR Fre LwSyncsWW Rfe SyncdRR
Relax acsdrr041 No ACSyncdRR
Safe=Fre LwSyncsWW
Time acsdrr041 94.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/acsdrr042.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acsdrr042
"Fre SyncdWR Fre LwSyncsWW Rfe SyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | lwsync | lwz r3,0(r4) ;
lwz r3,0(r4) | li r3,2 | ;
| stw r3,0(r2) | ;
exists (x=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 5,1
_litmus_P1_1_: stw 5,0(9)
_litmus_P1_2_: lwsync
_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 acsdrr042 Allowed
Histogram (15 states)
19308 :>0:r3=1; 2:r1=1; 2:r3=0; x=2;
91283 :>0:r3=1; 2:r1=0; 2:r3=1; x=2;
421382:>0:r3=2; 2:r1=0; 2:r3=1; x=2;
417135:>0:r3=1; 2:r1=1; 2:r3=1; x=2;
881413:>0:r3=1; 2:r1=2; 2:r3=1; x=2;
6257733:>0:r3=0; 2:r1=1; 2:r3=1; x=2;
1765362:>0:r3=2; 2:r1=1; 2:r3=0; x=2;
6249393:>0:r3=1; 2:r1=0; 2:r3=0; x=2;
1838781:>0:r3=2; 2:r1=1; 2:r3=1; x=2;
45387243:>0:r3=2; 2:r1=2; 2:r3=0; x=2;
49157268:>0:r3=0; 2:r1=2; 2:r3=1; x=2;
51376228:>0:r3=0; 2:r1=0; 2:r3=0; x=2;
86124233:>0:r3=2; 2:r1=2; 2:r3=1; x=2;
76777757:>0:r3=0; 2:r1=0; 2:r3=1; x=2;
73235481:>0:r3=2; 2:r1=0; 2:r3=0; x=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=072bd75a46e56407102445eff71eb534
Cycle=Fre SyncdWR Fre LwSyncsWW Rfe SyncdRR
Relax acsdrr042 No ACSyncdRR
Safe=Fre SyncdWR LwSyncsWW
Time acsdrr042 77.33
$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 18:59:31 GMT 2009