author | wenzelm |
Wed, 29 Nov 2023 00:07:54 +0100 | |
changeset 79074 | 7f24c5be57bd |
parent 78848 | 26a43785590b |
child 79602 | 9ba800f12785 |
permissions | -rw-r--r-- |
77475 | 1 |
/* Title: Pure/System/host.scala |
2 |
Author: Makarius |
|
3 |
||
77477 | 4 |
Information about compute hosts, including NUMA: Non-Uniform Memory Access of |
5 |
separate CPU nodes. |
|
6 |
||
77478 | 7 |
See also https://www.open-mpi.org/projects/hwloc --- notably "lstopo" or |
8 |
"hwloc-ls" (e.g. via Ubuntu package "hwloc"). |
|
77475 | 9 |
*/ |
10 |
||
11 |
package isabelle |
|
12 |
||
13 |
||
14 |
object Host { |
|
78837
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
15 |
|
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
16 |
object Range { |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
17 |
val Single = """^(\d+)$""".r |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
18 |
val Multiple = """^(\d+)-(\d+)$""".r |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
19 |
|
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
20 |
def apply(range: List[Int]): String = |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
21 |
range match { |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
22 |
case Nil => "" |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
23 |
case x :: xs => |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
24 |
def elem(start: Int, stop: Int): String = |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
25 |
if (start == stop) start.toString else start.toString + "-" + stop.toString |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
26 |
|
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
27 |
val (elems, (r0, rn)) = |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
28 |
xs.foldLeft((List.empty[String], (x, x))) { |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
29 |
case ((rs, (r0, rn)), x) => |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
30 |
if (rn + 1 == x) (rs, (r0, x)) else (rs :+ elem(r0, rn), (x, x)) |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
31 |
} |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
32 |
|
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
33 |
(elems :+ elem(r0, rn)).mkString(",") |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
34 |
} |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
35 |
|
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
36 |
def unapply(s: String): Option[List[Int]] = |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
37 |
space_explode(',', s).foldRight(Option(List.empty[Int])) { |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
38 |
case (Single(Value.Int(i)), Some(elems)) => Some(i :: elems) |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
39 |
case (Multiple(Value.Int(i), Value.Int(j)), Some(elems)) => Some((i to j).toList ::: elems) |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
40 |
case _ => None |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
41 |
} |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
42 |
|
78847 | 43 |
def from(s: String): List[Int] = |
78837
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
44 |
s match { |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
45 |
case Range(r) => r |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
46 |
case _ => Nil |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
47 |
} |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
48 |
} |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
49 |
|
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
50 |
|
78839
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
51 |
/* process policy via numactl and taskset tools */ |
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
52 |
|
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
53 |
def taskset(cpus: List[Int]): String = "taskset --cpu-list " + Range(cpus) |
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
54 |
def taskset_ok(cpus: List[Int]): Boolean = Isabelle_System.bash(taskset(cpus) + " true").ok |
77549 | 55 |
|
78839
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
56 |
def numactl(node: Int, rel_cpus: List[Int] = Nil): String = |
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
57 |
"numactl -m" + node + " -N" + node + if_proper(rel_cpus, " -C+" + Range(rel_cpus)) |
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
58 |
def numactl_ok(node: Int, rel_cpus: List[Int] = Nil): Boolean = |
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
59 |
Isabelle_System.bash(numactl(node, rel_cpus) + " true").ok |
77549 | 60 |
|
78839
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
61 |
def numa_options(options: Options, numa_node: Option[Int]): Options = |
77549 | 62 |
numa_node match { |
63 |
case None => options |
|
64 |
case Some(node) => |
|
65 |
options.string("process_policy") = if (numactl_ok(node)) numactl(node) else "" |
|
66 |
} |
|
67 |
||
78839
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
68 |
def node_options(options: Options, node: Node_Info): Options = { |
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
69 |
val threads_options = |
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
70 |
if (node.rel_cpus.isEmpty) options else options.int("threads") = node.rel_cpus.length |
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
71 |
|
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
72 |
node.numa_node match { |
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
73 |
case None if node.rel_cpus.isEmpty => |
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
74 |
threads_options |
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
75 |
case Some(numa_node) => |
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
76 |
threads_options.string("process_policy") = |
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
77 |
if (numactl_ok(numa_node, node.rel_cpus)) numactl(numa_node, node.rel_cpus) else "" |
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
78 |
case _ => |
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
79 |
threads_options.string("process_policy") = |
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
80 |
if (taskset_ok(node.rel_cpus)) taskset(node.rel_cpus) else "" |
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
81 |
} |
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
82 |
} |
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
83 |
|
77549 | 84 |
|
77475 | 85 |
/* allocated resources */ |
86 |
||
78839
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
87 |
object Node_Info { def none: Node_Info = Node_Info("", None, Nil) } |
77475 | 88 |
|
78839
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
89 |
sealed case class Node_Info(hostname: String, numa_node: Option[Int], rel_cpus: List[Int]) { |
77526 | 90 |
override def toString: String = |
78839
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
91 |
hostname + |
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
92 |
if_proper(numa_node, "/" + numa_node.get.toString) + |
7799ec03b8bd
generalized node infos: allow addressing of numa node segments via relative cpus;
Fabian Huch <huch@in.tum.de>
parents:
78838
diff
changeset
|
93 |
if_proper(rel_cpus, "+" + Range(rel_cpus)) |
77526 | 94 |
} |
77476 | 95 |
|
96 |
||
78838
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
97 |
/* statically available resources */ |
77477 | 98 |
|
99 |
private val numa_info_linux: Path = Path.explode("/sys/devices/system/node/online") |
|
100 |
||
78837
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
101 |
def parse_numa_info(numa_info: String): List[Int] = |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
102 |
numa_info match { |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
103 |
case Range(nodes) => nodes |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
104 |
case s => error("Cannot parse CPU NUMA node specification: " + quote(s)) |
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
105 |
} |
77477 | 106 |
|
78837
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
107 |
def numa_nodes(enabled: Boolean = true, ssh: SSH.System = SSH.Local): List[Int] = { |
77477 | 108 |
val numa_info = if (ssh.isabelle_platform.is_linux) Some(numa_info_linux) else None |
109 |
for { |
|
110 |
path <- numa_info.toList |
|
111 |
if enabled && ssh.is_file(path) |
|
78837
f97e23eaa628
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
Fabian Huch <huch@in.tum.de>
parents:
78435
diff
changeset
|
112 |
n <- parse_numa_info(ssh.read(path).trim) |
77477 | 113 |
} yield n |
114 |
} |
|
115 |
||
77548 | 116 |
def numa_node0(): Option[Int] = |
117 |
try { |
|
118 |
numa_nodes() match { |
|
119 |
case ns if ns.length >= 2 && numactl_ok(ns.head) => Some(ns.head) |
|
120 |
case _ => None |
|
121 |
} |
|
122 |
} |
|
123 |
catch { case ERROR(_) => None } |
|
124 |
||
78848 | 125 |
def num_cpus(ssh: SSH.System = SSH.Local): Int = |
126 |
if (ssh.is_local) Runtime.getRuntime.availableProcessors |
|
127 |
else { |
|
128 |
val command = |
|
129 |
if (ssh.isabelle_platform.is_macos) "sysctl -n hw.ncpu" else "nproc" |
|
130 |
val result = ssh.execute(command).check |
|
131 |
Library.trim_line(result.out) match { |
|
132 |
case Value.Int(n) => n |
|
133 |
case _ => 1 |
|
134 |
} |
|
135 |
} |
|
78838
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
136 |
|
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
137 |
object Info { |
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78839
diff
changeset
|
138 |
def gather(hostname: String, ssh: SSH.System = SSH.Local, score: Option[Double] = None): Info = |
78848 | 139 |
Info(hostname, numa_nodes(ssh = ssh), num_cpus(ssh = ssh), score) |
78838
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
140 |
} |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
141 |
|
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
142 |
sealed case class Info( |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
143 |
hostname: String, |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
144 |
numa_nodes: List[Int], |
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78839
diff
changeset
|
145 |
num_cpus: Int, |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78839
diff
changeset
|
146 |
benchmark_score: Option[Double]) |
77548 | 147 |
|
77477 | 148 |
|
149 |
/* shuffling of NUMA nodes */ |
|
150 |
||
151 |
def numa_check(progress: Progress, enabled: Boolean): Boolean = { |
|
152 |
def warning = |
|
153 |
numa_nodes() match { |
|
154 |
case ns if ns.length < 2 => Some("no NUMA nodes available") |
|
155 |
case ns if !numactl_ok(ns.head) => Some("bad numactl tool") |
|
156 |
case _ => None |
|
157 |
} |
|
158 |
||
159 |
enabled && |
|
160 |
(warning match { |
|
161 |
case Some(s) => |
|
162 |
progress.echo_warning("Shuffling of NUMA CPU nodes is disabled: " + s) |
|
163 |
false |
|
164 |
case _ => true |
|
165 |
}) |
|
166 |
} |
|
167 |
||
168 |
||
77476 | 169 |
/* SQL data model */ |
170 |
||
78396
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78356
diff
changeset
|
171 |
object private_data extends SQL.Data("isabelle_host") { |
78174
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
172 |
val database: Path = Path.explode("$ISABELLE_HOME_USER/host.db") |
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
173 |
|
78838
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
174 |
override lazy val tables = SQL.Tables(Node_Info.table, Info.table) |
77476 | 175 |
|
176 |
object Node_Info { |
|
177 |
val hostname = SQL.Column.string("hostname").make_primary_key |
|
77525
de6fb423fd4b
clarified database content: store actual value instead of index;
wenzelm
parents:
77483
diff
changeset
|
178 |
val numa_next = SQL.Column.int("numa_next") |
77476 | 179 |
|
78266 | 180 |
val table = make_table(List(hostname, numa_next), name = "node_info") |
77476 | 181 |
} |
182 |
||
77525
de6fb423fd4b
clarified database content: store actual value instead of index;
wenzelm
parents:
77483
diff
changeset
|
183 |
def read_numa_next(db: SQL.Database, hostname: String): Int = |
77552 | 184 |
db.execute_query_statementO[Int]( |
77525
de6fb423fd4b
clarified database content: store actual value instead of index;
wenzelm
parents:
77483
diff
changeset
|
185 |
Node_Info.table.select(List(Node_Info.numa_next), |
77552 | 186 |
sql = Node_Info.hostname.where_equal(hostname)), |
187 |
res => res.int(Node_Info.numa_next) |
|
188 |
).getOrElse(0) |
|
77476 | 189 |
|
78174
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
190 |
def write_numa_next(db: SQL.Database, hostname: String, numa_next: Int): Unit = { |
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
191 |
db.execute_statement(Node_Info.table.delete(sql = Node_Info.hostname.where_equal(hostname))) |
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
192 |
db.execute_statement(Node_Info.table.insert(), body = |
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
193 |
{ stmt => |
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
194 |
stmt.string(1) = hostname |
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
195 |
stmt.int(2) = numa_next |
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
196 |
}) |
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
197 |
} |
78838
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
198 |
|
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
199 |
object Info { |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
200 |
val hostname = SQL.Column.string("hostname").make_primary_key |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
201 |
val numa_info = SQL.Column.string("numa_info") |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
202 |
val num_cpus = SQL.Column.int("num_cpus") |
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78839
diff
changeset
|
203 |
val benchmark_score = SQL.Column.double("benchmark_score") |
78838
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
204 |
|
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
205 |
val table = |
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78839
diff
changeset
|
206 |
make_table(List(hostname, numa_info, num_cpus, benchmark_score), name = "info") |
78838
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
207 |
} |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
208 |
|
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
209 |
def write_info(db: SQL.Database, info: Info): Unit = { |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
210 |
db.execute_statement(Info.table.delete(sql = Info.hostname.where_equal(info.hostname))) |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
211 |
db.execute_statement(Info.table.insert(), body = |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
212 |
{ stmt => |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
213 |
stmt.string(1) = info.hostname |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
214 |
stmt.string(2) = info.numa_nodes.mkString(",") |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
215 |
stmt.int(3) = info.num_cpus |
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78839
diff
changeset
|
216 |
stmt.double(4) = info.benchmark_score |
78838
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
217 |
}) |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
218 |
} |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
219 |
|
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
220 |
def read_info(db: SQL.Database, hostname: String): Option[Host.Info] = |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
221 |
db.execute_query_statementO[Host.Info]( |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
222 |
Info.table.select(Info.table.columns.tail, sql = Info.hostname.where_equal(hostname)), |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
223 |
{ res => |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
224 |
val numa_info = res.string(Info.numa_info) |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
225 |
val num_cpus = res.int(Info.num_cpus) |
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78839
diff
changeset
|
226 |
val benchmark_score = res.get_double(Info.benchmark_score) |
78838
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
227 |
|
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78839
diff
changeset
|
228 |
Host.Info(hostname, parse_numa_info(numa_info), num_cpus, benchmark_score) |
78838
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
229 |
}) |
78174
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
230 |
} |
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
231 |
|
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
232 |
def next_numa_node( |
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
233 |
db: SQL.Database, |
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
234 |
hostname: String, |
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
235 |
available_nodes: List[Int], |
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
236 |
used_nodes: => Set[Int] |
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
237 |
): Option[Int] = |
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
238 |
if (available_nodes.isEmpty) None |
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
239 |
else { |
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
240 |
val available = available_nodes.zipWithIndex |
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
241 |
val used = used_nodes |
78396
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78356
diff
changeset
|
242 |
private_data.transaction_lock(db, create = true, label = "Host.next_numa_node") { |
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78356
diff
changeset
|
243 |
val numa_next = private_data.read_numa_next(db, hostname) |
78174
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
244 |
val numa_index = available.collectFirst({ case (n, i) if n == numa_next => i }).getOrElse(0) |
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
245 |
val candidates = available.drop(numa_index) ::: available.take(numa_index) |
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
246 |
val (n, i) = |
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
247 |
candidates.find({ case (n, i) => i == numa_index && !used(n) }) orElse |
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
248 |
candidates.find({ case (n, _) => !used(n) }) getOrElse candidates.head |
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
249 |
|
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
250 |
val numa_next1 = available_nodes((i + 1) % available_nodes.length) |
78396
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78356
diff
changeset
|
251 |
if (numa_next != numa_next1) private_data.write_numa_next(db, hostname, numa_next1) |
78174
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
252 |
|
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
253 |
Some(n) |
77476 | 254 |
} |
78174
cc0bd66eb498
separate host.db for independent db.transaction_lock;
wenzelm
parents:
77552
diff
changeset
|
255 |
} |
78838
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
256 |
|
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
257 |
def write_info(db: SQL.Database, info: Info): Unit = |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
258 |
private_data.transaction_lock(db, create = true, label = "Host.write_info") { |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
259 |
private_data.write_info(db, info) |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
260 |
} |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
261 |
def read_info(db: SQL.Database, hostname: String): Option[Host.Info] = |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
262 |
private_data.transaction_lock(db, create = true, label = "Host.read_info") { |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
263 |
private_data.read_info(db, hostname) |
4b014e6c1dfe
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
Fabian Huch <huch@in.tum.de>
parents:
78837
diff
changeset
|
264 |
} |
77475 | 265 |
} |