--- a/etc/build.props Thu Mar 02 14:41:21 2023 +0100
+++ b/etc/build.props Thu Mar 02 14:58:59 2023 +0100
@@ -163,7 +163,6 @@
src/Pure/System/linux.scala \
src/Pure/System/mingw.scala \
src/Pure/System/nodejs.scala \
- src/Pure/System/numa.scala \
src/Pure/System/options.scala \
src/Pure/System/platform.scala \
src/Pure/System/posix_interrupt.scala \
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala Thu Mar 02 14:41:21 2023 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Thu Mar 02 14:58:59 2023 +0100
@@ -215,7 +215,7 @@
progress = progress,
dirs = dirs,
select_dirs = select_dirs,
- numa_shuffling = NUMA.check(progress, numa_shuffling),
+ numa_shuffling = Host.numa_check(progress, numa_shuffling),
max_jobs = max_jobs,
verbose = verbose)
}
--- a/src/Pure/System/host.scala Thu Mar 02 14:41:21 2023 +0100
+++ b/src/Pure/System/host.scala Thu Mar 02 14:58:59 2023 +0100
@@ -1,7 +1,10 @@
/* Title: Pure/System/host.scala
Author: Makarius
-Information about compute hosts.
+Information about compute hosts, including NUMA: Non-Uniform Memory Access of
+separate CPU nodes.
+
+See also https://www.open-mpi.org/projects/hwloc notably "hwloc-ls".
*/
package isabelle
@@ -15,6 +18,77 @@
sealed case class Node_Info(hostname: String, numa_node: Option[Int])
+ /* available NUMA nodes */
+
+ private val numa_info_linux: Path = Path.explode("/sys/devices/system/node/online")
+
+ def numa_nodes(enabled: Boolean = true, ssh: SSH.System = SSH.Local): List[Int] = {
+ val Single = """^(\d+)$""".r
+ val Multiple = """^(\d+)-(\d+)$""".r
+
+ def parse(s: String): List[Int] =
+ s match {
+ case Single(Value.Int(i)) => List(i)
+ case Multiple(Value.Int(i), Value.Int(j)) => (i to j).toList
+ case _ => error("Cannot parse CPU NUMA node specification: " + quote(s))
+ }
+
+ val numa_info = if (ssh.isabelle_platform.is_linux) Some(numa_info_linux) else None
+ for {
+ path <- numa_info.toList
+ if enabled && ssh.is_file(path)
+ s <- space_explode(',', ssh.read(path).trim)
+ n <- parse(s)
+ } yield n
+ }
+
+
+ /* process policy via numactl tool */
+
+ def numactl(node: Int): String = "numactl -m" + node + " -N" + node
+ def numactl_ok(node: Int): Boolean = Isabelle_System.bash(numactl(node) + " true").ok
+
+ def process_policy(node: Int): String = if (numactl_ok(node)) numactl(node) else ""
+
+ def process_policy_options(options: Options, numa_node: Option[Int]): Options =
+ numa_node match {
+ case None => options
+ case Some(n) => options.string("ML_process_policy") = process_policy(n)
+ }
+
+ def perhaps_process_policy_options(options: Options): Options = {
+ val numa_node =
+ try {
+ numa_nodes() match {
+ case ns if ns.length >= 2 && numactl_ok(ns.head) => Some(ns.head)
+ case _ => None
+ }
+ }
+ catch { case ERROR(_) => None }
+ process_policy_options(options, numa_node)
+ }
+
+
+ /* shuffling of NUMA nodes */
+
+ def numa_check(progress: Progress, enabled: Boolean): Boolean = {
+ def warning =
+ numa_nodes() match {
+ case ns if ns.length < 2 => Some("no NUMA nodes available")
+ case ns if !numactl_ok(ns.head) => Some("bad numactl tool")
+ case _ => None
+ }
+
+ enabled &&
+ (warning match {
+ case Some(s) =>
+ progress.echo_warning("Shuffling of NUMA CPU nodes is disabled: " + s)
+ false
+ case _ => true
+ })
+ }
+
+
/* SQL data model */
object Data {
--- a/src/Pure/System/numa.scala Thu Mar 02 14:41:21 2023 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,78 +0,0 @@
-/* Title: Pure/System/numa.scala
- Author: Makarius
-
-Support for Non-Uniform Memory Access of separate CPU nodes.
-*/
-
-package isabelle
-
-
-object NUMA {
- /* information about nodes */
-
- private val numa_info_linux: Path = Path.explode("/sys/devices/system/node/online")
-
- private val Info_Single = """^(\d+)$""".r
- private val Info_Multiple = """^(\d+)-(\d+)$""".r
-
- private def parse_nodes(s: String): List[Int] =
- s match {
- case Info_Single(Value.Int(i)) => List(i)
- case Info_Multiple(Value.Int(i), Value.Int(j)) => (i to j).toList
- case _ => error("Cannot parse CPU node specification: " + quote(s))
- }
-
- def nodes(enabled: Boolean = true, ssh: SSH.System = SSH.Local): List[Int] = {
- val numa_info = if (ssh.isabelle_platform.is_linux) Some(numa_info_linux) else None
- for {
- path <- numa_info.toList
- if enabled && ssh.is_file(path)
- s <- space_explode(',', ssh.read(path).trim)
- n <- parse_nodes(s)
- } yield n
- }
-
-
- /* CPU policy via numactl tool */
-
- def numactl(node: Int): String = "numactl -m" + node + " -N" + node
- def numactl_ok(node: Int): Boolean = Isabelle_System.bash(numactl(node) + " true").ok
-
- def policy(node: Int): String = if (numactl_ok(node)) numactl(node) else ""
-
- def policy_options(options: Options, numa_node: Option[Int]): Options =
- numa_node match {
- case None => options
- case Some(n) => options.string("ML_process_policy") = policy(n)
- }
-
- def perhaps_policy_options(options: Options): Options = {
- val numa_node =
- try {
- nodes() match {
- case ns if ns.length >= 2 && numactl_ok(ns.head) => Some(ns.head)
- case _ => None
- }
- }
- catch { case ERROR(_) => None }
- policy_options(options, numa_node)
- }
-
-
- /* shuffling of CPU nodes */
-
- def check(progress: Progress, enabled: Boolean): Boolean = {
- def warning =
- nodes() match {
- case ns if ns.length < 2 => Some("no NUMA nodes available")
- case ns if !numactl_ok(ns.head) => Some("bad numactl tool")
- case _ => None
- }
-
- enabled &&
- (warning match {
- case Some(s) => progress.echo_warning("Shuffling of CPU nodes is disabled: " + s); false
- case _ => true
- })
- }
-}
--- a/src/Pure/Tools/build.scala Thu Mar 02 14:41:21 2023 +0100
+++ b/src/Pure/Tools/build.scala Thu Mar 02 14:58:59 2023 +0100
@@ -317,7 +317,7 @@
clean_build = clean_build,
dirs = dirs,
select_dirs = select_dirs,
- numa_shuffling = NUMA.check(progress, numa_shuffling),
+ numa_shuffling = Host.numa_check(progress, numa_shuffling),
max_jobs = max_jobs,
list_files = list_files,
check_keywords = check_keywords,
--- a/src/Pure/Tools/build_job.scala Thu Mar 02 14:41:21 2023 +0100
+++ b/src/Pure/Tools/build_job.scala Thu Mar 02 14:58:59 2023 +0100
@@ -112,7 +112,7 @@
def job_name: String = session_name
val info: Sessions.Info = session_background.sessions_structure(session_name)
- val options: Options = NUMA.policy_options(info.options, node_info.numa_node)
+ val options: Options = Host.process_policy_options(info.options, node_info.numa_node)
val session_sources: Sessions.Sources =
Sessions.Sources.load(session_background.base, cache = store.cache.compress)
--- a/src/Pure/Tools/build_process.scala Thu Mar 02 14:41:21 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Thu Mar 02 14:58:59 2023 +0100
@@ -78,7 +78,7 @@
}
}
- val numa_nodes = NUMA.nodes(enabled = numa_shuffling)
+ val numa_nodes = Host.numa_nodes(enabled = numa_shuffling)
new Context(store, build_deps, sessions, ordering, progress, hostname, numa_nodes,
build_heap = build_heap, max_jobs = max_jobs, fresh_build = fresh_build,
no_build = no_build, verbose = verbose, session_setup, uuid = uuid)
--- a/src/Pure/Tools/dump.scala Thu Mar 02 14:41:21 2023 +0100
+++ b/src/Pure/Tools/dump.scala Thu Mar 02 14:58:59 2023 +0100
@@ -98,7 +98,7 @@
): Context = {
val session_options: Options = {
val options1 =
- NUMA.perhaps_policy_options(options) +
+ Host.perhaps_process_policy_options(options) +
"parallel_proofs=0" +
"completion_limit=0" +
"editor_tracing_messages=0"
--- a/src/Pure/Tools/update.scala Thu Mar 02 14:41:21 2023 +0100
+++ b/src/Pure/Tools/update.scala Thu Mar 02 14:58:59 2023 +0100
@@ -220,7 +220,7 @@
clean_build,
dirs = dirs,
select_dirs = select_dirs,
- numa_shuffling = NUMA.check(progress, numa_shuffling),
+ numa_shuffling = Host.numa_check(progress, numa_shuffling),
max_jobs = max_jobs,
fresh_build,
no_build = no_build,