Wed Dec 30 10:35:30 GMT 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe036.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe036
"SyncdWW Wse SyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) ;
sync | sync ;
li r3,1 | li r3,1 ;
stw r3,0(r4) | stw r3,0(r4) ;
exists (x=2 /\ y=2)
Generated assembler
_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 5,2
_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 safe036 Allowed
Histogram (3 states)
53066256:>x=1; y=1;
293282251:>x=1; y=2;
293651493:>x=2; y=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ y=2) is NOT validated
Hash=b13e0c20b3a95ec28cc7a23efa1563b6
Cycle=SyncdWW Wse SyncdWW Wse
Relax safe036 No
Safe=Wse SyncdWW
Time safe036 63.20
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe037.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe037
"SyncdWW Wse SyncdWW Wse SyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
sync | sync | sync ;
li r3,1 | li r3,1 | li r3,1 ;
stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ;
exists (x=2 /\ y=2 /\ z=2)
Generated assembler
_litmus_P2_0_: li 4,2
_litmus_P2_1_: stw 4,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 3,1
_litmus_P2_4_: stw 3,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 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test safe037 Allowed
Histogram (7 states)
23566814:>x=2; y=1; z=2;
22961066:>x=2; y=2; z=1;
23937647:>x=1; y=2; z=2;
6068397:>x=1; y=1; z=1;
108258233:>x=2; y=1; z=1;
108021449:>x=1; y=1; z=2;
107186394:>x=1; y=2; z=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ z=2) is NOT validated
Hash=29e092e26d25015c351a682f181e1b0f
Cycle=SyncdWW Wse SyncdWW Wse SyncdWW Wse
Relax safe037 No
Safe=Wse SyncdWW
Time safe037 68.90
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe038.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe038
"LwSyncdWW Wse SyncdWW Wse SyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
sync | sync | lwsync ;
li r3,1 | li r3,1 | li r3,1 ;
stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ;
exists (x=2 /\ y=2 /\ z=2)
Generated assembler
_litmus_P2_0_: li 4,2
_litmus_P2_1_: stw 4,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 3,1
_litmus_P2_4_: stw 3,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 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test safe038 Allowed
Histogram (7 states)
5036042:>x=1; y=1; z=1;
29226605:>x=2; y=2; z=1;
103355169:>x=1; y=1; z=2;
99559845:>x=1; y=2; z=1;
23522140:>x=1; y=2; z=2;
112028073:>x=2; y=1; z=1;
27272126:>x=2; y=1; z=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ z=2) is NOT validated
Hash=9fdaf07975754951c834724222b34025
Cycle=LwSyncdWW Wse SyncdWW Wse SyncdWW Wse
Relax safe038 No
Safe=Wse SyncdWW LwSyncdWW
Time safe038 66.05
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe040.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe040
"SyncdWR Fre SyncdWW Wse SyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
sync | sync | sync ;
li r3,1 | li r3,1 | lwz r3,0(r4) ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (y=2 /\ z=2 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: li 30,2
_litmus_P2_1_: stw 30,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 3,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 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test safe040 Allowed
Histogram (7 states)
39393474:>2:r3=0; y=1; z=2;
3828490:>2:r3=1; y=1; z=1;
23435273:>2:r3=1; y=2; z=2;
33176642:>2:r3=0; y=2; z=1;
92795868:>2:r3=1; y=1; z=2;
94607122:>2:r3=1; y=2; z=1;
112763131:>2:r3=0; y=1; z=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ z=2 /\ 2:r3=0) is NOT validated
Hash=60904a5b2739e8950875099ac77c27af
Cycle=SyncdWR Fre SyncdWW Wse SyncdWW Wse
Relax safe040 No
Safe=Fre Wse SyncdWW SyncdWR
Time safe040 65.26
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe045.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe045
"LwSyncdWW Wse SyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) ;
sync | lwsync ;
li r3,1 | li r3,1 ;
stw r3,0(r4) | stw r3,0(r4) ;
exists (x=2 /\ y=2)
Generated assembler
_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 5,2
_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 safe045 Allowed
Histogram (3 states)
34925206:>x=1; y=1;
293299035:>x=1; y=2;
311775759:>x=2; y=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ y=2) is NOT validated
Hash=68b87fd4beebe403e166c8646f0170ab
Cycle=LwSyncdWW Wse SyncdWW Wse
Relax safe045 No
Safe=Wse SyncdWW LwSyncdWW
Time safe045 64.25
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe046.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe046
"LwSyncdWW Wse LwSyncdWW Wse SyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
lwsync | sync | lwsync ;
li r3,1 | li r3,1 | li r3,1 ;
stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ;
exists (x=2 /\ y=2 /\ z=2)
Generated assembler
_litmus_P2_0_: li 4,2
_litmus_P2_1_: stw 4,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 3,1
_litmus_P2_4_: stw 3,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 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test safe046 Allowed
Histogram (7 states)
3699403:>x=1; y=1; z=1;
26783591:>x=2; y=1; z=2;
33054976:>x=2; y=2; z=1;
103625542:>x=1; y=2; z=1;
107339743:>x=2; y=1; z=1;
96032932:>x=1; y=1; z=2;
29463813:>x=1; y=2; z=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ z=2) is NOT validated
Hash=ef787314c1fb4635934ec5bee20106c0
Cycle=LwSyncdWW Wse LwSyncdWW Wse SyncdWW Wse
Relax safe046 No
Safe=Wse SyncdWW LwSyncdWW
Time safe046 68.07
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe048.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe048
"SyncdWR Fre LwSyncdWW Wse SyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
lwsync | sync | sync ;
li r3,1 | li r3,1 | lwz r3,0(r4) ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (y=2 /\ z=2 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: li 30,2
_litmus_P2_1_: stw 30,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 3,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 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test safe048 Allowed
Histogram (7 states)
2171968:>2:r3=1; y=1; z=1;
39909426:>2:r3=0; y=1; z=2;
38803239:>2:r3=0; y=2; z=1;
96776754:>2:r3=1; y=2; z=1;
106957866:>2:r3=0; y=1; z=1;
84672378:>2:r3=1; y=1; z=2;
30708369:>2:r3=1; y=2; z=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ z=2 /\ 2:r3=0) is NOT validated
Hash=fded52f6a8a54c4d9bf3c0cde8ee353b
Cycle=SyncdWR Fre LwSyncdWW Wse SyncdWW Wse
Relax safe048 No
Safe=Fre Wse SyncdWW SyncdWR LwSyncdWW
Time safe048 64.11
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe069.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe069
"SyncdWR Fre SyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,1 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) ;
sync | sync ;
li r3,1 | lwz r3,0(r4) ;
stw r3,0(r4) | ;
exists (y=2 /\ 1:r3=0)
Generated assembler
_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 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 safe069 Allowed
Histogram (3 states)
32780834:>1:r3=1; y=1;
309764392:>1:r3=0; y=1;
297454774:>1:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (y=2 /\ 1:r3=0) is NOT validated
Hash=7da20a2ab953c9d18488d3f4e7841bb2
Cycle=SyncdWR Fre SyncdWW Wse
Relax safe069 No
Safe=Fre Wse SyncdWW SyncdWR
Time safe069 61.02
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe070.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe070
"LwSyncdWW Wse SyncdWR Fre SyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,1 | li r1,2 ;
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 /\ z=2 /\ 0:r3=0)
Generated assembler
_litmus_P2_0_: li 4,2
_litmus_P2_1_: stw 4,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 3,1
_litmus_P2_4_: stw 3,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 30,2
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test safe070 Allowed
Histogram (7 states)
27026215:>0:r3=1; x=2; z=2;
31351700:>0:r3=0; x=1; z=2;
46875374:>0:r3=0; x=2; z=1;
3119058:>0:r3=1; x=1; z=1;
96031367:>0:r3=1; x=2; z=1;
91955077:>0:r3=1; x=1; z=2;
103641209:>0:r3=0; x=1; z=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ z=2 /\ 0:r3=0) is NOT validated
Hash=41c68cedc1ddadab686061c793b3d241
Cycle=LwSyncdWW Wse SyncdWR Fre SyncdWW Wse
Relax safe070 No
Safe=Fre Wse SyncdWW SyncdWR LwSyncdWW
Time safe070 63.64
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe072.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe072
"SyncdWR Fre SyncdWR Fre SyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | li r1,2 ;
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 (z=2 /\ 0:r3=0 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: li 30,2
_litmus_P2_1_: stw 30,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 3,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 30,1
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test safe072 Allowed
Histogram (7 states)
1356910:>0:r3=1; 2:r3=1; z=1;
35051750:>0:r3=0; 2:r3=1; z=2;
53920262:>0:r3=0; 2:r3=0; z=1;
39960426:>0:r3=1; 2:r3=0; z=2;
93703467:>0:r3=1; 2:r3=0; z=1;
77915909:>0:r3=1; 2:r3=1; z=2;
98091276:>0:r3=0; 2:r3=1; z=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (z=2 /\ 0:r3=0 /\ 2:r3=0) is NOT validated
Hash=545ab7a6a327dd4d73e4f0fc0d60719e
Cycle=SyncdWR Fre SyncdWR Fre SyncdWW Wse
Relax safe072 No
Safe=Fre Wse SyncdWW SyncdWR
Time safe072 63.12
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe077.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe077
"SyncdWR Fre SyncsWR Fre SyncdWW Wse"
{0:r2=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
sync | sync | sync ;
lwz r3,0(r2) | li r3,1 | lwz r3,0(r4) ;
| stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 0:r3=1 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: li 30,2
_litmus_P2_1_: stw 30,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 3,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 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 4,0(9)
Test safe077 Allowed
Histogram (13 states)
111184:>0:r3=2; 2:r3=1; x=2; y=1;
19053855:>0:r3=1; 2:r3=2; x=1; y=1;
36606308:>0:r3=1; 2:r3=2; x=1; y=2;
63167764:>0:r3=1; 2:r3=1; x=2; y=1;
362796:>0:r3=2; 2:r3=2; x=2; y=1;
59707651:>0:r3=1; 2:r3=0; x=2; y=1;
64270009:>0:r3=1; 2:r3=0; x=1; y=1;
1680989:>0:r3=2; 2:r3=2; x=2; y=2;
35111893:>0:r3=1; 2:r3=2; x=2; y=1;
1410780:>0:r3=1; 2:r3=1; x=1; y=1;
77900257:>0:r3=1; 2:r3=1; x=1; y=2;
5408546:>0:r3=2; 2:r3=0; x=2; y=1;
35207968:>0:r3=1; 2:r3=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 2:r3=0) is NOT validated
Hash=90440690a11b718ea7844fef30ba96c5
Cycle=SyncdWR Fre SyncsWR Fre SyncdWW Wse
Relax safe077 No
Safe=Fre Wse SyncsWR SyncdWW SyncdWR
Time safe077 62.26
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe135.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe135
"LwSyncdWW Wse LwSyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) ;
lwsync | lwsync ;
li r3,1 | li r3,1 ;
stw r3,0(r4) | stw r3,0(r4) ;
exists (x=2 /\ y=2)
Generated assembler
_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 5,2
_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 safe135 Allowed
Histogram (3 states)
17001612:>x=1; y=1;
311278681:>x=2; y=1;
311719707:>x=1; y=2;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ y=2) is NOT validated
Hash=829af8195a1482485057a881cab011a8
Cycle=LwSyncdWW Wse LwSyncdWW Wse
Relax safe135 No
Safe=Wse LwSyncdWW
Time safe135 61.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe136.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe136
"LwSyncdWW Wse LwSyncdWW Wse LwSyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
lwsync | lwsync | lwsync ;
li r3,1 | li r3,1 | li r3,1 ;
stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ;
exists (x=2 /\ y=2 /\ z=2)
Generated assembler
_litmus_P2_0_: li 4,2
_litmus_P2_1_: stw 4,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 3,1
_litmus_P2_4_: stw 3,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 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test safe136 Allowed
Histogram (7 states)
33207388:>x=2; y=2; z=1;
2075038:>x=1; y=1; z=1;
34140136:>x=2; y=1; z=2;
34576193:>x=1; y=2; z=2;
99503453:>x=2; y=1; z=1;
98614738:>x=1; y=1; z=2;
97883054:>x=1; y=2; z=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ z=2) is NOT validated
Hash=20a6a34b6dc3f52d89ffdf88575062ca
Cycle=LwSyncdWW Wse LwSyncdWW Wse LwSyncdWW Wse
Relax safe136 No
Safe=Wse LwSyncdWW
Time safe136 66.83
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe138.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe138
"SyncdWR Fre LwSyncdWW Wse LwSyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
lwsync | lwsync | sync ;
li r3,1 | li r3,1 | lwz r3,0(r4) ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (y=2 /\ z=2 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: li 30,2
_litmus_P2_1_: stw 30,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 3,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 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test safe138 Allowed
Histogram (7 states)
1335310:>2:r3=1; y=1; z=1;
37021372:>2:r3=0; y=2; z=1;
46636869:>2:r3=0; y=1; z=2;
93676747:>2:r3=1; y=2; z=1;
98578250:>2:r3=0; y=1; z=1;
87485688:>2:r3=1; y=1; z=2;
35265764:>2:r3=1; y=2; z=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ z=2 /\ 2:r3=0) is NOT validated
Hash=d9622bc66160015a9bfad53625a07803
Cycle=SyncdWR Fre LwSyncdWW Wse LwSyncdWW Wse
Relax safe138 No
Safe=Fre Wse SyncdWR LwSyncdWW
Time safe138 64.47
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe158.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe158
"SyncdWR Fre LwSyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,1 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) ;
lwsync | sync ;
li r3,1 | lwz r3,0(r4) ;
stw r3,0(r4) | ;
exists (y=2 /\ 1:r3=0)
Generated assembler
_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 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 safe158 Allowed
Histogram (3 states)
17933117:>1:r3=1; y=1;
315188321:>1:r3=1; y=2;
306878562:>1:r3=0; y=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (y=2 /\ 1:r3=0) is NOT validated
Hash=178cdf8fa414f9851e5cbee2c97136b0
Cycle=SyncdWR Fre LwSyncdWW Wse
Relax safe158 No
Safe=Fre Wse SyncdWR LwSyncdWW
Time safe158 68.14
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe160.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe160
"SyncdWR Fre SyncdWR Fre LwSyncdWW Wse"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | li r1,2 ;
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 (z=2 /\ 0:r3=0 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: li 30,2
_litmus_P2_1_: stw 30,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 3,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 30,1
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test safe160 Allowed
Histogram (7 states)
745031:>0:r3=1; 2:r3=1; z=1;
49506921:>0:r3=0; 2:r3=0; z=1;
82805944:>0:r3=1; 2:r3=1; z=2;
37630871:>0:r3=0; 2:r3=1; z=2;
87035214:>0:r3=1; 2:r3=0; z=1;
47077185:>0:r3=1; 2:r3=0; z=2;
95198834:>0:r3=0; 2:r3=1; z=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (z=2 /\ 0:r3=0 /\ 2:r3=0) is NOT validated
Hash=1aec03977a16ccd6a8c5fc1afed64860
Cycle=SyncdWR Fre SyncdWR Fre LwSyncdWW Wse
Relax safe160 No
Safe=Fre Wse SyncdWR LwSyncdWW
Time safe160 63.71
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe165.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe165
"SyncdWR Fre SyncsWR Fre LwSyncdWW Wse"
{0:r2=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | li r1,2 ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ;
sync | lwsync | sync ;
lwz r3,0(r2) | li r3,1 | lwz r3,0(r4) ;
| stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 0:r3=1 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: li 30,2
_litmus_P2_1_: stw 30,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 3,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 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 4,0(9)
Test safe165 Allowed
Histogram (13 states)
140484:>0:r3=2; 2:r3=1; x=2; y=1;
352021:>0:r3=2; 2:r3=2; x=2; y=1;
2046753:>0:r3=2; 2:r3=2; x=2; y=2;
504000:>0:r3=1; 2:r3=1; x=1; y=1;
12003964:>0:r3=1; 2:r3=2; x=1; y=1;
5945773:>0:r3=2; 2:r3=0; x=2; y=1;
38029972:>0:r3=1; 2:r3=2; x=2; y=2;
61736781:>0:r3=1; 2:r3=1; x=2; y=1;
79006158:>0:r3=1; 2:r3=1; x=1; y=2;
57726333:>0:r3=1; 2:r3=0; x=2; y=1;
33684535:>0:r3=1; 2:r3=2; x=2; y=1;
44006210:>0:r3=1; 2:r3=2; x=1; y=2;
64817016:>0:r3=1; 2:r3=0; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 2:r3=0) is NOT validated
Hash=c2358315f3b0a52cdef1288bea12e53f
Cycle=SyncdWR Fre SyncsWR Fre LwSyncdWW Wse
Relax safe165 No
Safe=Fre Wse SyncsWR SyncdWR LwSyncdWW
Time safe165 62.77
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe358.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe358
"SyncdWR Fre SyncdWR Fre"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,1 | li r1,1 ;
stw r1,0(r2) | stw r1,0(r2) ;
sync | sync ;
lwz r3,0(r4) | lwz r3,0(r4) ;
exists (0:r3=0 /\ 1:r3=0)
Generated assembler
_litmus_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 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 safe358 Allowed
Histogram (3 states)
24199710:>0:r3=1; 1:r3=1;
308456006:>0:r3=0; 1:r3=1;
307344284:>0:r3=1; 1:r3=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r3=0 /\ 1:r3=0) is NOT validated
Hash=5db67b28ae44dfb0497cda13c245c4e4
Cycle=SyncdWR Fre SyncdWR Fre
Relax safe358 No
Safe=Fre SyncdWR
Time safe358 77.80
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe359.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe359
"SyncdWR Fre SyncdWR Fre SyncdWR Fre"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | li r1,1 ;
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 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: li 4,1
_litmus_P2_1_: stw 4,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 3,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 31,1
_litmus_P0_1_: stw 31,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test safe359 Allowed
Histogram (7 states)
410975:>0:r3=1; 1:r3=1; 2:r3=1;
53166072:>0:r3=0; 1:r3=0; 2:r3=1;
53159719:>0:r3=0; 1:r3=1; 2:r3=0;
52479505:>0:r3=1; 1:r3=0; 2:r3=0;
80021960:>0:r3=1; 1:r3=1; 2:r3=0;
80603477:>0:r3=1; 1:r3=0; 2:r3=1;
80158292:>0:r3=0; 1:r3=1; 2:r3=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (0:r3=0 /\ 1:r3=0 /\ 2:r3=0) is NOT validated
Hash=1bb05ee290fb3d2f94afc422c308bf1a
Cycle=SyncdWR Fre SyncdWR Fre SyncdWR Fre
Relax safe359 No
Safe=Fre SyncdWR
Time safe359 72.76
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/safe360.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
safe360
"SyncsWR Fre SyncdWR Fre SyncdWR Fre"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y;}
P0 | P1 | P2 ;
li r1,2 | li r1,1 | li r1,1 ;
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 (y=2 /\ 0:r3=0 /\ 1:r3=0 /\ 2:r3=1)
Generated assembler
_litmus_P2_0_: li 11,1
_litmus_P2_1_: stw 11,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 4,0(9)
_litmus_P1_0_: li 30,1
_litmus_P1_1_: stw 30,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 3,0(9)
_litmus_P0_0_: li 30,2
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test safe360 Allowed
Histogram (13 states)
2800274:>0:r3=0; 1:r3=2; 2:r3=2; y=2;
106220:>0:r3=1; 1:r3=1; 2:r3=2; y=2;
79973 :>0:r3=1; 1:r3=2; 2:r3=2; y=2;
4457504:>0:r3=1; 1:r3=2; 2:r3=1; y=1;
226455:>0:r3=1; 1:r3=1; 2:r3=1; y=1;
6042139:>0:r3=1; 1:r3=0; 2:r3=2; y=2;
51409563:>0:r3=0; 1:r3=2; 2:r3=1; y=1;
58247244:>0:r3=1; 1:r3=0; 2:r3=1; y=2;
54636002:>0:r3=0; 1:r3=2; 2:r3=1; y=2;
16286088:>0:r3=1; 1:r3=2; 2:r3=1; y=2;
63830700:>0:r3=1; 1:r3=0; 2:r3=1; y=1;
79256537:>0:r3=0; 1:r3=1; 2:r3=1; y=1;
62621301:>0:r3=1; 1:r3=1; 2:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=0 /\ 1:r3=0 /\ 2:r3=1) is NOT validated
Hash=73d6bfa4ac7e4a6fa2da6911e5f8c2e3
Cycle=SyncsWR Fre SyncdWR Fre SyncdWR Fre
Relax safe360 No
Safe=Fre SyncsWR SyncdWR
Time safe360 61.18
$Revision: 3163 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 2000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 20000
#endif
#ifndef N_EXE
#define N_EXE (32 < N ? 1 : 32 / N)
#endif
/* gcc options: -Wall -std=gnu99 -O -pthread */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: true */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 32 */
GCCOPTS="-Wall -std=gnu99 -O -pthread"
LITMUSOPTS=
Wed Dec 30 10:57:21 GMT 2009