# HG changeset patch # User Fabian Huch # Date 1710327246 -3600 # Node ID a3d53f2bc41d6a8d12ab6588fddb5e3aa392b592 # Parent c00181ecf8697c12d5b707d0b7ed0bcea8c51dab clarified build schedule host: proper module; diff -r c00181ecf869 -r a3d53f2bc41d src/Pure/Build/build_schedule.scala --- a/src/Pure/Build/build_schedule.scala Wed Mar 13 11:45:20 2024 +0100 +++ b/src/Pure/Build/build_schedule.scala Wed Mar 13 11:54:06 2024 +0100 @@ -47,8 +47,8 @@ (job_name, session_info) <- build_info.sessions.toList if build_info.finished_sessions.contains(job_name) hostname <- session_info.hostname.orElse(build_host).toList - host <- hosts.find(_.info.hostname == hostname).toList - threads = session_info.threads.getOrElse(host.info.num_cpus) + host <- hosts.find(_.name == hostname).toList + threads = session_info.threads.getOrElse(host.num_cpus) } yield (job_name, hostname, threads) -> session_info.timing val entries = @@ -332,19 +332,34 @@ /* host information */ - case class Host(info: isabelle.Host.Info, build: Build_Cluster.Host) { - def name: String = info.hostname - def num_cpus: Int = info.num_cpus - def max_threads(options: Options): Int = (options ++ build.options).threads(default = num_cpus) + case class Host( + name: String, + num_cpus: Int, + max_jobs: Int, + benchmark_score: Double, + numa: Boolean = false, + numa_nodes: List[Int] = Nil, + options: List[Options.Spec] = Nil + ) { + def max_threads(options: Options): Int = (options ++ this.options).threads(default = num_cpus) } object Host_Infos { def load(build_hosts: List[Build_Cluster.Host], db: SQL.Database): Host_Infos = { def get_host(build_host: Build_Cluster.Host): Host = { + val name = build_host.name val info = - isabelle.Host.read_info(db, build_host.name).getOrElse( - error("No benchmark for " + quote(build_host.name))) - Host(info, build_host) + isabelle.Host.read_info(db, name).getOrElse(error("No info for host " + quote(name))) + val score = info.benchmark_score.getOrElse(error("No benchmark for " + quote(name))) + + Host( + name = name, + num_cpus = info.num_cpus, + max_jobs = build_host.jobs, + numa = build_host.numa, + numa_nodes = info.numa_nodes, + benchmark_score = score, + options = build_host.options) } new Host_Infos(build_hosts.map(get_host)) @@ -357,7 +372,7 @@ private val by_hostname = hosts.map(host => host.name -> host).toMap def host_factor(from: Host, to: Host): Double = - from.info.benchmark_score.get / to.info.benchmark_score.get + from.benchmark_score / to.benchmark_score val host_speeds: Ordering[Host] = Ordering.fromLessThan((host1, host2) => host_factor(host1, host2) < 1) @@ -368,7 +383,7 @@ def num_threads(node_info: Node_Info): Int = if (node_info.rel_cpus.nonEmpty) node_info.rel_cpus.length - else the_host(node_info).info.num_cpus + else the_host(node_info).num_cpus def available(state: Build_Process.State): Resources = { val allocated = @@ -416,7 +431,7 @@ val (config, resources) = hosts.find((host, _) => available(host, min_threads)) match { case Some((host, host_max_threads)) => - val free_threads = host.info.num_cpus - ((host.build.jobs - 1) * host_max_threads) + val free_threads = host.num_cpus - ((host.max_jobs - 1) * host_max_threads) val node_info = next_node(host, (min_threads max free_threads) min max_threads) (Some(Config(task.name, node_info)), allocate(node_info)) case None => (None, this) @@ -426,15 +441,15 @@ } def next_node(host: Host, threads: Int): Node_Info = { - val numa_node_num_cpus = host.info.num_cpus / (host.info.numa_nodes.length max 1) + val numa_node_num_cpus = host.num_cpus / (host.numa_nodes.length max 1) def explicit_cpus(node_info: Node_Info): List[Int] = if (node_info.rel_cpus.nonEmpty) node_info.rel_cpus else (0 until numa_node_num_cpus).toList val used_nodes = allocated(host).groupMapReduce(_.numa_node)(explicit_cpus)(_ ::: _) - val available_nodes = host.info.numa_nodes + val available_nodes = host.numa_nodes val numa_node = - if (!host.build.numa) None + if (!host.numa) None else available_nodes.sortBy(n => used_nodes.getOrElse(Some(n), Nil).length).headOption val used_cpus = used_nodes.getOrElse(numa_node, Nil).toSet @@ -448,16 +463,16 @@ def available(host: Host, threads: Int): Boolean = { val used = allocated(host) - if (used.length >= host.build.jobs) false + if (used.length >= host.max_jobs) false else { - if (host.info.numa_nodes.length <= 1) - used.map(host_infos.num_threads).sum + threads <= host.info.num_cpus + if (host.numa_nodes.length <= 1) + used.map(host_infos.num_threads).sum + threads <= host.num_cpus else { def node_threads(n: Int): Int = used.filter(_.numa_node.contains(n)).map(host_infos.num_threads).sum - host.info.numa_nodes.exists( - node_threads(_) + threads <= host.info.num_cpus / host.info.numa_nodes.length) + host.numa_nodes.exists( + node_threads(_) + threads <= host.num_cpus / host.numa_nodes.length) } } } @@ -692,7 +707,7 @@ val host_infos: Host_Infos = timing_data.host_infos val ordered_hosts: List[Host] = host_infos.hosts.sorted(host_infos.host_speeds) - val max_threads: Int = host_infos.hosts.map(_.info.num_cpus).max min max_threads_limit + val max_threads: Int = host_infos.hosts.map(_.num_cpus).max min max_threads_limit type Node = String val build_graph: Graph[Node, Sessions.Info] = sessions_structure.build_graph @@ -709,7 +724,7 @@ def best_time(node: Node): Time = { val host = ordered_hosts.last - val threads = best_threads(node) min host.info.num_cpus + val threads = best_threads(node) min host.num_cpus timing_data.estimate(node, host.name, threads) } val best_times: Map[Node, Time] = build_graph.keys.map(node => node -> best_time(node)).toMap @@ -830,9 +845,9 @@ case Fixed_Fraction(fraction) => ((rev_ordered_hosts.length * fraction).ceil.toInt max 1) min max_critical_hosts case Host_Speed(min_factor) => - val best = rev_ordered_hosts.head._1.info.benchmark_score.get + val best = rev_ordered_hosts.head._1.benchmark_score val num_fast = - rev_ordered_hosts.count(_._1.info.benchmark_score.exists(_ >= best * min_factor)) + rev_ordered_hosts.count(_._1.benchmark_score >= best * min_factor) num_fast min max_critical_hosts }