src/Pure/System/benchmark.scala
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--
added initial version of benchmark module, e.g., to compare performance of different hosts; added benchmark operation to build cluster;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
}