author | wenzelm |
Sun, 03 Mar 2024 16:32:59 +0100 | |
changeset 79758 | 68f2fe632b4c |
parent 79650 | 65ef68bab8d6 |
child 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 |
} |
79758 | 42 |
if (physical_cores > 1) physical_cores else 1 |
79604
0e8ac7db1f4d
clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents:
79603
diff
changeset
|
43 |
} |
0e8ac7db1f4d
clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents:
79603
diff
changeset
|
44 |
|
0e8ac7db1f4d
clarified num_processors: follow Poly/ML (with its inaccuracies);
wenzelm
parents:
79603
diff
changeset
|
45 |
|
79603 | 46 |
/* max_threads */ |
47 |
||
79650 | 48 |
def max_threads( |
49 |
value: Int = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0, |
|
50 |
default: => Int = num_processors() |
|
51 |
): Int = { |
|
52 |
if (value > 0) value else (default max 1) min 8 |
|
79603 | 53 |
} |
54 |
} |