# HG changeset patch # User Fabian Huch # Date 1701953868 -3600 # Node ID f52201fc15b400cf293aaa7d9b15a9934d8f5b9c # Parent b0491edc1a9f147f65184c62641c9b393d320ec6 tuned; diff -r b0491edc1a9f -r f52201fc15b4 src/Pure/Tools/build_schedule.scala --- a/src/Pure/Tools/build_schedule.scala Thu Dec 07 13:53:54 2023 +0100 +++ b/src/Pure/Tools/build_schedule.scala Thu Dec 07 13:57:48 2023 +0100 @@ -18,6 +18,7 @@ def elapsed: Time = timing.elapsed def proper_cpu: Option[Time] = timing.cpu.proper_ms.map(Time.ms) } + case class Timing_Entries(entries: List[Timing_Entry]) { require(entries.nonEmpty) @@ -32,6 +33,66 @@ def best_entry: Timing_Entry = entries.minBy(_.elapsed.ms) } + object Timing_Data { + def median_timing(obs: List[Timing]): Timing = obs.sortBy(_.elapsed.ms).apply(obs.length / 2) + + def median_time(obs: List[Time]): Time = obs.sortBy(_.ms).apply(obs.length / 2) + + def mean_time(obs: Iterable[Time]): Time = Time.ms(obs.map(_.ms).sum / obs.size) + + private def dummy_entries(host: Host, host_factor: Double) = { + val baseline = Time.minutes(5).scale(host_factor) + val gc = Time.seconds(10).scale(host_factor) + List( + Timing_Entry("dummy", host.name, 1, Timing(baseline, baseline, gc)), + Timing_Entry("dummy", host.name, 8, Timing(baseline.scale(0.2), baseline, gc))) + } + + def make( + host_infos: Host_Infos, + build_history: List[(Build_Log.Meta_Info, Build_Log.Build_Info)], + ): Timing_Data = { + val hosts = host_infos.hosts + val measurements = + for { + (meta_info, build_info) <- build_history + build_host = meta_info.get(Build_Log.Prop.build_host) + (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) + } yield (job_name, hostname, threads) -> session_info.timing + + val entries = + if (measurements.isEmpty) { + val default_host = host_infos.hosts.sorted(host_infos.host_speeds).last + host_infos.hosts.flatMap(host => + dummy_entries(host, host_infos.host_factor(default_host, host))) + } + else + measurements.groupMap(_._1)(_._2).toList.map { + case ((job_name, hostname, threads), timings) => + Timing_Entry(job_name, hostname, threads, median_timing(timings)) + } + + new Timing_Data(Timing_Entries(entries), host_infos) + } + + def load(host_infos: Host_Infos, log_database: SQL.Database): Timing_Data = { + val build_history = + for { + log_name <- log_database.execute_query_statement( + Build_Log.private_data.meta_info_table.select(List(Build_Log.Column.log_name)), + List.from[String], res => res.string(Build_Log.Column.log_name)) + meta_info <- Build_Log.private_data.read_meta_info(log_database, log_name) + build_info = Build_Log.private_data.read_build_info(log_database, log_name) + } yield (meta_info, build_info) + + make(host_infos, build_history) + } + } + class Timing_Data private(data: Timing_Entries, val host_infos: Host_Infos) { private def inflection_point(last_mono: Int, next: Int): Int = last_mono + ((next - last_mono) / 2) @@ -224,64 +285,6 @@ } } - object Timing_Data { - def median_timing(obs: List[Timing]): Timing = obs.sortBy(_.elapsed.ms).apply(obs.length / 2) - def median_time(obs: List[Time]): Time = obs.sortBy(_.ms).apply(obs.length / 2) - def mean_time(obs: Iterable[Time]): Time = Time.ms(obs.map(_.ms).sum / obs.size) - - private def dummy_entries(host: Host, host_factor: Double) = { - val baseline = Time.minutes(5).scale(host_factor) - val gc = Time.seconds(10).scale(host_factor) - List( - Timing_Entry("dummy", host.name, 1, Timing(baseline, baseline, gc)), - Timing_Entry("dummy", host.name, 8, Timing(baseline.scale(0.2), baseline, gc))) - } - - def make( - host_infos: Host_Infos, - build_history: List[(Build_Log.Meta_Info, Build_Log.Build_Info)], - ): Timing_Data = { - val hosts = host_infos.hosts - val measurements = - for { - (meta_info, build_info) <- build_history - build_host = meta_info.get(Build_Log.Prop.build_host) - (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) - } yield (job_name, hostname, threads) -> session_info.timing - - val entries = - if (measurements.isEmpty) { - val default_host = host_infos.hosts.sorted(host_infos.host_speeds).last - host_infos.hosts.flatMap(host => - dummy_entries(host, host_infos.host_factor(default_host, host))) - } - else - measurements.groupMap(_._1)(_._2).toList.map { - case ((job_name, hostname, threads), timings) => - Timing_Entry(job_name, hostname, threads, median_timing(timings)) - } - - new Timing_Data(Timing_Entries(entries), host_infos) - } - - def load(host_infos: Host_Infos, log_database: SQL.Database): Timing_Data = { - val build_history = - for { - log_name <- log_database.execute_query_statement( - Build_Log.private_data.meta_info_table.select(List(Build_Log.Column.log_name)), - List.from[String], res => res.string(Build_Log.Column.log_name)) - meta_info <- Build_Log.private_data.read_meta_info(log_database, log_name) - build_info = Build_Log.private_data.read_build_info(log_database, log_name) - } yield (meta_info, build_info) - - make(host_infos, build_history) - } - } - /* host information */