author | wenzelm |
Sat, 17 Feb 2024 17:23:22 +0100 | |
changeset 79650 | 65ef68bab8d6 |
parent 79613 | 7a432595fb66 |
child 79758 | 68f2fe632b4c |
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 |
|
83627a092fbf
more accurate, notably on lxbroy10 and vmnipkow9;
wenzelm
parents:
79604
diff
changeset
|
26 |
var physical: Option[Int] = None |
83627a092fbf
more accurate, notably on lxbroy10 and vmnipkow9;
wenzelm
parents:
79604
diff
changeset
|
27 |
var physical_cores = Map.empty[Int, Int] |
83627a092fbf
more accurate, notably on lxbroy10 and vmnipkow9;
wenzelm
parents:
79604
diff
changeset
|
28 |
|
79607
118504de9d0d
more robust: avoid occasional problems reading this special file (e.g. SSH.Local or "lxcisa0");
wenzelm
parents:
79606
diff
changeset
|
29 |
val result = ssh.execute("cat /proc/cpuinfo").check |
118504de9d0d
more robust: avoid occasional problems reading this special file (e.g. SSH.Local or "lxcisa0");
wenzelm
parents:
79606
diff
changeset
|
30 |
for (line <- Library.trim_split_lines(result.out)) { |
79605
83627a092fbf
more accurate, notably on lxbroy10 and vmnipkow9;
wenzelm
parents:
79604
diff
changeset
|
31 |
line match { |
83627a092fbf
more accurate, notably on lxbroy10 and vmnipkow9;
wenzelm
parents:
79604
diff
changeset
|
32 |
case Physical(Value.Int(i)) => physical = Some(i) |
83627a092fbf
more accurate, notably on lxbroy10 and vmnipkow9;
wenzelm
parents:
79604
diff
changeset
|
33 |
case Cores(Value.Int(i)) |
83627a092fbf
more accurate, notably on lxbroy10 and vmnipkow9;
wenzelm
parents:
79604
diff
changeset
|
34 |
if physical.isDefined && !physical_cores.isDefinedAt(physical.get) => |
83627a092fbf
more accurate, notably on lxbroy10 and vmnipkow9;
wenzelm
parents:
79604
diff
changeset
|
35 |
physical_cores = physical_cores + (physical.get -> i) |
83627a092fbf
more accurate, notably on lxbroy10 and vmnipkow9;
wenzelm
parents:
79604
diff
changeset
|
36 |
case _ => |
83627a092fbf
more accurate, notably on lxbroy10 and vmnipkow9;
wenzelm
parents:
79604
diff
changeset
|
37 |
} |
83627a092fbf
more accurate, notably on lxbroy10 and vmnipkow9;
wenzelm
parents:
79604
diff
changeset
|
38 |
} |
79613 | 39 |
physical_cores.valuesIterator.sum max 1 |
79604
0e8ac7db1f4d
clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents:
79603
diff
changeset
|
40 |
} |
0e8ac7db1f4d
clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents:
79603
diff
changeset
|
41 |
|
0e8ac7db1f4d
clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents:
79603
diff
changeset
|
42 |
|
79603 | 43 |
/* max_threads */ |
44 |
||
79650 | 45 |
def max_threads( |
46 |
value: Int = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0, |
|
47 |
default: => Int = num_processors() |
|
48 |
): Int = { |
|
49 |
if (value > 0) value else (default max 1) min 8 |
|
79603 | 50 |
} |
51 |
} |