--- a/src/Pure/Concurrent/multithreading.ML Wed Feb 14 14:16:56 2024 +0100
+++ b/src/Pure/Concurrent/multithreading.ML Wed Feb 14 14:41:18 2024 +0100
@@ -8,6 +8,7 @@
signature MULTITHREADING =
sig
+ val num_processors: unit -> int
val max_threads: unit -> int
val max_threads_update: int -> unit
val parallel_proofs: int ref
@@ -22,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
--- a/src/Pure/Concurrent/multithreading.scala Wed Feb 14 14:16:56 2024 +0100
+++ b/src/Pure/Concurrent/multithreading.scala Wed Feb 14 14:41:18 2024 +0100
@@ -8,10 +8,27 @@
object Multithreading {
+ /* physical processors */
+
+ 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 Core_Id = """^\s*core id\s*:\s*(\d+)\s*$""".r
+ val cpuinfo = ssh.read(Path.explode("/proc/cpuinfo"))
+ (for (case Core_Id(Value.Int(i)) <- Library.trim_split_lines(cpuinfo)) yield i).toSet.size
+ }
+
+
/* max_threads */
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
+ if (m > 0) m else (num_processors() max 1) min 8
}
}