added initial version of benchmark module, e.g., to compare performance of different hosts;
added benchmark operation to build cluster;

--- a/etc/build.props	Wed Oct 18 19:26:37 2023 +0200
+++ b/etc/build.props	Wed Oct 18 19:49:08 2023 +0200
@@ -151,6 +151,7 @@
   src/Pure/PIDE/yxml.scala \
   src/Pure/ROOT.scala \
   src/Pure/System/bash.scala \
+  src/Pure/System/benchmark.scala \
   src/Pure/System/classpath.scala \
   src/Pure/System/command_line.scala \
   src/Pure/System/components.scala \

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/benchmark.scala	Wed Oct 18 19:49:08 2023 +0200
@@ -0,0 +1,70 @@
+/*  Title:      Pure/System/benchmark.scala
+    Author:     Fabian Huch, TU Muenchen
+
+Host platform benchmarks for performance estimation.
+*/
+
+package isabelle
+
+
+object Benchmark {
+
+  def benchmark_command(
+    host: Build_Cluster.Host,
+    ssh: SSH.System = SSH.Local,
+    isabelle_home: Path = Path.current,
+  ): String = {
+    val options = Options.Spec("build_hostname", Some(host.name)) :: host.options
+    ssh.bash_path(isabelle_home + Path.explode("bin/isabelle")) + " benchmark" +
+      options.map(opt => " -o " + Bash.string(opt.print)).mkString +
+      " " + Bash.string(host.name)
+  }
+
+  def benchmark(options: Options, progress: Progress = new Progress()): Unit = {
+    val hostname = options.string("build_hostname")
+    val store = Store(options)
+
+    using(store.open_server()) { server =>
+      val db = store.open_build_database(path = Host.private_data.database, server = server)
+
+      progress.echo("Starting benchmark...")
+      val start = Time.now()
+
+      // TODO proper benchmark
+      def fib(n: Long): Long = if (n < 2) 1 else fib(n - 2) + fib(n - 1)
+      val result = fib(42)
+
+      val stop = Time.now()
+      val timing = stop - start
+
+      val score = Time.seconds(100).ms.toDouble / (1 + timing.ms)
+      progress.echo(
+        "Finished benchmark in " + timing.message + ". Score: " + String.format("%.2f", score))
+
+      Host.write_info(db, Host.Info.gather(hostname, score = Some(score)))
+    }
+  }
+
+  val isabelle_tool = Isabelle_Tool("benchmark", "run system benchmark",
+    Scala_Project.here,
+    { args =>
+      var options = Options.init()
+
+      val getopts = Getopts("""
+Usage: isabelle benchmark [OPTIONS]
+
+  Options are:
+    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+
+  Run a system benchmark.
+""",
+        "o:" -> (arg => options = options + arg))
+
+      val more_args = getopts(args)
+      if (more_args.nonEmpty) getopts.usage()
+
+      val progress = new Console_Progress()
+
+      benchmark(options, progress = progress)
+    })
+}
\ No newline at end of file

--- a/src/Pure/System/host.scala	Wed Oct 18 19:26:37 2023 +0200
+++ b/src/Pure/System/host.scala	Wed Oct 18 19:49:08 2023 +0200
@@ -125,14 +125,15 @@
   def num_cpus(): Int = Runtime.getRuntime.availableProcessors
 
   object Info {
-    def gather(hostname: String, ssh: SSH.System = SSH.Local): Info =
-      Info(hostname, numa_nodes(ssh = ssh), num_cpus())
+    def gather(hostname: String, ssh: SSH.System = SSH.Local, score: Option[Double] = None): Info =
+      Info(hostname, numa_nodes(ssh = ssh), num_cpus(), score)
   }
 
   sealed case class Info(
     hostname: String,
     numa_nodes: List[Int],
-    num_cpus: Int)
+    num_cpus: Int,
+    benchmark_score: Option[Double])
 
 
   /* shuffling of NUMA nodes */
@@ -189,9 +190,10 @@
       val hostname = SQL.Column.string("hostname").make_primary_key
       val numa_info = SQL.Column.string("numa_info")
       val num_cpus = SQL.Column.int("num_cpus")
+      val benchmark_score = SQL.Column.double("benchmark_score")
 
       val table =
-        make_table(List(hostname, numa_info, num_cpus), name = "info")
+        make_table(List(hostname, numa_info, num_cpus, benchmark_score), name = "info")
     }
 
     def write_info(db: SQL.Database, info: Info): Unit = {
@@ -201,6 +203,7 @@
           stmt.string(1) = info.hostname
           stmt.string(2) = info.numa_nodes.mkString(",")
           stmt.int(3) = info.num_cpus
+          stmt.double(4) = info.benchmark_score
         })
     }
 
@@ -210,8 +213,9 @@
         { res =>
           val numa_info = res.string(Info.numa_info)
           val num_cpus = res.int(Info.num_cpus)
+          val benchmark_score = res.get_double(Info.benchmark_score)
 
-          Host.Info(hostname, parse_numa_info(numa_info), num_cpus)
+          Host.Info(hostname, parse_numa_info(numa_info), num_cpus, benchmark_score)
         })
   }
 

--- a/src/Pure/System/isabelle_tool.scala	Wed Oct 18 19:26:37 2023 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Wed Oct 18 19:49:08 2023 +0200
@@ -120,6 +120,7 @@
 class Isabelle_Scala_Tools(val tools: Isabelle_Tool*) extends Isabelle_System.Service
 
 class Tools extends Isabelle_Scala_Tools(
+  Benchmark.isabelle_tool,
   Build.isabelle_tool1,
   Build.isabelle_tool2,
   Build.isabelle_tool3,

--- a/src/Pure/Tools/build_cluster.scala	Wed Oct 18 19:26:37 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Wed Oct 18 19:49:08 2023 +0200
@@ -158,6 +158,12 @@
 
     def init(): Unit = remote_isabelle.init()
 
+    def benchmark(): Unit = {
+      val script =
+        Benchmark.benchmark_command(host, ssh = ssh, isabelle_home = remote_isabelle_home)
+      remote_isabelle.bash(script).check
+    }
+
     def start(): Process_Result = {
       val remote_ml_platform = remote_isabelle.getenv("ML_PLATFORM")
       if (remote_ml_platform != build_context.ml_platform) {
@@ -207,6 +213,7 @@
   def return_code(exn: Throwable): Unit = return_code(Process_Result.RC(exn))
   def open(): Unit = ()
   def init(): Unit = ()
+  def benchmark(): Unit = ()
   def start(): Unit = ()
   def active(): Boolean = false
   def join: List[Build_Cluster.Result] = Nil
@@ -269,7 +276,7 @@
   }
 
 
-  /* init remote Isabelle distributions */
+  /* init and benchmark remote Isabelle distributions */
 
   private var _init = List.empty[Future[Unit]]
 
@@ -286,6 +293,17 @@
         }
     }
   }
+  
+  override def benchmark(): Unit = synchronized {
+    _init.foreach(_.join)
+    _init =
+      for (session <- _sessions if !session.host.shared) yield {
+        Future.thread(session.host.message("session")) {
+          capture(session.host, "benchmark") { session.benchmark() }
+        }
+      }
+    _init.foreach(_.join)
+  }
 
 
   /* workers */