]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/scripts/public_html/bench.php
0ad31b26913ec3d43eb8e70a9f73d9e887a39846
[helm.git] / helm / software / matita / scripts / public_html / bench.php
1 <?php require("common.php"); 
2   
3 // syntax
4 //
5 // queries ::= query | query "###" queries
6 // query ::= name "@@@" sql
7 //
8 $limits = array("20","50","100");
9   
10 $quey_all = urlencode("Whole content:@@@select * from bench order by mark desc***");
11 $query_fail = urlencode(
12   "Number of failures@@@" .
13   "select mark, count(distinct test) as fail_no from bench where result = 'fail' group by mark order by mark desc***"
14   . "###" . 
15   "Tests failed@@@" .
16   "select distinct mark, test, result from bench where result = 'fail' order by mark desc***" 
17 );
18 $query_gc = urlencode(
19   "GC usage @@@" .
20   "select bench.mark, SUM(bench.time) - SUM(bench1.time) as gc_hoverhead from bench, bench as bench1 where bench.mark = bench1.mark and bench.test = bench1.test and bench.options = 'gc-on' and bench1.options = 'gc-off' and bench.compilation = bench1.compilation group by mark***"
21   . "###" . 
22   "GC usage (opt)@@@" .
23   "select bench.mark, SUM(bench.time) - SUM(bench1.time) as gc_hoverhead from bench, bench as bench1 where bench.mark = bench1.mark and bench.test = bench1.test and bench.options = 'gc-on' and bench1.options = 'gc-off' and bench.compilation = bench1.compilation and bench.compilation = 'opt' group by mark***"
24   . "###" . 
25   "GC usage (byte)@@@" .
26   "select bench.mark, SUM(bench.time) - SUM(bench1.time) as gc_hoverhead from bench, bench as bench1 where bench.mark = bench1.mark and bench.test = bench1.test and bench.options = 'gc-on' and bench1.options = 'gc-off' and bench.compilation = bench1.compilation and bench.compilation = 'byte' group by mark***"
27   
28 );
29 $query_auto = urlencode(
30   "Auto (with GC)@@@select mark, SUM(bench.time) as time from bench where test='auto.ma' and options = 'gc-on' group by mark order by mark desc***"
31   . "###" . 
32   "Auto (without GC)@@@select mark, SUM(bench.time) as time from bench where test='auto.ma' and options = 'gc-off' group by mark order by mark desc***"
33     . "###" . 
34    "GC overhead@@@select bench.mark, SUM(bench.time) - SUM(bench1.time) as gc_hoverhead from bench, bench as bench1 where bench.mark = bench1.mark and bench.test = bench1.test and bench.options = 'gc-on' and bench1.options = 'gc-off' and bench.compilation = bench1.compilation and bench.test = 'auto.ma' group by mark"
35 );
36
37 $query_csc = urlencode("Performances (byte and GC) per mark@@@select bench.mark ,bench_svn.revision as revision, SUM(bench.time) as sum_time, SUM(bench.timeuser) as sum_timeuser, COUNT(DISTINCT bench.test) as performed_tests from bench, bench_svn where bench.options = 'gc-on' and bench.compilation = 'byte' and bench_svn.mark = bench.mark group by bench.mark order by bench.mark desc"
38 );
39
40 $query_csc_opt = urlencode("Performances (opt and GC) per mark@@@select bench.mark,bench_svn.revision as revision, SUM(bench.time) as sum_time, SUM(bench.timeuser) as sum_timeuser, COUNT(DISTINCT bench.test) as performed_tests from bench, bench_svn where bench.options = 'gc-on' and bench.compilation = 'opt' and bench_svn.mark = bench.mark group by bench.mark order by bench.mark desc"
41 );
42
43 $query_total = urlencode(
44   
45 "Max N@@@select COUNT(DISTINCT test) as MAX from bench group by mark order by MAX desc LIMIT 0,1;"
46   . "###" .
47   "Number of compiled tests@@@select mark, COUNT(DISTINCT test) as N from bench group by mark order by mark desc***"
48 );
49
50 function minus1_to_all($s){
51   if ($s == "-1") 
52     return "all";
53   else 
54     return $s;
55 }
56
57 function links_of($name,$q,$limits){
58   echo "<li>$name :&nbsp;&nbsp;&nbsp;";
59   if (strpos($q, urlencode("***")) === false) {
60     echo "<a href=\"showquery.php?query=$q;\">all</a>";
61   } else {
62     foreach($limits as $l) {
63       $q1 = str_replace(urlencode("***"), " LIMIT 0,$l", $q);
64       echo "<a href=\"showquery.php?query=$q1;\">" . 
65             minus1_to_all($l) . "</a>&nbsp;&nbsp;";
66     }
67       $q1 = str_replace(urlencode("***"), " ", $q);
68       echo "<a href=\"showquery.php?query=$q1;\">" . 
69             minus1_to_all("-1") . "</a>&nbsp;&nbsp;";
70   }
71   echo "</li>";
72 }
73
74 ?>
75
76 <html>
77   <head>
78   <link type="text/css" rel="stylesheet" href="style.css"/>
79   </head>
80   <body>
81     <h1>QUERY the benchmark system</h1>
82     <h2>Common Queries</h2>
83     <p>
84       <ul>
85       <? links_of("Broken tests",$query_fail,$limits) ?>
86       <? links_of("Garbage collector killer",$query_gc,$limits) ?>
87       <? links_of("Auto performances",$query_auto,$limits) ?>
88       <? links_of("Global performances (bytecode)",$query_csc,$limits) ?>
89       <? links_of("Global performances (nativecode)",$query_csc_opt,$limits) ?>
90       <? links_of("Number of compiled tests",$query_total,$limits) ?>
91       <? links_of("All table contents",$quey_all,$limits) ?>
92       </ul>
93     </p>
94     <h2>Custom Query - Simple Interface</h2>
95     <form action="composequery.php" method="get">
96     <table>
97   <tr>
98     <td>Marks:</td>
99     <td> 
100       <select name="mark">";
101         <option value="--">--</option>";
102         <?query("select distinct mark from bench order by mark desc;",
103             "array_to_combo");?>
104       </select>      
105     </td>
106   </tr>
107   <tr>
108     <td>Compilations:</td>
109     <td> 
110       <select name="compilation">";
111         <option value="--">--</option>";
112           <?query("select distinct compilation from bench;","array_to_combo");?>
113       </select>      
114     </td>
115   </tr>
116   <tr>
117     <td>Options:</td>
118     <td>  
119       <select name="options">";
120         <option value="--">--</option>";
121           <?query("select distinct options from bench;","array_to_combo");?>
122       </select>      
123     </td>
124   </tr>
125   <tr>
126     <td>Tests:</td>
127     <td>    
128       <select name="test">";
129         <option value="--">--</option>";
130           <?query("select distinct test from bench;","array_to_combo");?>
131       </select>      
132     </td>
133   </tr>
134   <tr>
135     <td>Test results:</td>
136     <td>
137       <select name="result">";
138         <option value="--">--</option>";
139           <?query("select distinct result from bench;","array_to_combo"); ?>
140       </select>      
141     </td>
142   </tr>
143   <tr>
144     <td>Group By: </td>
145     <td>
146       <select name="groupby">";
147         <option value="--">--</option>";
148         <? array_to_combo(array("mark"));array_to_combo(array("options")); ?>
149       </select>      
150     </td>
151   </tr>
152   <tr>
153     <td>Limit: </td>
154     <td>
155       <select name="limit">";
156         <option value="--">--</option>";
157       <? foreach(array($limits) as $l) {array_to_combo($l);} ?>
158       </select>      
159     </td>
160   </tr>
161   <tr>
162     <td><input type="submit" value="Submit" class="button" /></td>
163   </tr>
164  </table>
165 </form>
166 <h2>Custom Query - raw SQL</h2>
167 <form action="showquery.php" method="get">
168 <table>
169 <tr><td>'bench' table description:</td></tr>
170 </tr>
171 <? query("describe bench","printer"); ?>
172 </tr>
173 <tr><td></td></tr>
174 <tr><td colspan="7">
175 SQL (only one query, ';' if present must terminate the query, no characters allowed after it):</td></tr>
176 <tr><td colspan="7">
177 <textarea rows="10" cols="120" name="query"/>
178 select 
179   b1.test as test, b1.timeuser as oldtime, b2.timeuser as newtime, b1.compilation as comp, b1.options as opts
180 from 
181   bench as b1, bench as b2 
182 where 
183   b1.test = b2.test and 
184   b1.options = b2.options and
185   b1.compilation = b2.compilation and 
186   b1.mark = '' and b2.mark= '' and
187   ABS(b1.timeuser - b2.timeuser) &gt; 100;</textarea>
188 </td>
189 </tr>
190 <tr><td>
191 <input type="submit" value="Submit" class="button" /></td>
192 </tr>
193 </table>
194 </form>
195
196 </body>
197 </html>