src/Pure/Tools/build_schedule.scala
author Fabian Huch <huch@in.tum.de>
Thu, 09 Nov 2023 11:41:19 +0100
changeset 78929 df323f23dfde
parent 78928 6c2c60b852e0
child 78930 f72f576fea3e
permissions -rw-r--r--
performance tuning for timing heuristic: pre-calculate graph operations;
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
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   146
          hostname = session_info.hostname.getOrElse(build_host)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   147
          host <- hosts.find(_.info.hostname == build_host).toList
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   148
          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
   149
        } 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
   150
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   151
      val entries =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   152
        if (measurements.isEmpty) dummy_entries
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   153
        else
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   154
          measurements.groupMap(_._1)(_._2).toList.map {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   155
            case ((job_name, hostname, threads), timings) =>
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   156
              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
   157
          }
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
      new Timing_Data(entries, host_infos)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   160
    }
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
  /* host information */
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   165
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   166
  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
   167
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   168
  object Host_Infos {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   169
    def dummy: Host_Infos =
78846
966aa081929f tuned imports;
wenzelm
parents: 78845
diff changeset
   170
      new Host_Infos(
966aa081929f tuned imports;
wenzelm
parents: 78845
diff changeset
   171
        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
   172
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   173
    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
   174
      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
   175
        val info =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   176
          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
   177
            error("No benchmark for " + quote(build_host.name)))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   178
        Host(info, build_host)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   179
      }
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
      new Host_Infos(build_hosts.map(get_host))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   182
    }
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
  class Host_Infos private(val hosts: List[Host]) {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   186
    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
   187
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   188
    def host_factor(from: Host, to: Host): Double =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   189
      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
   190
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   191
    val host_speeds: Ordering[Host] =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   192
      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
   193
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   194
    def the_host(hostname: String): Host =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   195
      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
   196
    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
   197
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   198
    def num_threads(node_info: Node_Info): Int =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   199
      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
   200
      else the_host(node_info).info.num_cpus
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   201
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   202
    def available(state: Build_Process.State): Resources = {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   203
      val allocated =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   204
        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
   205
      Resources(this, allocated)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   206
    }
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
  /* offline tracking of resource allocations */
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   211
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   212
  case class Resources(
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   213
    host_infos: Host_Infos,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   214
    allocated_nodes: Map[Host, List[Node_Info]]
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   215
  ) {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   216
    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
   217
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   218
    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
   219
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   220
    def allocate(node: Node_Info): Resources = {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   221
      val host = host_infos.the_host(node)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   222
      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
   223
    }
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
    def try_allocate_tasks(
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   226
      hosts: List[Host],
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   227
      tasks: List[(Build_Process.Task, Int)]
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   228
    ): (List[Config], Resources) =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   229
      tasks match {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   230
        case Nil => (Nil, this)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   231
        case (task, threads) :: tasks =>
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   232
          val (config, resources) =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   233
            hosts.find(available(_, threads)) match {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   234
              case Some(host) =>
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   235
                val node_info = next_node(host, threads)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   236
                (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
   237
              case None => (None, this)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   238
            }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   239
          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
   240
          (configs ++ config, resources1)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   241
      }
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
    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
   244
      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
   245
      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
   246
        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
   247
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   248
      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
   249
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   250
      val available_nodes = host.info.numa_nodes
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   251
      val numa_node =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   252
        if (!host.build.numa) None
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   253
        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
   254
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   255
      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
   256
      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
   257
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   258
      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
   259
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   260
      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
   261
    }
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
    def available(host: Host, threads: Int): Boolean = {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   264
      val used = allocated(host)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   265
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   266
      if (used.length >= host.build.jobs) false
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   267
      else {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   268
        if (host.info.numa_nodes.length <= 1)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   269
          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
   270
        else {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   271
          def node_threads(n: Int): Int =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   272
            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
   273
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   274
          host.info.numa_nodes.exists(
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   275
            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
   276
        }
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
  /* schedule generation */
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   283
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   284
  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
   285
    def start(config: Config): State =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   286
      copy(build_state =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   287
        build_state.copy(running = build_state.running +
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   288
          (config.job_name -> config.job_of(current_time))))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   289
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   290
    def step(timing_data: Timing_Data): State = {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   291
      val remaining =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   292
        build_state.running.values.toList.map { job =>
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   293
          val elapsed = current_time - job.start_date.time
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   294
          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
   295
          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
   296
          job -> remaining
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   297
        }
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
      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
   300
      else {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   301
        val (job, elapsed) = remaining.minBy(_._2.ms)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   302
        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
   303
      }
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
    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
   307
  }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   308
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
   309
  abstract class Scheduler(timing_data: Timing_Data) {
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   310
    def ready_jobs(state: Build_Process.State): Build_Process.State.Pending =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   311
      state.pending.filter(entry => entry.is_ready && !state.is_running(entry.name))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   312
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
   313
    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
   314
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
   315
    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
   316
      @tailrec
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   317
      def simulate(state: State): State =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   318
        if (state.finished) state
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   319
        else {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   320
          val state1 =
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
   321
            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
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   330
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   331
  /* heuristics */
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   332
78929
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   333
  class Timing_Heuristic(
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   334
    threshold: Time,
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   335
    timing_data: Timing_Data,
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   336
    sessions_structure: Sessions.Structure
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   337
  ) extends Scheduler(timing_data) {
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   338
    /* 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
   339
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   340
    type Node = String
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   341
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   342
    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
   343
    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
   344
    val maximals_preds =
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   345
      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
   346
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   347
    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
   348
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   349
    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
   350
      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
   351
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   352
    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
   353
      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
   354
      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
   355
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   356
      maximals
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   357
        .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
   358
        .groupMapReduce(_._1)(_._2)(_ max _)
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
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   361
    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
   362
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   363
    val critical_path_nodes =
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   364
      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
   365
        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
   366
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   367
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   368
    /* scheduling */
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   369
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   370
    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
   371
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
   372
    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
   373
      val resources = host_infos.available(state)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   374
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   375
      def best_threads(task: Build_Process.Task): Int =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   376
        timing_data.best_threads(task.name).getOrElse(
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   377
          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
   378
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   379
      val ready = ready_jobs(state)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   380
      val free = resources.unused_hosts
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   381
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   382
      if (ready.length <= free.length)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   383
        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
   384
      else {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   385
        val pending_tasks = state.pending.map(_.name).toSet
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   386
78929
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   387
        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
   388
        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
   389
78929
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   390
        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
   391
          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
   392
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   393
        val (critical, other) =
78929
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   394
          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
   395
            is_critical(task.name))
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   396
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   397
        val (critical_hosts, other_hosts) =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   398
          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
   399
            critical.map(_.name).map(parallel_paths).sum)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   400
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   401
        val (configs1, resources1) =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   402
          resources.try_allocate_tasks(critical_hosts,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   403
            critical.map(task => task -> best_threads(task)))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   404
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   405
        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
   406
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   407
        configs1 ::: configs2
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   408
      }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   409
    }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   410
  }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   411
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
   412
  class Meta_Heuristic(schedulers: List[Scheduler], timing_data: Timing_Data)
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
   413
    extends Scheduler(timing_data) {
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   414
    require(schedulers.nonEmpty)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   415
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
   416
    def next(state: Build_Process.State): List[Config] = {
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
   417
      val (best, _) = schedulers.map(h => h -> h.build_duration(state)).minBy(_._2.ms)
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
   418
      best.next(state)
78845
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
  /* process for scheduled build */
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   424
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
   425
  abstract class Scheduled_Build_Process(
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   426
    build_context: Build.Context,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   427
    build_progress: Progress,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   428
    server: SSH.Server,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   429
  ) extends Build_Process(build_context, build_progress, server) {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   430
    protected val start_date = Date.now()
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   431
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
   432
    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
   433
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   434
    /* global resources with common close() operation */
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   435
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   436
    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
   437
    private final lazy val _log_database: SQL.Database =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   438
      try {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   439
        val db = _log_store.open_database(server = this.server)
78851
db37cae970a6 more robust init_database();
wenzelm
parents: 78849
diff changeset
   440
        _log_store.init_database(db)
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   441
        db
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   442
      }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   443
      catch { case exn: Throwable => close(); throw exn }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   444
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   445
    override def close(): Unit = {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   446
      super.close()
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   447
      Option(_log_database).foreach(_.close())
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   448
    }
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
    /* previous results via build log */
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   452
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   453
    override def open_build_cluster(): Build_Cluster = {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   454
      val build_cluster = super.open_build_cluster()
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   455
      build_cluster.init()
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   456
      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
   457
        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
   458
        Benchmark.benchmark(benchmark_options, progress)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   459
      }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   460
      build_cluster.benchmark()
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   461
      build_cluster
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   462
    }
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
    private val timing_data: Timing_Data = {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   465
      val cluster_hosts: List[Build_Cluster.Host] =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   466
        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
   467
        else {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   468
          val local_build_host =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   469
            Build_Cluster.Host(
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   470
              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
   471
          local_build_host :: build_context.build_hosts
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   472
        }
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
      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
   475
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   476
      val build_history =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   477
        for {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   478
          log_name <- _log_database.execute_query_statement(
78849
df162316b6a7 clarified names;
wenzelm
parents: 78846
diff changeset
   479
            Build_Log.private_data.meta_info_table.select(List(Build_Log.private_data.log_name)),
df162316b6a7 clarified names;
wenzelm
parents: 78846
diff changeset
   480
            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
   481
          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
   482
          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
   483
        } yield (meta_info, build_info)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   484
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   485
      Timing_Data.make(host_infos, build_history)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   486
    }
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
   487
    private val scheduler = init_scheduler(timing_data)
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   488
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   489
    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
   490
      val sessions =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   491
        for {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   492
          (session_name, result) <- state.toList
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   493
          if !result.current
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   494
        } yield {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   495
          val info = build_context.sessions_structure(session_name)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   496
          val entry =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   497
            if (!results.cancelled(session_name)) {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   498
              val status =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   499
                if (result.ok) Build_Log.Session_Status.finished
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   500
                else Build_Log.Session_Status.failed
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   501
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   502
              Build_Log.Session_Entry(
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   503
                chapter = info.chapter,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   504
                groups = info.groups,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   505
                hostname = Some(result.node_info.hostname),
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   506
                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
   507
                timing = result.process_result.timing,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   508
                sources = Some(result.output_shasum.digest.toString),
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   509
                status = Some(status))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   510
            }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   511
            else
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   512
              Build_Log.Session_Entry(
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   513
                chapter = info.chapter,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   514
                groups = info.groups,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   515
                status = Some(Build_Log.Session_Status.cancelled))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   516
          session_name -> entry
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   517
        }
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
      val settings =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   520
        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
   521
          name -> Isabelle_System.getenv(name))
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   522
      val props =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   523
        List(
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   524
          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
   525
          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
   526
          Build_Log.Prop.build_host.name -> hostname,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   527
          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
   528
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   529
      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
   530
      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
   531
      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
   532
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   533
      _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
   534
      _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
   535
    }
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
    /* build process */
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   539
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   540
    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
   541
      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
   542
      def is_current_estimate(estimate: Date): Boolean =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   543
        this.estimate.time - estimate.time >= Time.seconds(1)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   544
    }
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
    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
   547
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   548
    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
   549
      val configs =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   550
        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
   551
        else scheduler.next(state)
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   552
      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
   553
    }
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
    override def next_jobs(state: Build_Process.State): List[String] =
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   556
      if (cache.is_current(state)) cache.configs.map(_.job_name)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   557
      else {
78884
0233d5a5a4ca improved build messages;
Fabian Huch <huch@in.tum.de>
parents: 78851
diff changeset
   558
        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
   559
        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
   560
        val estimate = Date(Time.now() + scheduler.build_duration(state))
78884
0233d5a5a4ca improved build messages;
Fabian Huch <huch@in.tum.de>
parents: 78851
diff changeset
   561
        val elapsed = Time.now() - start
0233d5a5a4ca improved build messages;
Fabian Huch <huch@in.tum.de>
parents: 78851
diff changeset
   562
0233d5a5a4ca improved build messages;
Fabian Huch <huch@in.tum.de>
parents: 78851
diff changeset
   563
        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
   564
        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
   565
          "Estimated completion: " + estimate + timing_msg)
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   566
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   567
        val configs = next.filter(_.node_info.hostname == hostname)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   568
        cache = Cache(state, configs, estimate)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   569
        configs.map(_.job_name)
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   570
      }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   571
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   572
    override def run(): Build.Results = {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   573
      val results = super.run()
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   574
      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
   575
      results
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   576
    }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   577
  }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   578
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   579
  class Engine extends Build.Engine(engine_name) {
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   580
    override def open_build_process(
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   581
      context: Build.Context,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   582
      progress: Progress,
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   583
      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
   584
    ): 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
   585
      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
   586
        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
   587
          val heuristics =
78929
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   588
            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
   589
              Timing_Heuristic(
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   590
                Time.minutes(minutes),
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   591
                timing_data,
df323f23dfde performance tuning for timing heuristic: pre-calculate graph operations;
Fabian Huch <huch@in.tum.de>
parents: 78928
diff changeset
   592
                context.build_deps.sessions_structure))
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
   593
          new Meta_Heuristic(heuristics, timing_data)
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
   594
        }
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
   595
      }
78845
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   596
  }
ff96d94957cb add module for faster scheduled builds;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   597
}