Tue Dec 29 09:33:53 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 7,2
_litmus_P1_1_: stw 7,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 6,1
_litmus_P1_4_: stw 6,0(9)
_litmus_P0_0_: li 7,2
_litmus_P0_1_: stw 7,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 6,1
_litmus_P0_4_: stw 6,0(9)
Test safe036 Allowed
Histogram (3 states)
299719548:>x=1; y=2;
58915229:>x=1; y=1;
281365223:>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 26.47
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 7,2
_litmus_P2_1_: stw 7,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 6,1
_litmus_P2_4_: stw 6,0(9)
_litmus_P1_0_: li 7,2
_litmus_P1_1_: stw 7,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 6,1
_litmus_P1_4_: stw 6,0(9)
_litmus_P0_0_: li 7,2
_litmus_P0_1_: stw 7,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 6,1
_litmus_P0_4_: stw 6,0(9)
Test safe037 Allowed
Histogram (7 states)
63210577:>x=1; y=2; z=1;
1655522:>x=1; y=1; z=1;
63923744:>x=2; y=2; z=1;
66287972:>x=2; y=1; z=1;
71480096:>x=2; y=1; z=2;
66494813:>x=1; y=2; z=2;
66947276:>x=1; y=1; z=2;
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 41.52
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 7,2
_litmus_P2_1_: stw 7,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 6,1
_litmus_P2_4_: stw 6,0(9)
_litmus_P1_0_: li 7,2
_litmus_P1_1_: stw 7,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 6,1
_litmus_P1_4_: stw 6,0(9)
_litmus_P0_0_: li 7,2
_litmus_P0_1_: stw 7,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 6,1
_litmus_P0_4_: stw 6,0(9)
Test safe038 Allowed
Histogram (7 states)
147894913:>x=2; y=2; z=1;
27383951:>x=1; y=1; z=2;
27543630:>x=2; y=1; z=2;
145553309:>x=2; y=1; z=1;
866262:>x=1; y=1; z=1;
27423503:>x=1; y=2; z=1;
23334432:>x=1; y=2; 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 41.12
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 5,0(9)
_litmus_P1_0_: li 7,2
_litmus_P1_1_: stw 7,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 6,1
_litmus_P1_4_: stw 6,0(9)
_litmus_P0_0_: li 7,1
_litmus_P0_1_: stw 7,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 6,1
_litmus_P0_4_: stw 6,0(9)
Test safe040 Allowed
Histogram (7 states)
174192:>2:r3=1; y=1; z=1;
53537921:>2:r3=0; y=1; z=2;
16197177:>2:r3=1; y=1; z=2;
14392228:>2:r3=1; y=2; z=2;
27272833:>2:r3=1; y=2; z=1;
108784218:>2:r3=0; y=2; z=1;
179641431:>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 36.02
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 7,2
_litmus_P1_1_: stw 7,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 6,1
_litmus_P1_4_: stw 6,0(9)
_litmus_P0_0_: li 7,2
_litmus_P0_1_: stw 7,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 6,1
_litmus_P0_4_: stw 6,0(9)
Test safe045 Allowed
Histogram (3 states)
506950747:>x=2; y=1;
11284635:>x=1; y=1;
121764618:>x=1; y=2;
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 26.55
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 7,2
_litmus_P2_1_: stw 7,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 6,1
_litmus_P2_4_: stw 6,0(9)
_litmus_P1_0_: li 7,2
_litmus_P1_1_: stw 7,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 6,1
_litmus_P1_4_: stw 6,0(9)
_litmus_P0_0_: li 7,2
_litmus_P0_1_: stw 7,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 6,1
_litmus_P0_4_: stw 6,0(9)
Test safe046 Allowed
Histogram (7 states)
12321504:>x=2; y=1; z=2;
12639265:>x=1; y=1; z=2;
727186:>x=1; y=1; z=1;
146654345:>x=2; y=2; z=1;
134086873:>x=1; y=2; z=1;
49607895:>x=1; y=2; z=2;
43962932:>x=2; y=1; z=1;
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 40.40
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 5,0(9)
_litmus_P1_0_: li 7,2
_litmus_P1_1_: stw 7,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 6,1
_litmus_P1_4_: stw 6,0(9)
_litmus_P0_0_: li 7,1
_litmus_P0_1_: stw 7,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 6,1
_litmus_P0_4_: stw 6,0(9)
Test safe048 Allowed
Histogram (7 states)
108592:>2:r3=1; y=1; z=1;
11664032:>2:r3=1; y=1; z=2;
18875799:>2:r3=0; y=1; z=2;
72929957:>2:r3=0; y=1; z=1;
162669057:>2:r3=0; y=2; z=1;
55402919:>2:r3=1; y=2; z=1;
78349644:>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 34.90
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 6,2
_litmus_P1_1_: stw 6,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 5,0(9)
_litmus_P0_0_: li 7,1
_litmus_P0_1_: stw 7,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 6,1
_litmus_P0_4_: stw 6,0(9)
Test safe069 Allowed
Histogram (3 states)
90974000:>1:r3=1; y=2;
14481681:>1:r3=1; y=1;
534544319:>1:r3=0; y=1;
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 21.31
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 7,2
_litmus_P2_1_: stw 7,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 6,1
_litmus_P2_4_: stw 6,0(9)
_litmus_P1_0_: li 7,1
_litmus_P1_1_: stw 7,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 6,1
_litmus_P1_4_: stw 6,0(9)
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 5,0(9)
Test safe070 Allowed
Histogram (7 states)
57796 :>0:r3=1; x=1; z=1;
12979704:>0:r3=1; x=2; z=2;
55453661:>0:r3=1; x=2; z=1;
130212878:>0:r3=0; x=1; z=1;
162419091:>0:r3=0; x=2; z=1;
28442699:>0:r3=0; x=1; z=2;
10434171:>0:r3=1; x=1; z=2;
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 36.32
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 5,0(9)
_litmus_P1_0_: li 7,1
_litmus_P1_1_: stw 7,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 6,1
_litmus_P1_4_: stw 6,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 5,0(9)
Test safe072 Allowed
Histogram (7 states)
7133 :>0:r3=1; 2:r3=1; z=1;
30944486:>0:r3=1; 2:r3=0; z=1;
17511023:>0:r3=1; 2:r3=0; z=2;
1959372:>0:r3=1; 2:r3=1; z=2;
28265645:>0:r3=0; 2:r3=1; z=2;
255130626:>0:r3=0; 2:r3=0; z=1;
66181715:>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 33.31
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 5,0(9)
_litmus_P1_0_: li 7,2
_litmus_P1_1_: stw 7,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 6,1
_litmus_P1_4_: stw 6,0(9)
_litmus_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 7,0(9)
Test safe077 Allowed
Histogram (13 states)
157 :>0:r3=2; 2:r3=1; x=2; y=1;
1284 :>0:r3=2; 2:r3=2; x=2; y=1;
13305 :>0:r3=1; 2:r3=1; x=1; y=1;
47494 :>0:r3=2; 2:r3=2; x=2; y=2;
4233233:>0:r3=1; 2:r3=2; x=1; y=1;
734311:>0:r3=2; 2:r3=0; x=2; y=1;
71113994:>0:r3=1; 2:r3=0; x=1; y=1;
2092149:>0:r3=1; 2:r3=2; x=2; y=1;
25644650:>0:r3=1; 2:r3=2; x=2; y=2;
7718402:>0:r3=1; 2:r3=1; x=1; y=2;
4668307:>0:r3=1; 2:r3=2; x=1; y=2;
90906792:>0:r3=1; 2:r3=1; x=2; y=1;
192825922:>0:r3=1; 2:r3=0; x=2; y=1;
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 34.49
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 7,2
_litmus_P1_1_: stw 7,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 6,1
_litmus_P1_4_: stw 6,0(9)
_litmus_P0_0_: li 7,2
_litmus_P0_1_: stw 7,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 6,1
_litmus_P0_4_: stw 6,0(9)
Test safe135 Allowed
Histogram (3 states)
312422851:>x=1; y=2;
28133189:>x=1; y=1;
299443960:>x=2; y=1;
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 27.65
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 7,2
_litmus_P2_1_: stw 7,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 6,1
_litmus_P2_4_: stw 6,0(9)
_litmus_P1_0_: li 7,2
_litmus_P1_1_: stw 7,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 6,1
_litmus_P1_4_: stw 6,0(9)
_litmus_P0_0_: li 7,2
_litmus_P0_1_: stw 7,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 6,1
_litmus_P0_4_: stw 6,0(9)
Test safe136 Allowed
Histogram (7 states)
67041904:>x=2; y=2; z=1;
66069959:>x=1; y=2; z=2;
901299:>x=1; y=1; z=1;
65597915:>x=1; y=1; z=2;
64489189:>x=2; y=1; z=1;
66656249:>x=2; y=1; z=2;
69243485:>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 40.65
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 5,0(9)
_litmus_P1_0_: li 7,2
_litmus_P1_1_: stw 7,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 6,1
_litmus_P1_4_: stw 6,0(9)
_litmus_P0_0_: li 7,1
_litmus_P0_1_: stw 7,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 6,1
_litmus_P0_4_: stw 6,0(9)
Test safe138 Allowed
Histogram (7 states)
79446377:>2:r3=0; y=1; z=2;
81154 :>2:r3=1; y=1; z=1;
20589130:>2:r3=1; y=2; z=1;
76076163:>2:r3=1; y=2; z=2;
73984340:>2:r3=1; y=1; z=2;
94392626:>2:r3=0; y=1; z=1;
55430210:>2:r3=0; y=2; z=1;
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 35.06
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 6,2
_litmus_P1_1_: stw 6,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 5,0(9)
_litmus_P0_0_: li 7,1
_litmus_P0_1_: stw 7,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 6,1
_litmus_P0_4_: stw 6,0(9)
Test safe158 Allowed
Histogram (3 states)
228462660:>1:r3=1; y=2;
1362386:>1:r3=1; y=1;
410174954:>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 22.51
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 5,0(9)
_litmus_P1_0_: li 7,1
_litmus_P1_1_: stw 7,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 6,1
_litmus_P1_4_: stw 6,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 5,0(9)
Test safe160 Allowed
Histogram (7 states)
6809 :>0:r3=1; 2:r3=1; z=1;
35640364:>0:r3=0; 2:r3=1; z=1;
126490012:>0:r3=0; 2:r3=0; z=1;
91669813:>0:r3=1; 2:r3=0; z=2;
61896097:>0:r3=1; 2:r3=0; z=1;
69467924:>0:r3=0; 2:r3=1; z=2;
14828981:>0:r3=1; 2:r3=1; z=2;
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 32.89
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 5,0(9)
_litmus_P1_0_: li 7,2
_litmus_P1_1_: stw 7,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 6,1
_litmus_P1_4_: stw 6,0(9)
_litmus_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 7,0(9)
Test safe165 Allowed
Histogram (13 states)
122 :>0:r3=2; 2:r3=1; x=2; y=1;
1489 :>0:r3=2; 2:r3=2; x=2; y=1;
17155 :>0:r3=1; 2:r3=1; x=1; y=1;
402107:>0:r3=1; 2:r3=2; x=2; y=1;
213301:>0:r3=2; 2:r3=0; x=2; y=1;
148441199:>0:r3=1; 2:r3=0; x=1; y=1;
3620669:>0:r3=1; 2:r3=2; x=1; y=1;
39805395:>0:r3=1; 2:r3=2; x=1; y=2;
53950682:>0:r3=1; 2:r3=1; x=1; y=2;
293532:>0:r3=2; 2:r3=2; x=2; y=2;
37650260:>0:r3=1; 2:r3=2; x=2; y=2;
38029002:>0:r3=1; 2:r3=1; x=2; y=1;
77575087:>0:r3=1; 2:r3=0; x=2; 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 33.22
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 7,1
_litmus_P1_1_: stw 7,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 6,0(9)
_litmus_P0_0_: li 7,1
_litmus_P0_1_: stw 7,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 6,0(9)
Test safe358 Allowed
Histogram (3 states)
10091270:>0:r3=1; 1:r3=1;
297970662:>0:r3=0; 1:r3=1;
331938068:>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 17.92
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 7,1
_litmus_P2_1_: stw 7,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: lwz 6,0(9)
_litmus_P1_0_: li 7,1
_litmus_P1_1_: stw 7,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 6,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 5,0(9)
Test safe359 Allowed
Histogram (7 states)
4409 :>0:r3=1; 1:r3=1; 2:r3=1;
17842582:>0:r3=1; 1:r3=0; 2:r3=1;
125859867:>0:r3=1; 1:r3=0; 2:r3=0;
132389467:>0:r3=0; 1:r3=0; 2:r3=1;
11689147:>0:r3=0; 1:r3=1; 2:r3=1;
98043356:>0:r3=0; 1:r3=1; 2:r3=0;
14171172:>0:r3=1; 1:r3=1; 2:r3=0;
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 30.50
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 7,0(9)
_litmus_P1_0_: li 6,1
_litmus_P1_1_: stw 6,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 5,0(9)
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 5,0(9)
Test safe360 Allowed
Histogram (13 states)
158 :>0:r3=1; 1:r3=1; 2:r3=2; y=2;
174 :>0:r3=1; 1:r3=2; 2:r3=2; y=2;
2418 :>0:r3=1; 1:r3=1; 2:r3=1; y=1;
1676090:>0:r3=1; 1:r3=2; 2:r3=1; y=1;
40771828:>0:r3=0; 1:r3=2; 2:r3=1; y=1;
304826:>0:r3=1; 1:r3=0; 2:r3=2; y=2;
24128286:>0:r3=1; 1:r3=1; 2:r3=1; y=2;
1919013:>0:r3=1; 1:r3=2; 2:r3=1; y=2;
383432:>0:r3=0; 1:r3=2; 2:r3=2; y=2;
114670221:>0:r3=0; 1:r3=2; 2:r3=1; y=2;
91172173:>0:r3=0; 1:r3=1; 2:r3=1; y=1;
63114249:>0:r3=1; 1:r3=0; 2:r3=1; y=2;
61857132:>0:r3=1; 1:r3=0; 2:r3=1; y=1;
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 31.42
$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: none */
/* 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=-s 100000 -r 400
Tue Dec 29 09:44:40 GMT 2009