src/Pure/Tools/build_schedule.scala
author Fabian Huch <huch@in.tum.de>
Thu, 09 Nov 2023 17:58:21 +0100
changeset 78933 4f940d7293ea
parent 78932 ae1403e341dd
child 78934 5553a86a1091
permissions -rw-r--r--
use only finished sessions in timing data;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
     1
/*  Title:      Pure/Tools/build_schedule.scala
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
     2
    Author:     Fabian Huch, TU Muenchen
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
     3
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
     4
Build schedule generated by Heuristic methods, allowing for more efficient builds.
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
     5
 */
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
     6
package isabelle
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
     7
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
     8
78846
966aa081929f tuned imports;
wenzelm
parents: 78845
diff changeset
     9
import Host.Node_Info
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    10
import scala.annotation.tailrec
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    11
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    12
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    13
object Build_Schedule {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    14
  val engine_name = "build_schedule"
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    15
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    16
  object Config {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    17
    def from_job(job: Build_Process.Job): Config = Config(job.name, job.node_info)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    18
  }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    19
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    20
  case class Config(job_name: String, node_info: Node_Info) {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    21
    def job_of(start_time: Time): Build_Process.Job =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    22
      Build_Process.Job(job_name, "", "", node_info, Date(start_time), None)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    23
  }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    24
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    25
  /* organized historic timing information (extracted from build logs) */
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    26
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    27
  case class Timing_Entry(job_name: String, hostname: String, threads: Int, elapsed: Time)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    28
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    29
  class Timing_Data private(data: List[Timing_Entry], val host_infos: Host_Infos) {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    30
    require(data.nonEmpty)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    31
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    32
    def is_empty = data.isEmpty
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    33
    def size = data.length
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    34
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    35
    private lazy val by_job =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    36
      data.groupBy(_.job_name).view.mapValues(new Timing_Data(_, host_infos)).toMap
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    37
    private lazy val by_threads =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    38
      data.groupBy(_.threads).view.mapValues(new Timing_Data(_, host_infos)).toMap
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    39
    private lazy val by_hostname =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    40
      data.groupBy(_.hostname).view.mapValues(new Timing_Data(_, host_infos)).toMap
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    41
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    42
    def mean_time: Time = Timing_Data.mean_time(data.map(_.elapsed))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    43
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    44
    private def best_entry: Timing_Entry = data.minBy(_.elapsed.ms)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    45
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    46
    def best_threads(job_name: String): Option[Int] = by_job.get(job_name).map(_.best_entry.threads)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    47
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    48
    def best_time(job_name: String): Time =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    49
      by_job.get(job_name).map(_.best_entry.elapsed).getOrElse(
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    50
        estimate_config(Config(job_name, Node_Info(best_entry.hostname, None, Nil))))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    51
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    52
    private def hostname_factor(from: String, to: String): Double =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    53
      host_infos.host_factor(host_infos.the_host(from), host_infos.the_host(to))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    54
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    55
    def approximate_threads(threads: Int): Option[Time] = {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    56
      val approximations =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    57
        by_job.values.filter(_.size > 1).map { data =>
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    58
          val (ref_hostname, x0) =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    59
            data.by_hostname.toList.flatMap((hostname, data) =>
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    60
              data.by_threads.keys.map(hostname -> _)).minBy((_, n) => Math.abs(n - threads))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    61
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    62
          def unify_hosts(data: Timing_Data): List[Time] =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    63
            data.by_hostname.toList.map((hostname, data) =>
78888
95bbf9a576b3 prefer Time.scale(), following Isabelle/ML;
wenzelm
parents: 78884
diff changeset
    64
              data.mean_time.scale(hostname_factor(hostname, ref_hostname)))
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    65
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    66
          val entries =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    67
            data.by_threads.toList.map((threads, data) =>
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    68
              threads -> Timing_Data.median_time(unify_hosts(data)))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    69
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    70
          val y0 = data.by_hostname(ref_hostname).by_threads(x0).mean_time
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    71
          val (x1, y1_data) =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    72
            data.by_hostname(ref_hostname).by_threads.toList.minBy((n, _) => Math.abs(n - threads))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    73
          val y1 = y1_data.mean_time
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    74
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    75
          val a = (y1.ms - y0.ms).toDouble / (x1 - x0)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    76
          val b = y0.ms - a * x0
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    77
          Time.ms((a * threads + b).toLong)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    78
        }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    79
      if (approximations.isEmpty) None else Some(Timing_Data.mean_time(approximations))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    80
    }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    81
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    82
    def threads_factor(divided: Int, divisor: Int): Double =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    83
      (approximate_threads(divided), approximate_threads(divisor)) match {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    84
        case (Some(dividend), Some(divisor)) => dividend.ms.toDouble / divisor.ms
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    85
        case _ => divided.toDouble / divisor
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    86
      }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    87
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    88
    def estimate_config(config: Config): Time =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    89
      by_job.get(config.job_name) match {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    90
        case None => mean_time
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    91
        case Some(data) =>
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    92
          val hostname = config.node_info.hostname
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    93
          val threads = host_infos.num_threads(config.node_info)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    94
          data.by_threads.get(threads) match {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    95
            case None => // interpolate threads
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    96
              data.by_hostname.get(hostname).flatMap(
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    97
                _.approximate_threads(threads)).getOrElse {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    98
                  // per machine, try to approximate config for threads
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    99
                  val approximated =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   100
                    data.by_hostname.toList.flatMap((hostname1, data) =>
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   101
                      data.approximate_threads(threads).map(time =>
78888
95bbf9a576b3 prefer Time.scale(), following Isabelle/ML;
wenzelm
parents: 78884
diff changeset
   102
                        time.scale(hostname_factor(hostname1, hostname))))
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   103
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   104
                  if (approximated.nonEmpty) Timing_Data.mean_time(approximated)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   105
                  else {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   106
                    // no machine where config can be approximated
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   107
                    data.approximate_threads(threads).getOrElse {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   108
                      // only single data point, use global curve to approximate
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   109
                      val global_factor = threads_factor(data.by_threads.keys.head, threads)
78888
95bbf9a576b3 prefer Time.scale(), following Isabelle/ML;
wenzelm
parents: 78884
diff changeset
   110
                      data.by_threads.values.head.mean_time.scale(global_factor)
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   111
                    }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   112
                  }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   113
                }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   114
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   115
            case Some(data) => // time for job/thread exists, interpolate machine
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   116
              data.by_hostname.get(hostname).map(_.mean_time).getOrElse {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   117
                Timing_Data.median_time(
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   118
                  data.by_hostname.toList.map((hostname1, data) =>
78888
95bbf9a576b3 prefer Time.scale(), following Isabelle/ML;
wenzelm
parents: 78884
diff changeset
   119
                    data.mean_time.scale(hostname_factor(hostname1, hostname))))
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   120
              }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   121
          }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   122
      }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   123
  }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   124
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   125
  object Timing_Data {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   126
    def median_time(obs: List[Time]): Time = obs.sortBy(_.ms).drop(obs.length / 2).head
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   127
    def mean_time(obs: Iterable[Time]): Time = Time.ms(obs.map(_.ms).sum / obs.size)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   128
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   129
    private val dummy_entries =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   130
      List(
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   131
        Timing_Entry("dummy", "dummy", 1, Time.minutes(5)),
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   132
        Timing_Entry("dummy", "dummy", 8, Time.minutes(1)))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   133
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   134
    def dummy: Timing_Data = new Timing_Data(dummy_entries, Host_Infos.dummy)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   135
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   136
    def make(
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   137
      host_infos: Host_Infos,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   138
      build_history: List[(Build_Log.Meta_Info, Build_Log.Build_Info)],
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   139
    ): Timing_Data = {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   140
      val hosts = host_infos.hosts
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   141
      val measurements =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   142
        for {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   143
          (meta_info, build_info) <- build_history
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   144
          build_host <- meta_info.get(Build_Log.Prop.build_host).toList
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   145
          (job_name, session_info) <- build_info.sessions.toList
78933
4f940d7293ea use only finished sessions in timing data;
Fabian Huch <huch@in.tum.de>
parents: 78932
diff changeset
   146
          if build_info.finished_sessions.contains(job_name)
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   147
          hostname = session_info.hostname.getOrElse(build_host)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   148
          host <- hosts.find(_.info.hostname == build_host).toList
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   149
          threads = session_info.threads.getOrElse(host.info.num_cpus)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   150
        } yield (job_name, hostname, threads) -> session_info.timing.elapsed
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   151
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   152
      val entries =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   153
        if (measurements.isEmpty) dummy_entries
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   154
        else
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   155
          measurements.groupMap(_._1)(_._2).toList.map {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   156
            case ((job_name, hostname, threads), timings) =>
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   157
              Timing_Entry(job_name, hostname, threads, median_time(timings))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   158
          }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   159
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   160
      new Timing_Data(entries, host_infos)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   161
    }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   162
  }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   163
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   164
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   165
  /* host information */
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   166
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   167
  case class Host(info: isabelle.Host.Info, build: Build_Cluster.Host)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   168
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   169
  object Host_Infos {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   170
    def dummy: Host_Infos =
78846
966aa081929f tuned imports;
wenzelm
parents: 78845
diff changeset
   171
      new Host_Infos(
966aa081929f tuned imports;
wenzelm
parents: 78845
diff changeset
   172
        List(Host(isabelle.Host.Info("dummy", Nil, 8, Some(1.0)), Build_Cluster.Host("dummy"))))
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   173
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   174
    def apply(build_hosts: List[Build_Cluster.Host], db: SQL.Database): Host_Infos = {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   175
      def get_host(build_host: Build_Cluster.Host): Host = {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   176
        val info =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   177
          isabelle.Host.read_info(db, build_host.name).getOrElse(
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   178
            error("No benchmark for " + quote(build_host.name)))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   179
        Host(info, build_host)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   180
      }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   181
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   182
      new Host_Infos(build_hosts.map(get_host))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   183
    }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   184
  }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   185
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   186
  class Host_Infos private(val hosts: List[Host]) {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   187
    private val by_hostname = hosts.map(host => host.info.hostname -> host).toMap
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   188
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   189
    def host_factor(from: Host, to: Host): Double =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   190
      from.info.benchmark_score.get / to.info.benchmark_score.get
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   191
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   192
    val host_speeds: Ordering[Host] =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   193
      Ordering.fromLessThan((host1, host2) => host_factor(host1, host2) > 1)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   194
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   195
    def the_host(hostname: String): Host =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   196
      by_hostname.getOrElse(hostname, error("Unknown host " + quote(hostname)))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   197
    def the_host(node_info: Node_Info): Host = the_host(node_info.hostname)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   198
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   199
    def num_threads(node_info: Node_Info): Int =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   200
      if (node_info.rel_cpus.nonEmpty) node_info.rel_cpus.length
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   201
      else the_host(node_info).info.num_cpus
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   202
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   203
    def available(state: Build_Process.State): Resources = {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   204
      val allocated =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   205
        state.running.values.map(_.node_info).groupMapReduce(the_host)(List(_))(_ ::: _)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   206
      Resources(this, allocated)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   207
    }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   208
  }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   209
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   210
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   211
  /* offline tracking of resource allocations */
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   212
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   213
  case class Resources(
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   214
    host_infos: Host_Infos,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   215
    allocated_nodes: Map[Host, List[Node_Info]]
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   216
  ) {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   217
    val unused_hosts: List[Host] = host_infos.hosts.filter(allocated(_).isEmpty)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   218
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   219
    def allocated(host: Host): List[Node_Info] = allocated_nodes.getOrElse(host, Nil)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   220
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   221
    def allocate(node: Node_Info): Resources = {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   222
      val host = host_infos.the_host(node)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   223
      copy(allocated_nodes = allocated_nodes + (host -> (node :: allocated(host))))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   224
    }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   225
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   226
    def try_allocate_tasks(
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   227
      hosts: List[Host],
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   228
      tasks: List[(Build_Process.Task, Int)]
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   229
    ): (List[Config], Resources) =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   230
      tasks match {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   231
        case Nil => (Nil, this)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   232
        case (task, threads) :: tasks =>
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   233
          val (config, resources) =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   234
            hosts.find(available(_, threads)) match {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   235
              case Some(host) =>
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   236
                val node_info = next_node(host, threads)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   237
                (Some(Config(task.name, node_info)), allocate(node_info))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   238
              case None => (None, this)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   239
            }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   240
          val (configs, resources1) = resources.try_allocate_tasks(hosts, tasks)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   241
          (configs ++ config, resources1)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   242
      }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   243
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   244
    def next_node(host: Host, threads: Int): Node_Info = {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   245
      val numa_node_num_cpus = host.info.num_cpus / (host.info.numa_nodes.length max 1)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   246
      def explicit_cpus(node_info: Node_Info): List[Int] =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   247
        if (node_info.rel_cpus.nonEmpty) node_info.rel_cpus else (0 until numa_node_num_cpus).toList
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   248
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   249
      val used_nodes = allocated(host).groupMapReduce(_.numa_node)(explicit_cpus)(_ ::: _)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   250
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   251
      val available_nodes = host.info.numa_nodes
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   252
      val numa_node =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   253
        if (!host.build.numa) None
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   254
        else available_nodes.sortBy(n => used_nodes.getOrElse(Some(n), Nil).length).headOption
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   255
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   256
      val used_cpus = used_nodes.getOrElse(numa_node, Nil).toSet
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   257
      val available_cpus = (0 until numa_node_num_cpus).filterNot(used_cpus.contains).toList
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   258
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   259
      val rel_cpus = if (available_cpus.length >= threads) available_cpus.take(threads) else Nil
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   260
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   261
      Node_Info(host.info.hostname, numa_node, rel_cpus)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   262
    }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   263
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   264
    def available(host: Host, threads: Int): Boolean = {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   265
      val used = allocated(host)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   266
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   267
      if (used.length >= host.build.jobs) false
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   268
      else {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   269
        if (host.info.numa_nodes.length <= 1)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   270
          used.map(host_infos.num_threads).sum + threads <= host.info.num_cpus
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   271
        else {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   272
          def node_threads(n: Int): Int =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   273
            used.filter(_.numa_node.contains(n)).map(host_infos.num_threads).sum
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   274
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   275
          host.info.numa_nodes.exists(
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   276
            node_threads(_) + threads <= host.info.num_cpus / host.info.numa_nodes.length)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   277
        }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   278
      }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   279
    }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   280
  }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   281
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   282
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   283
  /* schedule generation */
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   284
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   285
  case class State(build_state: Build_Process.State, current_time: Time) {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   286
    def start(config: Config): State =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   287
      copy(build_state =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   288
        build_state.copy(running = build_state.running +
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   289
          (config.job_name -> config.job_of(current_time))))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   290
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   291
    def step(timing_data: Timing_Data): State = {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   292
      val remaining =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   293
        build_state.running.values.toList.map { job =>
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   294
          val elapsed = current_time - job.start_date.time
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   295
          val predicted = timing_data.estimate_config(Config.from_job(job))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   296
          val remaining = if (elapsed > predicted) Time.zero else predicted - elapsed
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   297
          job -> remaining
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   298
        }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   299
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   300
      if (remaining.isEmpty) error("Schedule step without running sessions")
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   301
      else {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   302
        val (job, elapsed) = remaining.minBy(_._2.ms)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   303
        State(build_state.remove_running(job.name).remove_pending(job.name), current_time + elapsed)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   304
      }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   305
    }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   306
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   307
    def finished: Boolean = build_state.pending.isEmpty && build_state.running.isEmpty
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   308
  }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   309
78932
Fabian Huch <huch@in.tum.de>
parents: 78931
diff changeset
   310
  trait Scheduler {
78928
6c2c60b852e0 move timing data into scheduler for more efficient heuristics (e.g., with pre-calculated values);
Fabian Huch <huch@in.tum.de>
parents: 78888
diff changeset
   311
    def next(state: Build_Process.State): List[Config]
78931
26841d3c568c performance tuning for build schedule: explicit schedule generation, without mixing heuristics;
Fabian Huch <huch@in.tum.de>
parents: 78930
diff changeset
   312
    def build_duration(build_state: Build_Process.State): Time
26841d3c568c performance tuning for build schedule: explicit schedule generation, without mixing heuristics;
Fabian Huch <huch@in.tum.de>
parents: 78930
diff changeset
   313
  }
26841d3c568c performance tuning for build schedule: explicit schedule generation, without mixing heuristics;
Fabian Huch <huch@in.tum.de>
parents: 78930
diff changeset
   314
26841d3c568c performance tuning for build schedule: explicit schedule generation, without mixing heuristics;
Fabian Huch <huch@in.tum.de>
parents: 78930
diff changeset
   315
  abstract class Heuristic(timing_data: Timing_Data) extends Scheduler {
78928
6c2c60b852e0 move timing data into scheduler for more efficient heuristics (e.g., with pre-calculated values);
Fabian Huch <huch@in.tum.de>
parents: 78888
diff changeset
   316
    def build_duration(build_state: Build_Process.State): Time = {
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   317
      @tailrec
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   318
      def simulate(state: State): State =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   319
        if (state.finished) state
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   320
        else {
78932
Fabian Huch <huch@in.tum.de>
parents: 78931
diff changeset
   321
          val state1 = next(state.build_state).foldLeft(state)(_.start(_)).step(timing_data)
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   322
          simulate(state1)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   323
        }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   324
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   325
      val start = Time.now()
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   326
      simulate(State(build_state, start)).current_time - start
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   327
    }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   328
  }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   329
78931
26841d3c568c performance tuning for build schedule: explicit schedule generation, without mixing heuristics;
Fabian Huch <huch@in.tum.de>
parents: 78930
diff changeset
   330
  class Meta_Heuristic(heuristics: List[Heuristic]) extends Scheduler {
26841d3c568c performance tuning for build schedule: explicit schedule generation, without mixing heuristics;
Fabian Huch <huch@in.tum.de>
parents: 78930
diff changeset
   331
    require(heuristics.nonEmpty)
26841d3c568c performance tuning for build schedule: explicit schedule generation, without mixing heuristics;
Fabian Huch <huch@in.tum.de>
parents: 78930
diff changeset
   332
26841d3c568c performance tuning for build schedule: explicit schedule generation, without mixing heuristics;
Fabian Huch <huch@in.tum.de>
parents: 78930
diff changeset
   333
    def best_result(state: Build_Process.State): (Heuristic, Time) =
26841d3c568c performance tuning for build schedule: explicit schedule generation, without mixing heuristics;
Fabian Huch <huch@in.tum.de>
parents: 78930
diff changeset
   334
      heuristics.map(heuristic => heuristic -> heuristic.build_duration(state)).minBy(_._2.ms)
26841d3c568c performance tuning for build schedule: explicit schedule generation, without mixing heuristics;
Fabian Huch <huch@in.tum.de>
parents: 78930
diff changeset
   335
26841d3c568c performance tuning for build schedule: explicit schedule generation, without mixing heuristics;
Fabian Huch <huch@in.tum.de>
parents: 78930
diff changeset
   336
    def next(state: Build_Process.State): List[Config] = best_result(state)._1.next(state)
26841d3c568c performance tuning for build schedule: explicit schedule generation, without mixing heuristics;
Fabian Huch <huch@in.tum.de>
parents: 78930
diff changeset
   337
26841d3c568c performance tuning for build schedule: explicit schedule generation, without mixing heuristics;
Fabian Huch <huch@in.tum.de>
parents: 78930
diff changeset
   338
    def build_duration(state: Build_Process.State): Time = best_result(state)._2
26841d3c568c performance tuning for build schedule: explicit schedule generation, without mixing heuristics;
Fabian Huch <huch@in.tum.de>
parents: 78930
diff changeset
   339
  }
26841d3c568c performance tuning for build schedule: explicit schedule generation, without mixing heuristics;
Fabian Huch <huch@in.tum.de>
parents: 78930
diff changeset
   340
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   341
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   342
  /* heuristics */
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   343
78929
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   344
  class Timing_Heuristic(
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   345
    threshold: Time,
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   346
    timing_data: Timing_Data,
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   347
    sessions_structure: Sessions.Structure
78931
26841d3c568c performance tuning for build schedule: explicit schedule generation, without mixing heuristics;
Fabian Huch <huch@in.tum.de>
parents: 78930
diff changeset
   348
  ) extends Heuristic(timing_data) {
78929
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   349
    /* pre-computed properties for efficient heuristic */
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   350
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   351
    type Node = String
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   352
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   353
    val build_graph = sessions_structure.build_graph
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   354
    val all_maximals = build_graph.maximals.toSet
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   355
    val maximals_preds =
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   356
      all_maximals.map(node => node -> build_graph.all_preds(List(node)).toSet).toMap
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   357
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   358
    val remaining_time = build_graph.node_height(timing_data.best_time(_).ms)
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   359
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   360
    def elapsed_times(node: Node): Map[Node, Long] =
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   361
      build_graph.reachable_length(timing_data.best_time(_).ms, build_graph.imm_succs, List(node))
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   362
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   363
    def path_times(node: Node): Map[Node, Long] = {
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   364
      val maximals = all_maximals.intersect(build_graph.all_succs(List(node)).toSet)
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   365
      val elapsed_time = elapsed_times(node)
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   366
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   367
      maximals
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   368
        .flatMap(node => maximals_preds(node).map(_ -> elapsed_time(node)))
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   369
        .groupMapReduce(_._1)(_._2)(_ max _)
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   370
    }
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   371
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   372
    def is_critical(ms: Long): Boolean = ms > threshold.ms
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   373
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   374
    val critical_path_nodes =
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   375
      build_graph.keys.map(node =>
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   376
        node -> path_times(node).filter((_, time) => is_critical(time)).keySet).toMap
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   377
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   378
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   379
    /* scheduling */
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   380
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   381
    val host_infos = timing_data.host_infos
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   382
78928
6c2c60b852e0 move timing data into scheduler for more efficient heuristics (e.g., with pre-calculated values);
Fabian Huch <huch@in.tum.de>
parents: 78888
diff changeset
   383
    def next(state: Build_Process.State): List[Config] = {
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   384
      val resources = host_infos.available(state)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   385
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   386
      def best_threads(task: Build_Process.Task): Int =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   387
        timing_data.best_threads(task.name).getOrElse(
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   388
          host_infos.hosts.map(_.info.num_cpus).max min 8)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   389
78932
Fabian Huch <huch@in.tum.de>
parents: 78931
diff changeset
   390
      val ready = state.pending.filter(entry => entry.is_ready && !state.is_running(entry.name))
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   391
      val free = resources.unused_hosts
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   392
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   393
      if (ready.length <= free.length)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   394
        resources.try_allocate_tasks(free, ready.map(task => task -> best_threads(task)))._1
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   395
      else {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   396
        val pending_tasks = state.pending.map(_.name).toSet
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   397
78929
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   398
        val critical_nodes = ready.toSet.flatMap(task => critical_path_nodes(task.name))
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   399
        def is_critical(node: Node): Boolean = critical_nodes.contains(node)
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   400
78929
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   401
        def parallel_paths(node: Node): Int =
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   402
          build_graph.imm_succs(node).filter(is_critical).map(parallel_paths(_) max 1).sum max 1
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   403
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   404
        val (critical, other) =
78929
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   405
          ready.sortBy(task => remaining_time(task.name)).reverse.partition(task =>
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   406
            is_critical(task.name))
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   407
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   408
        val (critical_hosts, other_hosts) =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   409
          host_infos.hosts.sorted(host_infos.host_speeds).reverse.splitAt(
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   410
            critical.map(_.name).map(parallel_paths).sum)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   411
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   412
        val (configs1, resources1) =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   413
          resources.try_allocate_tasks(critical_hosts,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   414
            critical.map(task => task -> best_threads(task)))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   415
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   416
        val (configs2, _) = resources1.try_allocate_tasks(other_hosts, other.map(_ -> 1))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   417
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   418
        configs1 ::: configs2
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   419
      }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   420
    }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   421
  }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   422
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   423
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   424
  /* process for scheduled build */
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   425
78928
6c2c60b852e0 move timing data into scheduler for more efficient heuristics (e.g., with pre-calculated values);
Fabian Huch <huch@in.tum.de>
parents: 78888
diff changeset
   426
  abstract class Scheduled_Build_Process(
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   427
    build_context: Build.Context,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   428
    build_progress: Progress,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   429
    server: SSH.Server,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   430
  ) extends Build_Process(build_context, build_progress, server) {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   431
    protected val start_date = Date.now()
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   432
78928
6c2c60b852e0 move timing data into scheduler for more efficient heuristics (e.g., with pre-calculated values);
Fabian Huch <huch@in.tum.de>
parents: 78888
diff changeset
   433
    def init_scheduler(timing_data: Timing_Data): Scheduler
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   434
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   435
    /* global resources with common close() operation */
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   436
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   437
    private final lazy val _log_store: Build_Log.Store = Build_Log.store(build_options)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   438
    private final lazy val _log_database: SQL.Database =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   439
      try {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   440
        val db = _log_store.open_database(server = this.server)
78851
db37cae970a6 more robust init_database();
wenzelm
parents: 78849
diff changeset
   441
        _log_store.init_database(db)
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   442
        db
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   443
      }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   444
      catch { case exn: Throwable => close(); throw exn }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   445
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   446
    override def close(): Unit = {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   447
      super.close()
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   448
      Option(_log_database).foreach(_.close())
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   449
    }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   450
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   451
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   452
    /* previous results via build log */
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   453
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   454
    override def open_build_cluster(): Build_Cluster = {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   455
      val build_cluster = super.open_build_cluster()
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   456
      build_cluster.init()
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   457
      if (build_context.master && build_context.max_jobs > 0) {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   458
        val benchmark_options = build_options.string("build_hostname") = hostname
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   459
        Benchmark.benchmark(benchmark_options, progress)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   460
      }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   461
      build_cluster.benchmark()
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   462
      build_cluster
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   463
    }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   464
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   465
    private val timing_data: Timing_Data = {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   466
      val cluster_hosts: List[Build_Cluster.Host] =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   467
        if (build_context.max_jobs == 0) build_context.build_hosts
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   468
        else {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   469
          val local_build_host =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   470
            Build_Cluster.Host(
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   471
              hostname, jobs = build_context.max_jobs, numa = build_context.numa_shuffling)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   472
          local_build_host :: build_context.build_hosts
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   473
        }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   474
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   475
      val host_infos = Host_Infos(cluster_hosts, _host_database)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   476
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   477
      val build_history =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   478
        for {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   479
          log_name <- _log_database.execute_query_statement(
78849
df162316b6a7 clarified names;
wenzelm
parents: 78846
diff changeset
   480
            Build_Log.private_data.meta_info_table.select(List(Build_Log.private_data.log_name)),
df162316b6a7 clarified names;
wenzelm
parents: 78846
diff changeset
   481
            List.from[String], res => res.string(Build_Log.private_data.log_name))
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   482
          meta_info <- _log_store.read_meta_info(_log_database, log_name)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   483
          build_info = _log_store.read_build_info(_log_database, log_name)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   484
        } yield (meta_info, build_info)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   485
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   486
      Timing_Data.make(host_infos, build_history)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   487
    }
78928
6c2c60b852e0 move timing data into scheduler for more efficient heuristics (e.g., with pre-calculated values);
Fabian Huch <huch@in.tum.de>
parents: 78888
diff changeset
   488
    private val scheduler = init_scheduler(timing_data)
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   489
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   490
    def write_build_log(results: Build.Results, state: Build_Process.State.Results): Unit = {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   491
      val sessions =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   492
        for {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   493
          (session_name, result) <- state.toList
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   494
          if !result.current
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   495
        } yield {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   496
          val info = build_context.sessions_structure(session_name)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   497
          val entry =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   498
            if (!results.cancelled(session_name)) {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   499
              val status =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   500
                if (result.ok) Build_Log.Session_Status.finished
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   501
                else Build_Log.Session_Status.failed
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   502
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   503
              Build_Log.Session_Entry(
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   504
                chapter = info.chapter,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   505
                groups = info.groups,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   506
                hostname = Some(result.node_info.hostname),
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   507
                threads = Some(timing_data.host_infos.num_threads(result.node_info)),
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   508
                timing = result.process_result.timing,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   509
                sources = Some(result.output_shasum.digest.toString),
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   510
                status = Some(status))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   511
            }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   512
            else
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   513
              Build_Log.Session_Entry(
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   514
                chapter = info.chapter,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   515
                groups = info.groups,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   516
                status = Some(Build_Log.Session_Status.cancelled))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   517
          session_name -> entry
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   518
        }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   519
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   520
      val settings =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   521
        Build_Log.Settings.all_settings.map(_.name).map(name =>
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   522
          name -> Isabelle_System.getenv(name))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   523
      val props =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   524
        List(
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   525
          Build_Log.Prop.build_id.name -> build_context.build_uuid,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   526
          Build_Log.Prop.build_engine.name -> build_context.engine.name,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   527
          Build_Log.Prop.build_host.name -> hostname,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   528
          Build_Log.Prop.build_start.name -> Build_Log.print_date(start_date))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   529
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   530
      val meta_info = Build_Log.Meta_Info(props, settings)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   531
      val build_info = Build_Log.Build_Info(sessions.toMap)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   532
      val log_name = Build_Log.log_filename(engine = engine_name, date = start_date)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   533
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   534
      _log_store.update_sessions(_log_database, log_name.file_name, build_info)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   535
      _log_store.update_meta_info(_log_database, log_name.file_name, meta_info)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   536
    }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   537
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   538
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   539
    /* build process */
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   540
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   541
    case class Cache(state: Build_Process.State, configs: List[Config], estimate: Date) {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   542
      def is_current(state: Build_Process.State): Boolean = this.state == state
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   543
      def is_current_estimate(estimate: Date): Boolean =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   544
        this.estimate.time - estimate.time >= Time.seconds(1)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   545
    }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   546
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   547
    private var cache = Cache(Build_Process.State(), Nil, Date.now())
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   548
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   549
    override def next_node_info(state: Build_Process.State, session_name: String): Node_Info = {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   550
      val configs =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   551
        if (cache.is_current(state)) cache.configs
78928
6c2c60b852e0 move timing data into scheduler for more efficient heuristics (e.g., with pre-calculated values);
Fabian Huch <huch@in.tum.de>
parents: 78888
diff changeset
   552
        else scheduler.next(state)
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   553
      configs.find(_.job_name == session_name).get.node_info
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   554
    }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   555
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   556
    override def next_jobs(state: Build_Process.State): List[String] =
78930
f72f576fea3e performance tuning for build schedule: faster stopping;
Fabian Huch <huch@in.tum.de>
parents: 78929
diff changeset
   557
      if (progress.stopped)
f72f576fea3e performance tuning for build schedule: faster stopping;
Fabian Huch <huch@in.tum.de>
parents: 78929
diff changeset
   558
        state.pending.filter(entry => entry.is_ready && !state.is_running(entry.name)).map(_.name)
f72f576fea3e performance tuning for build schedule: faster stopping;
Fabian Huch <huch@in.tum.de>
parents: 78929
diff changeset
   559
      else if (cache.is_current(state)) cache.configs.map(_.job_name)
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   560
      else {
78884
0233d5a5a4ca improved build messages;
Fabian Huch <huch@in.tum.de>
parents: 78851
diff changeset
   561
        val start = Time.now()
78928
6c2c60b852e0 move timing data into scheduler for more efficient heuristics (e.g., with pre-calculated values);
Fabian Huch <huch@in.tum.de>
parents: 78888
diff changeset
   562
        val next = scheduler.next(state)
6c2c60b852e0 move timing data into scheduler for more efficient heuristics (e.g., with pre-calculated values);
Fabian Huch <huch@in.tum.de>
parents: 78888
diff changeset
   563
        val estimate = Date(Time.now() + scheduler.build_duration(state))
78884
0233d5a5a4ca improved build messages;
Fabian Huch <huch@in.tum.de>
parents: 78851
diff changeset
   564
        val elapsed = Time.now() - start
0233d5a5a4ca improved build messages;
Fabian Huch <huch@in.tum.de>
parents: 78851
diff changeset
   565
0233d5a5a4ca improved build messages;
Fabian Huch <huch@in.tum.de>
parents: 78851
diff changeset
   566
        val timing_msg = if (elapsed.is_relevant) " (in " + elapsed.message + ")" else ""
0233d5a5a4ca improved build messages;
Fabian Huch <huch@in.tum.de>
parents: 78851
diff changeset
   567
        progress.echo_if(build_context.master && !cache.is_current_estimate(estimate),
0233d5a5a4ca improved build messages;
Fabian Huch <huch@in.tum.de>
parents: 78851
diff changeset
   568
          "Estimated completion: " + estimate + timing_msg)
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   569
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   570
        val configs = next.filter(_.node_info.hostname == hostname)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   571
        cache = Cache(state, configs, estimate)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   572
        configs.map(_.job_name)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   573
      }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   574
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   575
    override def run(): Build.Results = {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   576
      val results = super.run()
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   577
      if (build_context.master) write_build_log(results, snapshot().results)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   578
      results
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   579
    }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   580
  }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   581
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   582
  class Engine extends Build.Engine(engine_name) {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   583
    override def open_build_process(
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   584
      context: Build.Context,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   585
      progress: Progress,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   586
      server: SSH.Server
78928
6c2c60b852e0 move timing data into scheduler for more efficient heuristics (e.g., with pre-calculated values);
Fabian Huch <huch@in.tum.de>
parents: 78888
diff changeset
   587
    ): Build_Process =
6c2c60b852e0 move timing data into scheduler for more efficient heuristics (e.g., with pre-calculated values);
Fabian Huch <huch@in.tum.de>
parents: 78888
diff changeset
   588
      new Scheduled_Build_Process(context, progress, server) {
6c2c60b852e0 move timing data into scheduler for more efficient heuristics (e.g., with pre-calculated values);
Fabian Huch <huch@in.tum.de>
parents: 78888
diff changeset
   589
        def init_scheduler(timing_data: Timing_Data): Scheduler = {
6c2c60b852e0 move timing data into scheduler for more efficient heuristics (e.g., with pre-calculated values);
Fabian Huch <huch@in.tum.de>
parents: 78888
diff changeset
   590
          val heuristics =
78929
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   591
            List(5, 10, 20).map(minutes =>
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   592
              Timing_Heuristic(
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   593
                Time.minutes(minutes),
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   594
                timing_data,
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   595
                context.build_deps.sessions_structure))
78931
26841d3c568c performance tuning for build schedule: explicit schedule generation, without mixing heuristics;
Fabian Huch <huch@in.tum.de>
parents: 78930
diff changeset
   596
          new Meta_Heuristic(heuristics)
78928
6c2c60b852e0 move timing data into scheduler for more efficient heuristics (e.g., with pre-calculated values);
Fabian Huch <huch@in.tum.de>
parents: 78888
diff changeset
   597
        }
6c2c60b852e0 move timing data into scheduler for more efficient heuristics (e.g., with pre-calculated values);
Fabian Huch <huch@in.tum.de>
parents: 78888
diff changeset
   598
      }
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   599
  }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   600
}