author | haftmann |
Wed, 21 May 2025 20:13:43 +0200 | |
changeset 82648 | 35e40c60c680 |
parent 79759 | 5492439ffe89 |
permissions | -rw-r--r-- |
79603 | 1 |
/* Title: Pure/Concurrent/multithreading.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Multithreading in Isabelle/Scala. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
object Multithreading { |
|
79604
0e8ac7db1f4d
clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents:
79603
diff
changeset
|
11 |
/* physical processors */ |
0e8ac7db1f4d
clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents:
79603
diff
changeset
|
12 |
|
79605
83627a092fbf
more accurate, notably on lxbroy10 and vmnipkow9;
wenzelm
parents:
79604
diff
changeset
|
13 |
// slightly different from Poly/ML (more accurate) |
79604
0e8ac7db1f4d
clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents:
79603
diff
changeset
|
14 |
def num_processors(ssh: SSH.System = SSH.Local): Int = |
0e8ac7db1f4d
clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents:
79603
diff
changeset
|
15 |
if (ssh.isabelle_platform.is_macos) { |
0e8ac7db1f4d
clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents:
79603
diff
changeset
|
16 |
val result = ssh.execute("sysctl -n hw.physicalcpu").check |
0e8ac7db1f4d
clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents:
79603
diff
changeset
|
17 |
Library.trim_line(result.out) match { |
79613 | 18 |
case Value.Int(n) => n max 1 |
79604
0e8ac7db1f4d
clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents:
79603
diff
changeset
|
19 |
case _ => 1 |
0e8ac7db1f4d
clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents:
79603
diff
changeset
|
20 |
} |
0e8ac7db1f4d
clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents:
79603
diff
changeset
|
21 |
} |
0e8ac7db1f4d
clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents:
79603
diff
changeset
|
22 |
else { |
79605
83627a092fbf
more accurate, notably on lxbroy10 and vmnipkow9;
wenzelm
parents:
79604
diff
changeset
|
23 |
val Physical = """^\s*physical id\s*:\s*(\d+)\s*$""".r |
83627a092fbf
more accurate, notably on lxbroy10 and vmnipkow9;
wenzelm
parents:
79604
diff
changeset
|
24 |
val Cores = """^\s*cpu cores\s*:\s*(\d+)\s*$""".r |
83627a092fbf
more accurate, notably on lxbroy10 and vmnipkow9;
wenzelm
parents:
79604
diff
changeset
|
25 |
|
79758 | 26 |
val physical_cores: Int = { |
27 |
var physical: Option[Int] = None |
|
28 |
var cores = Map.empty[Int, Int] |
|
79605
83627a092fbf
more accurate, notably on lxbroy10 and vmnipkow9;
wenzelm
parents:
79604
diff
changeset
|
29 |
|
79758 | 30 |
val result = ssh.execute("cat /proc/cpuinfo").check |
31 |
for (line <- Library.trim_split_lines(result.out)) { |
|
32 |
line match { |
|
33 |
case Physical(Value.Int(i)) => physical = Some(i) |
|
34 |
case Cores(Value.Int(i)) |
|
35 |
if physical.isDefined && !cores.isDefinedAt(physical.get) => |
|
36 |
cores = cores + (physical.get -> i) |
|
37 |
case _ => |
|
38 |
} |
|
79605
83627a092fbf
more accurate, notably on lxbroy10 and vmnipkow9;
wenzelm
parents:
79604
diff
changeset
|
39 |
} |
79758 | 40 |
cores.valuesIterator.sum |
79605
83627a092fbf
more accurate, notably on lxbroy10 and vmnipkow9;
wenzelm
parents:
79604
diff
changeset
|
41 |
} |
79759
5492439ffe89
more robust: imitate Isabelle/ML operation more closely (after 26a43785590b);
wenzelm
parents:
79758
diff
changeset
|
42 |
|
5492439ffe89
more robust: imitate Isabelle/ML operation more closely (after 26a43785590b);
wenzelm
parents:
79758
diff
changeset
|
43 |
def logical_cores(): Int = |
5492439ffe89
more robust: imitate Isabelle/ML operation more closely (after 26a43785590b);
wenzelm
parents:
79758
diff
changeset
|
44 |
if (ssh.is_local) Runtime.getRuntime.availableProcessors() |
5492439ffe89
more robust: imitate Isabelle/ML operation more closely (after 26a43785590b);
wenzelm
parents:
79758
diff
changeset
|
45 |
else { |
5492439ffe89
more robust: imitate Isabelle/ML operation more closely (after 26a43785590b);
wenzelm
parents:
79758
diff
changeset
|
46 |
Library.trim_line(ssh.execute("nproc").check.out) match { |
5492439ffe89
more robust: imitate Isabelle/ML operation more closely (after 26a43785590b);
wenzelm
parents:
79758
diff
changeset
|
47 |
case Value.Nat(n) => n |
5492439ffe89
more robust: imitate Isabelle/ML operation more closely (after 26a43785590b);
wenzelm
parents:
79758
diff
changeset
|
48 |
case _ => 1 |
5492439ffe89
more robust: imitate Isabelle/ML operation more closely (after 26a43785590b);
wenzelm
parents:
79758
diff
changeset
|
49 |
} |
5492439ffe89
more robust: imitate Isabelle/ML operation more closely (after 26a43785590b);
wenzelm
parents:
79758
diff
changeset
|
50 |
} |
5492439ffe89
more robust: imitate Isabelle/ML operation more closely (after 26a43785590b);
wenzelm
parents:
79758
diff
changeset
|
51 |
|
5492439ffe89
more robust: imitate Isabelle/ML operation more closely (after 26a43785590b);
wenzelm
parents:
79758
diff
changeset
|
52 |
if (physical_cores > 0) physical_cores else logical_cores() |
79604
0e8ac7db1f4d
clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents:
79603
diff
changeset
|
53 |
} |
0e8ac7db1f4d
clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents:
79603
diff
changeset
|
54 |
|
0e8ac7db1f4d
clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents:
79603
diff
changeset
|
55 |
|
79603 | 56 |
/* max_threads */ |
57 |
||
79650 | 58 |
def max_threads( |
59 |
value: Int = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0, |
|
60 |
default: => Int = num_processors() |
|
61 |
): Int = { |
|
62 |
if (value > 0) value else (default max 1) min 8 |
|
79603 | 63 |
} |
64 |
} |