# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1697648706 -7200
# Node ID 4b014e6c1dfec06e050f00cd7e90bdcfcbf15061
# Parent  f97e23eaa62880f69cdb726c10d10e63bf584c52
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);

diff -r f97e23eaa628 -r 4b014e6c1dfe src/Pure/Concurrent/isabelle_thread.scala
--- a/src/Pure/Concurrent/isabelle_thread.scala	Wed Oct 18 18:53:26 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.scala	Wed Oct 18 19:05:06 2023 +0200
@@ -74,7 +74,7 @@
 
   def max_threads(): Int = {
     val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
-    if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8
+    if (m > 0) m else (Host.num_cpus() max 1) min 8
   }
 
   lazy val pool: ThreadPoolExecutor = {
diff -r f97e23eaa628 -r 4b014e6c1dfe src/Pure/System/host.scala
--- a/src/Pure/System/host.scala	Wed Oct 18 18:53:26 2023 +0200
+++ b/src/Pure/System/host.scala	Wed Oct 18 19:05:06 2023 +0200
@@ -71,7 +71,7 @@
   }
 
 
-  /* available NUMA nodes */
+  /* statically available resources */
 
   private val numa_info_linux: Path = Path.explode("/sys/devices/system/node/online")
 
@@ -99,6 +99,17 @@
     }
     catch { case ERROR(_) => None }
 
+  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())
+  }
+
+  sealed case class Info(
+    hostname: String,
+    numa_nodes: List[Int],
+    num_cpus: Int)
 
 
   /* shuffling of NUMA nodes */
@@ -126,7 +137,7 @@
   object private_data extends SQL.Data("isabelle_host") {
     val database: Path = Path.explode("$ISABELLE_HOME_USER/host.db")
 
-    override lazy val tables = SQL.Tables(Node_Info.table)
+    override lazy val tables = SQL.Tables(Node_Info.table, Info.table)
 
     object Node_Info {
       val hostname = SQL.Column.string("hostname").make_primary_key
@@ -150,6 +161,35 @@
           stmt.int(2) = numa_next
         })
     }
+
+    object Info {
+      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 table =
+        make_table(List(hostname, numa_info, num_cpus), name = "info")
+    }
+
+    def write_info(db: SQL.Database, info: Info): Unit = {
+      db.execute_statement(Info.table.delete(sql = Info.hostname.where_equal(info.hostname)))
+      db.execute_statement(Info.table.insert(), body =
+        { stmt =>
+          stmt.string(1) = info.hostname
+          stmt.string(2) = info.numa_nodes.mkString(",")
+          stmt.int(3) = info.num_cpus
+        })
+    }
+
+    def read_info(db: SQL.Database, hostname: String): Option[Host.Info] =
+      db.execute_query_statementO[Host.Info](
+        Info.table.select(Info.table.columns.tail, sql = Info.hostname.where_equal(hostname)),
+        { res =>
+          val numa_info = res.string(Info.numa_info)
+          val num_cpus = res.int(Info.num_cpus)
+
+          Host.Info(hostname, parse_numa_info(numa_info), num_cpus)
+        })
   }
 
   def next_numa_node(
@@ -176,4 +216,13 @@
         Some(n)
       }
     }
+
+  def write_info(db: SQL.Database, info: Info): Unit =
+    private_data.transaction_lock(db, create = true, label = "Host.write_info") {
+      private_data.write_info(db, info)
+    }
+  def read_info(db: SQL.Database, hostname: String): Option[Host.Info] =
+    private_data.transaction_lock(db, create = true, label = "Host.read_info") {
+      private_data.read_info(db, hostname)
+    }
 }