# HG changeset patch # User wenzelm # Date 1677765539 -3600 # Node ID f376aebca9c1a644fa395e7753ca890e127ea814 # Parent 5f6f567a2661bf479489248e46f343a1f77fdd04 clarified modules; tuned signature; tuned comments; diff -r 5f6f567a2661 -r f376aebca9c1 etc/build.props --- 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 \ diff -r 5f6f567a2661 -r f376aebca9c1 src/HOL/Tools/Mirabelle/mirabelle.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) } diff -r 5f6f567a2661 -r f376aebca9c1 src/Pure/System/host.scala --- 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 { diff -r 5f6f567a2661 -r f376aebca9c1 src/Pure/System/numa.scala --- 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 - }) - } -} diff -r 5f6f567a2661 -r f376aebca9c1 src/Pure/Tools/build.scala --- 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, diff -r 5f6f567a2661 -r f376aebca9c1 src/Pure/Tools/build_job.scala --- 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) diff -r 5f6f567a2661 -r f376aebca9c1 src/Pure/Tools/build_process.scala --- 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) diff -r 5f6f567a2661 -r f376aebca9c1 src/Pure/Tools/dump.scala --- 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" diff -r 5f6f567a2661 -r f376aebca9c1 src/Pure/Tools/update.scala --- 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,