author | wenzelm |
Thu, 15 Feb 2024 09:53:58 +0100 | |
changeset 79613 | 7a432595fb66 |
parent 79607 | 118504de9d0d |
child 79650 | 65ef68bab8d6 |
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 |
||
45 |
def max_threads(): Int = { |
|
46 |
val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0 |
|
79613 | 47 |
if (m > 0) m else num_processors() min 8 |
79603 | 48 |
} |
49 |
} |