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 $query_last_mark = "select mark from bench order by mark desc limit 1;";
  11 $last_mark = "";
  12 function set_last_mark($a) {
  13  global $last_mark;
  14  foreach ($a as $k => $v) {
  15    $last_mark = $v;
  16  }
  17 }
  18 query($query_last_mark,"set_last_mark");
  19
  20 $query_before_last_mark = "select mark from bench where mark <> '$last_mark' order by mark desc limit 1;";
  21 $before_last_mark = "";
  22 function set_before_last_mark($a) {
  23  global $before_last_mark;
  24  foreach ($a as $k => $v) {
  25    $before_last_mark = $v;
  26  }
  27 }
  28 query($query_before_last_mark,"set_before_last_mark");
  29
  30 $quey_all = urlencode("
  31 Whole content:
  32 @@@
  33 select * from bench order by mark desc***");
  34
  35 $query_time_diff = urlencode("
  36 Time diff:
  37 @@@
  38 select
  39   b1.test as test, b1.timeuser as oldtime, b2.timeuser as newtime, b1.compilation as comp, b1.options as opts,
  40   (b2.timeuser - b1.timeuser) as diff
  41 from
  42   bench as b1, bench as b2
  43 where
  44   b1.test = b2.test and
  45   b1.options = b2.options and
  46   b1.compilation = b2.compilation and
  47   b1.result = b2.result and
  48   b1.mark = '$before_last_mark' and b2.mark= '$last_mark' and
  49   ABS(b2.timeuser - b1.timeuser) > 100
  50 order by diff desc***");
  51
  52 $query_result_diff = urlencode("
  53 Result diff:
  54 @@@
  55 select
  56   b1.test as test, b1.result as oldresult, b2.result as newresult, b1.timeuser as oldtime, b2.timeuser as newtime, b1.compilation as comp, b1.options as opts,
  57   (b2.timeuser - b1.timeuser) as diff
  58 from
  59   bench as b1, bench as b2
  60 where
  61   b1.test = b2.test and
  62   b1.options = b2.options and
  63   b1.compilation = b2.compilation and
  64   b1.result <> b2.result and
  65   b1.mark = '$before_last_mark' and b2.mark= '$last_mark'
  66 order by test desc***");
  67
  68 $query_fail = urlencode("
  69 Number of failures
  70 @@@
  71 select
  72   mark, count(distinct test) as fail_no
  73 from bench
  74 where result = 'fail' group by mark order by mark desc***
  75 ###
  76 Tests failed
  77 @@@
  78 select distinct mark, test, result
  79 from bench
  80 where result = 'fail' order by mark desc***");
  81
  82 $query_gc = urlencode("
  83 GC usage
  84 @@@
  85 select
  86   bench.mark, SUM(bench.time) - SUM(bench1.time) as gc_hoverhead
  87 from bench, bench as bench1
  88 where
  89   bench.mark = bench1.mark and
  90   bench.test = bench1.test and
  91   bench.options = 'gc-on' and
  92   bench1.options = 'gc-off' and
  93   bench.compilation = bench1.compilation
  94 group by mark***
  95 ###
  96 GC usage (opt)
  97 @@@
  98 select
  99   bench.mark, SUM(bench.time) - SUM(bench1.time) as gc_hoverhead
 100 from bench, bench as bench1
 101 where
 102   bench.mark = bench1.mark and
 103   bench.test = bench1.test and
 104   bench.options = 'gc-on' and
 105   bench1.options = 'gc-off' and
 106   bench.compilation = bench1.compilation and
 107   bench.compilation = 'opt'
 108 group by mark***
 109 ###
 110 GC usage (byte)
 111 @@@
 112 select
 113   bench.mark, SUM(bench.time) - SUM(bench1.time) as gc_hoverhead
 114 from bench, bench as bench1
 115 where
 116   bench.mark = bench1.mark and
 117   bench.test = bench1.test and
 118   bench.options = 'gc-on' and
 119   bench1.options = 'gc-off' and
 120   bench.compilation = bench1.compilation and
 121   bench.compilation = 'byte'
 122 group by mark***");
 123
 124 $query_auto = urlencode("
 125 Auto (with GC)
 126 @@@
 127 select
 128   mark, SUM(bench.time) as time
 129 from
 130   bench
 131 where
 132   test='auto.ma' and options = 'gc-on'
 133 group by mark
 134 order by mark desc***
 135 ###
 136 Auto (without GC)
 137 @@@
 138 select
 139   mark, SUM(bench.time) as time
 140 from
 141   bench
 142 where
 143   test='auto.ma' and options = 'gc-off'
 144 group by mark
 145 order by mark desc
 146 ***
 147 ###
 148 GC overhead
 149 @@@
 150 select
 151   bench.mark, SUM(bench.time) - SUM(bench1.time) as gc_hoverhead
 152 from
 153   bench, bench as bench1
 154 where
 155   bench.mark = bench1.mark and
 156   bench.test = bench1.test and
 157   bench.options = 'gc-on' and
 158   bench1.options = 'gc-off' and
 159   bench.compilation = bench1.compilation and
 160   bench.test = 'auto.ma'
 161 group by mark
 162 ***");
 163
 164 $query_csc = urlencode("
 165 Performances (byte and GC) per mark
 166 @@@
 167 select
 168   bench_times.mark as mark,
 169   bench_svn.revision,
 170   bench_times.time         as time,
 171   bench_times.timeuser     as timeuser,
 172   bench_times_opt.time     as time_opt,
 173   bench_times_opt.timeuser as timeuser_opt,
 174   bench_times.tests     as tests,
 175   bench_times_opt.tests as tests_opt,
 176   bench_fails.count     as fail,
 177   bench_fails_opt.count as fail_opt
 178 from
 179   bench_svn,
 180   (select
 181     b1.mark as mark, SUM(b1.time) as time,
 182     SUM(b1.timeuser) as timeuser,COUNT(DISTINCT b1.test) as tests
 183    from bench as b1
 184    where
 185      b1.options = 'gc-on' and
 186      b1.compilation = 'opt'
 187      group by b1.mark) as bench_times_opt,
 188   (select
 189     b1.mark as mark, SUM(b1.time) as time,
 190     SUM(b1.timeuser) as timeuser,COUNT(DISTINCT b1.test) as tests
 191    from bench as b1
 192    where
 193      b1.options = 'gc-on' and
 194      b1.compilation = 'byte'
 195      group by b1.mark) as bench_times,
 196   (select
 197     b1.mark as mark,
 198     SUM(if(b1.result='fail' and b1.compilation='byte' and b1.options='gc-on',1,0))
 199     as count
 200    from bench as b1
 201    group by b1.mark) as bench_fails,
 202   (select
 203     b1.mark as mark,
 204     SUM(if(b1.result='fail' and b1.compilation='opt' and b1.options='gc-on',1,0))
 205     as count
 206    from bench as b1
 207    group by b1.mark) as bench_fails_opt
 208 where
 209   bench_times.mark = bench_fails.mark and
 210   bench_times_opt.mark = bench_fails_opt.mark and
 211   bench_times.mark = bench_times_opt.mark and
 212   bench_svn.mark = bench_times.mark
 213   order by bench_svn.mark desc
 214 ***");
 215
 216 $query_total = urlencode("
 217 Max N
 218 @@@
 219 select
 220   COUNT(DISTINCT test) as MAX
 221 from
 222   bench
 223 group by mark
 224 order by MAX desc
 225 LIMIT 0,1;
 226 ###
 227 Number of compiled tests
 228 @@@
 229 select
 230   mark,
 231   COUNT(DISTINCT test) as N
 232 from
 233   bench
 234 group by mark
 235 order by mark desc
 236 ***");
 237
 238 function minus1_to_all($s){
 239   if ($s == "-1")
 240     return "all";
 241   else
 242     return $s;
 243 }
 244
 245 function links_of($name,$q,$limits){
 246   echo "<li>$name :&nbsp;&nbsp;&nbsp;";
 247   if (strpos($q, urlencode("***")) === false) {
 248     echo "<a href=\"showquery.php?query=$q;\">all</a>";
 249   } else {
 250     foreach($limits as $l) {
 251       $q1 = str_replace(urlencode("***"), " LIMIT 0,$l", $q);
 252       echo "<a href=\"showquery.php?query=$q1;\">" .
 253             minus1_to_all($l) . "</a>&nbsp;&nbsp;";
 254     }
 255       $q1 = str_replace(urlencode("***"), " ", $q);
 256       echo "<a href=\"showquery.php?query=$q1;\">" .
 257             minus1_to_all("-1") . "</a>&nbsp;&nbsp;";
 258   }
 259   echo "</li>";
 260 }
 261
 262 ?>
 263
 264 <html>
 265   <head>
 266   <link type="text/css" rel="stylesheet" href="style.css"/>
 267   </head>
 268   <body>
 269     <h1>QUERY the benchmark system</h1>
 270     <h2>Common Queries</h2>
 271     <p>
 272       <ul>
 273       <? links_of("Broken tests",$query_fail,$limits) ?>
 274       <? links_of("Time diff",$query_time_diff,$limits) ?>
 275       <? links_of("Result diff",$query_result_diff,$limits) ?>
 276       <? links_of("Garbage collector killer",$query_gc,$limits) ?>
 277       <? links_of("Auto performances",$query_auto,$limits) ?>
 278       <? links_of("Global performances",$query_csc,$limits) ?>
 279       <? links_of("Number of compiled tests",$query_total,$limits) ?>
 280       <? links_of("All table contents",$quey_all,$limits) ?>
 281       </ul>
 282     </p>
 283     <h2>Custom Query - Simple Interface</h2>
 284     <form action="composequery.php" method="get">
 285     <table>
 286   <tr>
 287     <td>Marks:</td>
 288     <td>
 289       <select name="mark">";
 290         <option value="--">--</option>";
 291         <?query("select distinct mark from bench order by mark desc;",
 292             "array_to_combo");?>
 293       </select>
 294     </td>
 295   </tr>
 296   <tr>
 297     <td>Compilations:</td>
 298     <td>
 299       <select name="compilation">";
 300         <option value="--">--</option>";
 301           <?query("select distinct compilation from bench;","array_to_combo");?>
 302       </select>
 303     </td>
 304   </tr>
 305   <tr>
 306     <td>Options:</td>
 307     <td>
 308       <select name="options">";
 309         <option value="--">--</option>";
 310           <?query("select distinct options from bench;","array_to_combo");?>
 311       </select>
 312     </td>
 313   </tr>
 314   <tr>
 315     <td>Tests:</td>
 316     <td>
 317       <select name="test">";
 318         <option value="--">--</option>";
 319           <?query("select distinct test from bench order by test;","array_to_combo");?>
 320       </select>
 321     </td>
 322   </tr>
 323   <tr>
 324     <td>Test results:</td>
 325     <td>
 326       <select name="result">";
 327         <option value="--">--</option>";
 328           <?query("select distinct result from bench;","array_to_combo"); ?>
 329       </select>
 330     </td>
 331   </tr>
 332   <tr>
 333     <td>Group By: </td>
 334     <td>
 335       <select name="groupby">";
 336         <option value="--">--</option>";
 337         <? array_to_combo(array("mark"));array_to_combo(array("options")); ?>
 338       </select>
 339     </td>
 340   </tr>
 341   <tr>
 342     <td>Limit: </td>
 343     <td>
 344       <select name="limit">";
 345         <option value="--">--</option>";
 346       <? foreach(array($limits) as $l) {array_to_combo($l);} ?>
 347       </select>
 348     </td>
 349   </tr>
 350   <tr>
 351     <td><input type="submit" value="Submit" class="button" /></td>
 352   </tr>
 353  </table>
 354 </form>
 355 <h2>Custom Query - raw SQL</h2>
 356 <form action="showquery.php" method="get">
 357 <table>
 358 <tr><td>'bench' table description:</td></tr>
 359 </tr>
 360 <? query("describe bench","printer"); ?>
 361 </tr>
 362 <tr><td></td></tr>
 363 <tr><td colspan="7">
 364 SQL (only one query, ';' if present must terminate the query, no characters allowed after it):</td></tr>
 365 <tr><td colspan="7">
 366 <textarea rows="10" cols="120" name="query"/>
 367 select
 368   b1.test as test, b1.timeuser as oldtime, b2.timeuser as newtime, b1.compilation as comp, b1.options as opts,
 369   (b2.timeuser - b1.timeuser) as diff
 370 from
 371   bench as b1, bench as b2
 372 where
 373   b1.test = b2.test and
 374   b1.options = b2.options and
 375   b1.compilation = b2.compilation and
 376   b1.result = b2.result and
 377   b1.mark = '<?php echo $before_last_mark ?>' and b2.mark= '<?php echo $last_mark ?>' and
 378   ABS(b2.timeuser - b1.timeuser) &lt; 100
 379 order by diff desc;
 380 </textarea>
 381 </td>
 382 </tr>
 383 <tr><td>
 384 <input type="submit" value="Submit" class="button" /></td>
 385 </tr>
 386 </table>
 387 </form>
 388
 389 </body>
 390 </html>