Tue Dec 22 17:21:21 GMT 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr000
"Fre SyncdWW Rfe PodRR"
{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) | lwz r3,0(r4) ;
sync | ;
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_: 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 podrr000 Allowed
Histogram (4 states)
54328 :>1:r1=1; 1:r3=0;
77588197:>1:r1=0; 1:r3=1;
320111446:>1:r1=0; 1:r3=0;
242246029:>1:r1=1; 1:r3=1;
Ok
Witnesses
Positive: 54328, Negative: 639945672
Condition exists (1:r1=1 /\ 1:r3=0) is validated
Hash=78d7a77bf8b1a9bd43cfddf06e35d5d3
Cycle=Fre SyncdWW Rfe PodRR
Relax podrr000 Ok PodRR
Safe=Fre BCSyncdWW
Time podrr000 80.49
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr001
"Fre SyncdWW Rfe PodRR Fre SyncdWW Rfe PodRR"
{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) | lwz r3,0(r4) | stw r1,0(r2) | lwz r3,0(r4) ;
sync | | sync | ;
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_: 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_: 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 podrr001 Allowed
Histogram (16 states)
2275 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0;
1312786:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
2299629:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
2671330:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
4343351:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
26720760:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
16632168:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
21349953:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
22457388:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
25131195:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
86409684:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
3304267:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
18577745:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
36423597:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
40764401:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
11599471:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
Ok
Witnesses
Positive: 2275, Negative: 319997725
Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated
Hash=2e6b2a124722ed948c8f7dc35dc4b80f
Cycle=Fre SyncdWW Rfe PodRR Fre SyncdWW Rfe PodRR
Relax podrr001 Ok PodRR
Safe=Fre BCSyncdWW
Time podrr001 92.65
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr002
"Fre SyncsWW Rfe PodRR Fre SyncdWW Rfe PodRR"
{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) | lwz r3,0(r4) | stw r1,0(r2) | lwz r3,0(r4) ;
sync | | sync | ;
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_: 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_: 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 podrr002 Allowed
Histogram (36 states)
3543 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
2184 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
24953 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
3596 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
72018 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
83248 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
85984 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
327872:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
1753467:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
2830986:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
3746298:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
940977:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
1215265:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
2951044:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
5796675:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
2250337:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
26040158:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
9716018:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
4224048:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
4075417:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
2303919:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
2227950:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
4938230:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
20846156:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
5478899:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
2401394:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
4376136:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
10640145:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
6004292:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
22868260:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
72655728:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
21385394:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
8375162:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
31263484:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
16385209:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
21705554:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
Ok
Witnesses
Positive: 3596, Negative: 319996404
Condition exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated
Hash=c594109cf9f75c58c9eec5a696ceb0a0
Cycle=Fre SyncsWW Rfe PodRR Fre SyncdWW Rfe PodRR
Relax podrr002 Ok PodRR
Safe=Fre BCSyncsWW BCSyncdWW
Time podrr002 91.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr003
"Fre SyncdWW Rfe SyncdRW Rfe PodRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;}
P0 | P1 | P2 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | lwz r3,0(r4) ;
sync | li r3,1 | ;
li r3,1 | stw r3,0(r4) | ;
stw r3,0(r4) | | ;
exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwz 31,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 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 podrr003 Allowed
Histogram (8 states)
1873 :>1:r1=1; 2:r1=1; 2:r3=0;
8220048:>1:r1=1; 2:r1=1; 2:r3=1;
85156107:>1:r1=0; 2:r1=1; 2:r3=1;
20980047:>1:r1=1; 2:r1=0; 2:r3=0;
19161907:>1:r1=0; 2:r1=0; 2:r3=1;
79365961:>1:r1=1; 2:r1=0; 2:r3=1;
139482745:>1:r1=0; 2:r1=0; 2:r3=0;
47631312:>1:r1=0; 2:r1=1; 2:r3=0;
Ok
Witnesses
Positive: 1873, Negative: 399998127
Condition exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0) is validated
Hash=3d48b5b0d8516d3d909b0a4f66959c71
Cycle=Fre SyncdWW Rfe SyncdRW Rfe PodRR
Relax podrr003 Ok PodRR
Safe=Fre BCSyncdWW BCSyncdRW
Time podrr003 73.67
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr004
"Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe PodRR"
{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) | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | sync | lwz r3,0(r4) ;
sync | li r3,1 | li r3,1 | ;
li r3,1 | stw r3,0(r4) | stw r3,0(r4) | ;
stw r3,0(r4) | | | ;
exists (1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwz 4,0(9)
_litmus_P2_0_: lwz 4,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: li 5,1
_litmus_P2_3_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 4,1
_litmus_P1_3_: stw 4,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 podrr004 Allowed
Histogram (16 states)
83 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=0;
78428 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1;
16991086:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0;
9184044:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1;
1013310:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0;
22880990:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1;
530123:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0;
2749761:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0;
28556961:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0;
4819455:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1;
36987498:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1;
5262876:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1;
73228705:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0;
34180811:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1;
54433720:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0;
29102149:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1;
Ok
Witnesses
Positive: 83, Negative: 319999917
Condition exists (1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0) is validated
Hash=b2067185c885838837d33372d57790fb
Cycle=Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe PodRR
Relax podrr004 Ok PodRR
Safe=Fre BCSyncdWW BCSyncdRW
Time podrr004 91.47
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr005
"Fre SyncsWW Rfe SyncdRW Rfe SyncdRW Rfe PodRR"
{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) | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | sync | lwz r3,0(r4) ;
sync | li r3,1 | li r3,1 | ;
li r3,2 | stw r3,0(r4) | stw r3,0(r4) | ;
stw r3,0(r2) | | | ;
exists (z=2 /\ 1:r1=2 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwz 4,0(9)
_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_: lwz 4,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 5,1
_litmus_P1_3_: stw 5,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 podrr005 Allowed
Histogram (36 states)
157 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=0; z=2;
170 :>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
131 :>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=0; z=2;
971 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
625868:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
1154777:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
2032629:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
2384435:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
2053181:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
327254:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
372344:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
1770133:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
597745:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
827195:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
7862876:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
5114276:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
945064:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
795077:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
1424211:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
5096768:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
4857451:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
1725620:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; z=2;
1087854:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
6043513:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
13680435:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
32863078:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
18216136:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
49009095:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
46564382:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
9288675:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
29496721:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
3112453:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
5258695:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
5841971:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
25360980:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
34207679:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
Ok
Witnesses
Positive: 131, Negative: 319999869
Condition exists (z=2 /\ 1:r1=2 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0) is validated
Hash=1a4d6f8ada041391fb8c242b28f54910
Cycle=Fre SyncsWW Rfe SyncdRW Rfe SyncdRW Rfe PodRR
Relax podrr005 Ok PodRR
Safe=Fre BCSyncsWW BCSyncdRW
Time podrr005 91.13
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr006
"Fre SyncsWW Rfe SyncdRW Rfe PodRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 2:r4=y;}
P0 | P1 | P2 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | lwz r3,0(r4) ;
sync | li r3,1 | ;
li r3,2 | stw r3,0(r4) | ;
stw r3,0(r2) | | ;
exists (y=2 /\ 1:r1=2 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwz 31,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 4,1
_litmus_P1_3_: stw 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 podrr006 Allowed
Histogram (18 states)
4127 :>1:r1=2; 2:r1=1; 2:r3=1; y=2;
4576 :>1:r1=1; 2:r1=1; 2:r3=0; y=2;
4622 :>1:r1=2; 2:r1=1; 2:r3=0; y=2;
184578:>1:r1=1; 2:r1=1; 2:r3=1; y=2;
1636807:>1:r1=0; 2:r1=0; 2:r3=2; y=2;
864507:>1:r1=0; 2:r1=0; 2:r3=1; y=2;
3831829:>1:r1=1; 2:r1=1; 2:r3=2; y=2;
3314491:>1:r1=1; 2:r1=0; 2:r3=1; y=2;
7152528:>1:r1=2; 2:r1=0; 2:r3=1; y=2;
15722842:>1:r1=1; 2:r1=0; 2:r3=0; y=2;
16543615:>1:r1=0; 2:r1=1; 2:r3=1; y=2;
43785824:>1:r1=0; 2:r1=1; 2:r3=2; y=2;
17654401:>1:r1=2; 2:r1=1; 2:r3=2; y=2;
41444453:>1:r1=2; 2:r1=0; 2:r3=0; y=2;
4306640:>1:r1=1; 2:r1=0; 2:r3=2; y=2;
42115755:>1:r1=0; 2:r1=1; 2:r3=0; y=2;
104110402:>1:r1=0; 2:r1=0; 2:r3=0; y=2;
97318003:>1:r1=2; 2:r1=0; 2:r3=2; y=2;
Ok
Witnesses
Positive: 4622, Negative: 399995378
Condition exists (y=2 /\ 1:r1=2 /\ 2:r1=1 /\ 2:r3=0) is validated
Hash=f5e5097c67500c52603a1c0158bb8551
Cycle=Fre SyncsWW Rfe SyncdRW Rfe PodRR
Relax podrr006 Ok PodRR
Safe=Fre BCSyncsWW BCSyncdRW
Time podrr006 77.11
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr007
"Fre SyncdWW Rfe SyncsRW Rfe SyncdRW Rfe PodRR"
{0:r2=z; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | sync | lwz r3,0(r4) ;
sync | li r3,2 | li r3,1 | ;
li r3,1 | stw r3,0(r2) | stw r3,0(r4) | ;
stw r3,0(r4) | | | ;
exists (x=2 /\ 1:r1=1 /\ 2:r1=2 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwz 4,0(9)
_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_: lwz 5,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,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 podrr007 Allowed
Histogram (36 states)
350 :>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=0; x=2;
262 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; x=2;
465 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=0; x=2;
4929 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; x=1;
145 :>1:r1=1; 2:r1=2; 3:r1=1; 3:r3=0; x=2;
675404:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
1246724:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
1341656:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=1;
14820744:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=1;
402908:>1:r1=1; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
604205:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
1112483:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
2962645:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
11068860:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
2097439:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
2322244:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=0; x=1;
14906517:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=1;
2313686:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1;
4104437:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
19635517:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
40076513:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=1;
9395699:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
7666465:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=1;
3625076:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
13178320:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
3016858:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
12194222:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
20919562:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
7430711:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=1;
28119891:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1;
45774050:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1;
9257389:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
3386395:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
12077494:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
20896050:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1;
3363685:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
Ok
Witnesses
Positive: 145, Negative: 319999855
Condition exists (x=2 /\ 1:r1=1 /\ 2:r1=2 /\ 3:r1=1 /\ 3:r3=0) is validated
Hash=c22fcb545cb7b0f7f27c11adc702bd5e
Cycle=Fre SyncdWW Rfe SyncsRW Rfe SyncdRW Rfe PodRR
Relax podrr007 Ok PodRR
Safe=Fre BCSyncsRW BCSyncdWW BCSyncdRW
Time podrr007 91.71
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr008.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr008
"Fre SyncsWW Rfe PodRR Fre SyncsWW Rfe PodRR"
{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) | lwz r3,0(r4) | stw r1,0(r2) | lwz r3,0(r4) ;
sync | | sync | ;
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_: 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_: 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 podrr008 Allowed
Histogram (81 states)
1035 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
888 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
7656 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
7397 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1366 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
2094 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
2838 :>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
5365 :>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
7744 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
4720 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
4779 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
5516 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
3735 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
2306 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
36308 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
37455 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
35465 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1915 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
6063 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
6094 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
52304 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
5796 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
48092 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
34110 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
47735 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
48821 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
47291 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
37661 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
712184:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
39704 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
38967 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
36221 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
717341:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
692125:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
111185:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
717801:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
109216:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1739377:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
4302219:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
676667:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
2736133:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1153177:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
668335:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
3250753:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
2475736:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
2725351:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
3308780:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
4238702:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
8325629:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
2386479:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
2363864:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
2657415:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
3220979:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
3272345:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1750764:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1645878:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
3201069:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
2388660:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
8144577:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
8340687:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
8124916:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
4224224:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
3169920:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
2734172:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
15661019:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
24717909:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1709639:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
15445181:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
24640612:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1708014:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
8367698:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
8342530:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
3371999:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
3226021:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
62869418:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1167644:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1748379:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
4319461:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
8537660:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
28912650:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
8350065:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
Ok
Witnesses
Positive: 2838, Negative: 319997162
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is validated
Hash=58c192e74d841e0ccb20b3014a58a473
Cycle=Fre SyncsWW Rfe PodRR Fre SyncsWW Rfe PodRR
Relax podrr008 Ok PodRR
Safe=Fre BCSyncsWW
Time podrr008 98.02
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr009.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr009
"Fre SyncdWW Rfe SyncsRW Rfe PodRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;}
P0 | P1 | P2 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | lwz r3,0(r4) ;
sync | li r3,2 | ;
li r3,1 | stw r3,0(r2) | ;
stw r3,0(r4) | | ;
exists (x=2 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwz 31,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,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 podrr009 Allowed
Histogram (18 states)
1028 :>1:r1=1; 2:r1=2; 2:r3=0; x=2;
2768 :>1:r1=1; 2:r1=1; 2:r3=0; x=2;
2630 :>1:r1=0; 2:r1=1; 2:r3=0; x=2;
3530 :>1:r1=0; 2:r1=2; 2:r3=0; x=2;
325505:>1:r1=0; 2:r1=1; 2:r3=0; x=1;
4594791:>1:r1=0; 2:r1=0; 2:r3=1; x=1;
7957617:>1:r1=0; 2:r1=1; 2:r3=1; x=2;
13565879:>1:r1=0; 2:r1=0; 2:r3=1; x=2;
27937041:>1:r1=0; 2:r1=2; 2:r3=1; x=1;
46268204:>1:r1=0; 2:r1=1; 2:r3=1; x=1;
22113050:>1:r1=0; 2:r1=2; 2:r3=1; x=2;
51760785:>1:r1=0; 2:r1=2; 2:r3=0; x=1;
28261560:>1:r1=1; 2:r1=0; 2:r3=1; x=2;
26289045:>1:r1=0; 2:r1=0; 2:r3=0; x=2;
10773007:>1:r1=1; 2:r1=2; 2:r3=1; x=2;
107782627:>1:r1=0; 2:r1=0; 2:r3=0; x=1;
18701125:>1:r1=1; 2:r1=0; 2:r3=0; x=2;
33659808:>1:r1=1; 2:r1=1; 2:r3=1; x=2;
Ok
Witnesses
Positive: 1028, Negative: 399998972
Condition exists (x=2 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=0) is validated
Hash=d6249053a9b844d8e7a3045b38500a3a
Cycle=Fre SyncdWW Rfe SyncsRW Rfe PodRR
Relax podrr009 Ok PodRR
Safe=Fre BCSyncsRW BCSyncdWW
Time podrr009 77.49
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr010
"Fre SyncdWW Rfe SyncdRW Rfe SyncsRW Rfe PodRR"
{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) | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | sync | lwz r3,0(r4) ;
sync | li r3,1 | li r3,2 | ;
li r3,1 | stw r3,0(r4) | stw r3,0(r2) | ;
stw r3,0(r4) | | | ;
exists (y=2 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwz 4,0(9)
_litmus_P2_0_: lwz 5,0(9)
_litmus_P2_1_: sync
_litmus_P2_2_: li 11,2
_litmus_P2_3_: stw 11,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 4,1
_litmus_P1_3_: 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 podrr010 Allowed
Histogram (36 states)
106 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=0; y=2;
65 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; y=2;
133 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; y=2;
72 :>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=0; y=2;
4430 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; y=1;
835296:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
1848167:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
445878:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
5630866:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
334435:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
526322:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
3358667:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
2639501:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
2567966:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=2;
606748:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
5858234:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
214962:>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
4919746:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=2;
6722219:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
22794896:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
5565908:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=1;
20177770:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
12725733:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=1;
11578950:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
20364832:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
4245058:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; y=2;
36900606:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
13950057:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
19987914:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
34887617:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
19306348:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
17807128:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; y=2;
12273872:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
3922835:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
23887766:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=1;
3108897:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
Ok
Witnesses
Positive: 72, Negative: 319999928
Condition exists (y=2 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r3=0) is validated
Hash=fcb68021656d7cbdb455ef5bd2648d65
Cycle=Fre SyncdWW Rfe SyncdRW Rfe SyncsRW Rfe PodRR
Relax podrr010 Ok PodRR
Safe=Fre BCSyncsRW BCSyncdWW BCSyncdRW
Time podrr010 89.85
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr011.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr011
"Fre SyncsWW Rfe SyncdRW Rfe SyncsRW Rfe PodRR"
{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) | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | sync | lwz r3,0(r4) ;
sync | li r3,1 | li r3,2 | ;
li r3,2 | stw r3,0(r4) | stw r3,0(r2) | ;
stw r3,0(r2) | | | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwz 4,0(9)
_litmus_P2_0_: lwz 5,0(9)
_litmus_P2_1_: sync
_litmus_P2_2_: li 11,2
_litmus_P2_3_: stw 11,0(9)
_litmus_P1_0_: lwz 4,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 5,1
_litmus_P1_3_: stw 5,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 podrr011 Allowed
Histogram (81 states)
111 :>1:r1=2; 2:r1=1; 3:r1=2; 3:r3=0; x=2; y=2;
114 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=0; x=2; y=2;
99 :>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=0; x=2; y=2;
390 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=0; x=2; y=2;
275 :>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=0; x=2; y=2;
401 :>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
843 :>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
5095 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
323 :>1:r1=2; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
281 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
187 :>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=0; x=2; y=2;
3293 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
104 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; x=2; y=2;
217 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; x=2; y=2;
3397 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
5520 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; x=1; y=2;
7082 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=0; x=1; y=2;
2984 :>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
66884 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
52509 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
1446276:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
322958:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
717076:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
115767:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
754181:>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
771207:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
838291:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
1343636:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
292418:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
992496:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
138306:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
486790:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
2663847:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
842048:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
1078812:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
3680245:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
980540:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
2485208:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
2298665:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
709295:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
483690:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
1641046:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
778778:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
1060133:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
5854516:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
1594326:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
4543647:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=2; y=2;
1563523:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
2335080:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
1018573:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
515342:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
5785200:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
2265142:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2; y=2;
936748:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
1428713:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
915872:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
443760:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
757221:>1:r1=2; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
3740071:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
1655611:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
12608831:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
1591510:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
10530283:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
16513720:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; x=2; y=2;
6084996:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
3851488:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
695158:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
2333528:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
8991458:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
21872620:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
23515151:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
21844252:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
4091038:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; x=2; y=2;
22915833:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
11988437:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1; y=2;
7817414:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
9447442:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
15762793:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
15879020:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
7216790:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
32023075:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
Ok
Witnesses
Positive: 111, Negative: 319999889
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r3=0) is validated
Hash=a463a88f960487eded38b9c473eec1b5
Cycle=Fre SyncsWW Rfe SyncdRW Rfe SyncsRW Rfe PodRR
Relax podrr011 Ok PodRR
Safe=Fre BCSyncsWW BCSyncsRW BCSyncdRW
Time podrr011 93.77
$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 17:38:51 GMT 2009