author | wenzelm |
Mon, 06 Mar 2023 21:12:47 +0100 | |
changeset 77552 | 080422b3d914 |
parent 77550 | ed2f53e1552c |
child 78174 | cc0bd66eb498 |
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 { |
|
77549 | 15 |
/* process policy via numactl tool */ |
16 |
||
17 |
def numactl(node: Int): String = "numactl -m" + node + " -N" + node |
|
18 |
def numactl_ok(node: Int): Boolean = Isabelle_System.bash(numactl(node) + " true").ok |
|
19 |
||
20 |
def process_policy(options: Options, numa_node: Option[Int]): Options = |
|
21 |
numa_node match { |
|
22 |
case None => options |
|
23 |
case Some(node) => |
|
24 |
options.string("process_policy") = if (numactl_ok(node)) numactl(node) else "" |
|
25 |
} |
|
26 |
||
27 |
||
77475 | 28 |
/* allocated resources */ |
29 |
||
30 |
object Node_Info { def none: Node_Info = Node_Info("", None) } |
|
31 |
||
77526 | 32 |
sealed case class Node_Info(hostname: String, numa_node: Option[Int]) { |
33 |
override def toString: String = |
|
34 |
hostname + if_proper(numa_node, "/" + numa_node.get.toString) |
|
77550 | 35 |
|
36 |
def process_policy(options: Options): Options = |
|
37 |
Host.process_policy(options, numa_node) |
|
77526 | 38 |
} |
77476 | 39 |
|
40 |
||
77477 | 41 |
/* available NUMA nodes */ |
42 |
||
43 |
private val numa_info_linux: Path = Path.explode("/sys/devices/system/node/online") |
|
44 |
||
45 |
def numa_nodes(enabled: Boolean = true, ssh: SSH.System = SSH.Local): List[Int] = { |
|
46 |
val Single = """^(\d+)$""".r |
|
47 |
val Multiple = """^(\d+)-(\d+)$""".r |
|
48 |
||
49 |
def parse(s: String): List[Int] = |
|
50 |
s match { |
|
51 |
case Single(Value.Int(i)) => List(i) |
|
52 |
case Multiple(Value.Int(i), Value.Int(j)) => (i to j).toList |
|
53 |
case _ => error("Cannot parse CPU NUMA node specification: " + quote(s)) |
|
54 |
} |
|
55 |
||
56 |
val numa_info = if (ssh.isabelle_platform.is_linux) Some(numa_info_linux) else None |
|
57 |
for { |
|
58 |
path <- numa_info.toList |
|
59 |
if enabled && ssh.is_file(path) |
|
60 |
s <- space_explode(',', ssh.read(path).trim) |
|
61 |
n <- parse(s) |
|
62 |
} yield n |
|
63 |
} |
|
64 |
||
77548 | 65 |
def numa_node0(): Option[Int] = |
66 |
try { |
|
67 |
numa_nodes() match { |
|
68 |
case ns if ns.length >= 2 && numactl_ok(ns.head) => Some(ns.head) |
|
69 |
case _ => None |
|
70 |
} |
|
71 |
} |
|
72 |
catch { case ERROR(_) => None } |
|
73 |
||
74 |
||
77477 | 75 |
|
76 |
/* shuffling of NUMA nodes */ |
|
77 |
||
78 |
def numa_check(progress: Progress, enabled: Boolean): Boolean = { |
|
79 |
def warning = |
|
80 |
numa_nodes() match { |
|
81 |
case ns if ns.length < 2 => Some("no NUMA nodes available") |
|
82 |
case ns if !numactl_ok(ns.head) => Some("bad numactl tool") |
|
83 |
case _ => None |
|
84 |
} |
|
85 |
||
86 |
enabled && |
|
87 |
(warning match { |
|
88 |
case Some(s) => |
|
89 |
progress.echo_warning("Shuffling of NUMA CPU nodes is disabled: " + s) |
|
90 |
false |
|
91 |
case _ => true |
|
92 |
}) |
|
93 |
} |
|
94 |
||
95 |
||
77476 | 96 |
/* SQL data model */ |
97 |
||
98 |
object Data { |
|
99 |
def make_table(name: String, columns: List[SQL.Column], body: String = ""): SQL.Table = |
|
100 |
SQL.Table("isabelle_host" + if_proper(name, "_" + name), columns, body = body) |
|
101 |
||
102 |
object Node_Info { |
|
103 |
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
|
104 |
val numa_next = SQL.Column.int("numa_next") |
77476 | 105 |
|
77525
de6fb423fd4b
clarified database content: store actual value instead of index;
wenzelm
parents:
77483
diff
changeset
|
106 |
val table = make_table("node_info", List(hostname, numa_next)) |
77476 | 107 |
} |
108 |
||
77525
de6fb423fd4b
clarified database content: store actual value instead of index;
wenzelm
parents:
77483
diff
changeset
|
109 |
def read_numa_next(db: SQL.Database, hostname: String): Int = |
77552 | 110 |
db.execute_query_statementO[Int]( |
77525
de6fb423fd4b
clarified database content: store actual value instead of index;
wenzelm
parents:
77483
diff
changeset
|
111 |
Node_Info.table.select(List(Node_Info.numa_next), |
77552 | 112 |
sql = Node_Info.hostname.where_equal(hostname)), |
113 |
res => res.int(Node_Info.numa_next) |
|
114 |
).getOrElse(0) |
|
77476 | 115 |
|
77525
de6fb423fd4b
clarified database content: store actual value instead of index;
wenzelm
parents:
77483
diff
changeset
|
116 |
def update_numa_next(db: SQL.Database, hostname: String, numa_next: Int): Boolean = |
de6fb423fd4b
clarified database content: store actual value instead of index;
wenzelm
parents:
77483
diff
changeset
|
117 |
if (read_numa_next(db, hostname) != numa_next) { |
77543 | 118 |
db.execute_statement(Node_Info.table.delete(sql = Node_Info.hostname.where_equal(hostname))) |
77541 | 119 |
db.execute_statement(Node_Info.table.insert(), body = |
120 |
{ stmt => |
|
121 |
stmt.string(1) = hostname |
|
122 |
stmt.int(2) = numa_next |
|
123 |
}) |
|
77476 | 124 |
true |
125 |
} |
|
126 |
else false |
|
127 |
} |
|
77475 | 128 |
} |