author | Fabian Huch <huch@in.tum.de> |
Wed, 18 Oct 2023 19:49:08 +0200 | |
changeset 78840 | 4b528ca25573 |
child 78887 | 6996a20a1b7c |
permissions | -rw-r--r-- |
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
1 |
/* Title: Pure/System/benchmark.scala |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
2 |
Author: Fabian Huch, TU Muenchen |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
3 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
4 |
Host platform benchmarks for performance estimation. |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
5 |
*/ |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
6 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
7 |
package isabelle |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
8 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
9 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
10 |
object Benchmark { |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
11 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
12 |
def benchmark_command( |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
13 |
host: Build_Cluster.Host, |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
14 |
ssh: SSH.System = SSH.Local, |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
15 |
isabelle_home: Path = Path.current, |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
16 |
): String = { |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
17 |
val options = Options.Spec("build_hostname", Some(host.name)) :: host.options |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
18 |
ssh.bash_path(isabelle_home + Path.explode("bin/isabelle")) + " benchmark" + |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
19 |
options.map(opt => " -o " + Bash.string(opt.print)).mkString + |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
20 |
" " + Bash.string(host.name) |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
21 |
} |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
22 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
23 |
def benchmark(options: Options, progress: Progress = new Progress()): Unit = { |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
24 |
val hostname = options.string("build_hostname") |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
25 |
val store = Store(options) |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
26 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
27 |
using(store.open_server()) { server => |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
28 |
val db = store.open_build_database(path = Host.private_data.database, server = server) |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
29 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
30 |
progress.echo("Starting benchmark...") |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
31 |
val start = Time.now() |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
32 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
33 |
// TODO proper benchmark |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
34 |
def fib(n: Long): Long = if (n < 2) 1 else fib(n - 2) + fib(n - 1) |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
35 |
val result = fib(42) |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
36 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
37 |
val stop = Time.now() |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
38 |
val timing = stop - start |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
39 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
40 |
val score = Time.seconds(100).ms.toDouble / (1 + timing.ms) |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
41 |
progress.echo( |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
42 |
"Finished benchmark in " + timing.message + ". Score: " + String.format("%.2f", score)) |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
43 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
44 |
Host.write_info(db, Host.Info.gather(hostname, score = Some(score))) |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
45 |
} |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
46 |
} |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
47 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
48 |
val isabelle_tool = Isabelle_Tool("benchmark", "run system benchmark", |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
49 |
Scala_Project.here, |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
50 |
{ args => |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
51 |
var options = Options.init() |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
52 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
53 |
val getopts = Getopts(""" |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
54 |
Usage: isabelle benchmark [OPTIONS] |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
55 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
56 |
Options are: |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
57 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
58 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
59 |
Run a system benchmark. |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
60 |
""", |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
61 |
"o:" -> (arg => options = options + arg)) |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
62 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
63 |
val more_args = getopts(args) |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
64 |
if (more_args.nonEmpty) getopts.usage() |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
65 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
66 |
val progress = new Console_Progress() |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
67 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
68 |
benchmark(options, progress = progress) |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
69 |
}) |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
70 |
} |