author | wenzelm |
Fri, 01 Apr 2022 17:06:10 +0200 | |
changeset 75393 | 87ebf5a50283 |
parent 71601 | 97ccf48c2f0c |
child 77316 | d17b0851a61a |
permissions | -rw-r--r-- |
64264
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/System/numa.scala |
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
3 |
|
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
4 |
Support for Non-Uniform Memory Access of separate CPU nodes. |
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
6 |
|
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
8 |
|
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
9 |
|
75393 | 10 |
object NUMA { |
64264
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
11 |
/* available nodes */ |
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
12 |
|
75393 | 13 |
def nodes(): List[Int] = { |
64264
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
14 |
val numa_nodes_linux = Path.explode("/sys/devices/system/node/online") |
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
15 |
|
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
16 |
val Single = """^(\d+)$""".r |
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
17 |
val Multiple = """^(\d+)-(\d+)$""".r |
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
18 |
|
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
19 |
def read(s: String): List[Int] = |
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
20 |
s match { |
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
21 |
case Single(Value.Int(i)) => List(i) |
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
22 |
case Multiple(Value.Int(i), Value.Int(j)) => (i to j).toList |
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
23 |
case _ => error("Cannot parse CPU node specification: " + quote(s)) |
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
24 |
} |
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
25 |
|
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
26 |
if (numa_nodes_linux.is_file) { |
71601 | 27 |
space_explode(',', File.read(numa_nodes_linux).trim).flatMap(read) |
64264
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
28 |
} |
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
29 |
else Nil |
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
30 |
} |
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
31 |
|
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
32 |
|
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
33 |
/* CPU policy via numactl tool */ |
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
34 |
|
68955
0851db8cde12
more robust test: virtualization may provide misleading information;
wenzelm
parents:
68954
diff
changeset
|
35 |
lazy val numactl_available: Boolean = Isabelle_System.bash("numactl -m0 -N0 true").ok |
64264
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
36 |
|
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
37 |
def policy(node: Int): String = |
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
38 |
if (numactl_available) "numactl -m" + node + " -N" + node else "" |
64265 | 39 |
|
68954
8be4030394b8
implicit use of NUMA policy, absorbing potential errors;
wenzelm
parents:
68953
diff
changeset
|
40 |
def policy_options(options: Options, numa_node: Option[Int] = Some(0)): Options = |
68953 | 41 |
numa_node match { |
42 |
case None => options |
|
43 |
case Some(n) => options.string("ML_process_policy") = policy(n) |
|
44 |
} |
|
45 |
||
64265 | 46 |
|
47 |
/* shuffling of CPU nodes */ |
|
48 |
||
68954
8be4030394b8
implicit use of NUMA policy, absorbing potential errors;
wenzelm
parents:
68953
diff
changeset
|
49 |
def enabled: Boolean = |
8be4030394b8
implicit use of NUMA policy, absorbing potential errors;
wenzelm
parents:
68953
diff
changeset
|
50 |
try { nodes().length >= 2 && numactl_available } |
8be4030394b8
implicit use of NUMA policy, absorbing potential errors;
wenzelm
parents:
68953
diff
changeset
|
51 |
catch { case ERROR(_) => false } |
8be4030394b8
implicit use of NUMA policy, absorbing potential errors;
wenzelm
parents:
68953
diff
changeset
|
52 |
|
75393 | 53 |
def enabled_warning(progress: Progress, enabled: Boolean): Boolean = { |
64265 | 54 |
def warning = |
55 |
if (nodes().length < 2) Some("no NUMA nodes available") |
|
68956 | 56 |
else if (!numactl_available) Some("bad numactl tool") |
64265 | 57 |
else None |
58 |
||
59 |
enabled && |
|
60 |
(warning match { |
|
65831 | 61 |
case Some(s) => progress.echo_warning("Shuffling of CPU nodes is disabled: " + s); false |
64265 | 62 |
case _ => true |
63 |
}) |
|
64 |
} |
|
65 |
||
75393 | 66 |
class Nodes(enabled: Boolean = true) { |
64265 | 67 |
private val available = nodes().zipWithIndex |
68 |
private var next_index = 0 |
|
69 |
||
70 |
def next(used: Int => Boolean = _ => false): Option[Int] = synchronized { |
|
71 |
if (!enabled || available.isEmpty) None |
|
72 |
else { |
|
73 |
val candidates = available.drop(next_index) ::: available.take(next_index) |
|
74 |
val (n, i) = |
|
75 |
candidates.find({ case (n, i) => i == next_index && !used(n) }) orElse |
|
76 |
candidates.find({ case (n, _) => !used(n) }) getOrElse candidates.head |
|
77 |
next_index = (i + 1) % available.length |
|
78 |
Some(n) |
|
79 |
} |
|
80 |
} |
|
81 |
} |
|
64264
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff
changeset
|
82 |
} |