--- 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 \
--- 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)
--- 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(
--- 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
--- /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
+ }
+}
--- 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)))
}
}
}
--- 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 */