# HG changeset patch
# User wenzelm
# Date 1707926447 -3600
# Node ID 71731d28b86dfa267411a1bea5cf89700ebf61ac
# Parent  d9eb4807557c5474b083000f908c52cd39fb45f3# Parent  f1df99019b508c68dd23acaa752561d3facfa028
merged

diff -r d9eb4807557c -r 71731d28b86d etc/build.props
--- a/etc/build.props	Wed Feb 14 15:33:52 2024 +0000
+++ b/etc/build.props	Wed Feb 14 17:00:47 2024 +0100
@@ -68,6 +68,7 @@
   src/Pure/Concurrent/future.scala \
   src/Pure/Concurrent/isabelle_thread.scala \
   src/Pure/Concurrent/mailbox.scala \
+  src/Pure/Concurrent/multithreading.scala \
   src/Pure/Concurrent/par_list.scala \
   src/Pure/Concurrent/synchronized.scala \
   src/Pure/GUI/color_value.scala \
diff -r d9eb4807557c -r 71731d28b86d src/HOL/Tools/Nitpick/kodkod.scala
--- a/src/HOL/Tools/Nitpick/kodkod.scala	Wed Feb 14 15:33:52 2024 +0000
+++ b/src/HOL/Tools/Nitpick/kodkod.scala	Wed Feb 14 17:00:47 2024 +0100
@@ -42,7 +42,7 @@
   ): Result = {
     /* executor */
 
-    val pool_size = if (max_threads == 0) Isabelle_Thread.max_threads() else max_threads
+    val pool_size = if (max_threads == 0) Multithreading.max_threads() else max_threads
     val executor: ThreadPoolExecutor =
       new ThreadPoolExecutor(pool_size, pool_size, 0L, TimeUnit.MILLISECONDS,
         new LinkedBlockingQueue[Runnable], new ThreadPoolExecutor.CallerRunsPolicy)
diff -r d9eb4807557c -r 71731d28b86d src/Pure/Concurrent/isabelle_thread.scala
--- a/src/Pure/Concurrent/isabelle_thread.scala	Wed Feb 14 15:33:52 2024 +0000
+++ b/src/Pure/Concurrent/isabelle_thread.scala	Wed Feb 14 17:00:47 2024 +0100
@@ -72,13 +72,8 @@
 
   /* thread pool */
 
-  def max_threads(): Int = {
-    val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
-    if (m > 0) m else (Host.num_cpus() max 1) min 8
-  }
-
   lazy val pool: ThreadPoolExecutor = {
-    val n = max_threads()
+    val n = Multithreading.max_threads()
     val executor =
       new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable])
     executor.setThreadFactory(
diff -r d9eb4807557c -r 71731d28b86d src/Pure/Concurrent/multithreading.ML
--- a/src/Pure/Concurrent/multithreading.ML	Wed Feb 14 15:33:52 2024 +0000
+++ b/src/Pure/Concurrent/multithreading.ML	Wed Feb 14 17:00:47 2024 +0100
@@ -1,11 +1,14 @@
 (*  Title:      Pure/Concurrent/multithreading.ML
     Author:     Makarius
 
-Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
+Multithreading in Poly/ML, see also
+  - $ML_SOURCES/basis/Thread.sml: numPhysicalProcessors
+  - $ML_SOURCES/libpolyml/processes.cpp: PolyThreadNumPhysicalProcessors
 *)
 
 signature MULTITHREADING =
 sig
+  val num_processors: unit -> int
   val max_threads: unit -> int
   val max_threads_update: int -> unit
   val parallel_proofs: int ref
@@ -20,15 +23,18 @@
 structure Multithreading: MULTITHREADING =
 struct
 
-(* max_threads *)
-
-local
+(* physical processors *)
 
 fun num_processors () =
   (case Thread.Thread.numPhysicalProcessors () of
     SOME n => n
   | NONE => Thread.Thread.numProcessors ());
 
+
+(* max_threads *)
+
+local
+
 fun max_threads_result m =
   if Thread_Data.is_virtual then 1
   else if m > 0 then m
diff -r d9eb4807557c -r 71731d28b86d src/Pure/Concurrent/multithreading.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/multithreading.scala	Wed Feb 14 17:00:47 2024 +0100
@@ -0,0 +1,49 @@
+/*  Title:      Pure/Concurrent/multithreading.scala
+    Author:     Makarius
+
+Multithreading in Isabelle/Scala.
+*/
+
+package isabelle
+
+
+object Multithreading {
+  /* physical processors */
+
+  // slightly different from Poly/ML (more accurate)
+  def num_processors(ssh: SSH.System = SSH.Local): Int =
+    if (ssh.isabelle_platform.is_macos) {
+      val result = ssh.execute("sysctl -n hw.physicalcpu").check
+      Library.trim_line(result.out) match {
+        case Value.Int(n) => n
+        case _ => 1
+      }
+    }
+    else {
+      val Physical = """^\s*physical id\s*:\s*(\d+)\s*$""".r
+      val Cores = """^\s*cpu cores\s*:\s*(\d+)\s*$""".r
+
+      var physical: Option[Int] = None
+      var physical_cores = Map.empty[Int, Int]
+
+      val result = ssh.execute("cat /proc/cpuinfo").check
+      for (line <- Library.trim_split_lines(result.out)) {
+        line match {
+          case Physical(Value.Int(i)) => physical = Some(i)
+          case Cores(Value.Int(i))
+            if physical.isDefined && !physical_cores.isDefinedAt(physical.get) =>
+            physical_cores = physical_cores + (physical.get -> i)
+          case _ =>
+        }
+      }
+      physical_cores.valuesIterator.sum.max(1)
+    }
+
+
+  /* max_threads */
+
+  def max_threads(): Int = {
+    val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
+    if (m > 0) m else (num_processors() max 1) min 8
+  }
+}
diff -r d9eb4807557c -r 71731d28b86d src/Pure/System/benchmark.scala
--- a/src/Pure/System/benchmark.scala	Wed Feb 14 15:33:52 2024 +0000
+++ b/src/Pure/System/benchmark.scala	Wed Feb 14 17:00:47 2024 +0100
@@ -98,7 +98,7 @@
         progress.echo(
           "Finished benchmark in " + timing.message + ". Score: " + String.format("%.2f", score))
 
-        Host.write_info(db, Host.Info.gather(hostname, score = Some(score)))
+        Host.write_info(db, Host.Info.init(hostname = hostname, score = Some(score)))
       }
     }
   }
diff -r d9eb4807557c -r 71731d28b86d src/Pure/System/host.scala
--- a/src/Pure/System/host.scala	Wed Feb 14 15:33:52 2024 +0000
+++ b/src/Pure/System/host.scala	Wed Feb 14 17:00:47 2024 +0100
@@ -122,28 +122,22 @@
     }
     catch { case ERROR(_) => None }
 
-  def num_cpus(ssh: SSH.System = SSH.Local): Int =
-    if (ssh.is_local) Runtime.getRuntime.availableProcessors
-    else {
-      val command =
-        if (ssh.isabelle_platform.is_macos) "sysctl -n hw.ncpu" else "nproc"
-      val result = ssh.execute(command).check
-      Library.trim_line(result.out) match {
-        case Value.Int(n) => n
-        case _ => 1
-      }
-    }
-
   object Info {
-    def gather(hostname: String, ssh: SSH.System = SSH.Local, score: Option[Double] = None): Info =
-      Info(hostname, numa_nodes(ssh = ssh), num_cpus(ssh = ssh), score)
+    def init(
+      hostname: String = SSH.LOCAL,
+      ssh: SSH.System = SSH.Local,
+      score: Option[Double] = None
+    ): Info = Info(hostname, numa_nodes(ssh = ssh), Multithreading.num_processors(ssh = ssh), score)
   }
 
   sealed case class Info(
     hostname: String,
     numa_nodes: List[Int],
     num_cpus: Int,
-    benchmark_score: Option[Double])
+    benchmark_score: Option[Double]
+  ) {
+    override def toString: String = hostname
+  }
 
 
   /* shuffling of NUMA nodes */