# HG changeset patch # User Fabian Huch # Date 1700735443 -3600 # Node ID abc27a824419fa18a7ea30e2d87757dd6032c115 # Parent e4fc535d4d2f87be72a322a86b9486468e27da0b better build time interpolation: model with Amdahl's law where applicable; diff -r e4fc535d4d2f -r abc27a824419 src/Pure/Tools/build_schedule.scala --- a/src/Pure/Tools/build_schedule.scala Wed Nov 22 18:10:21 2023 +0100 +++ b/src/Pure/Tools/build_schedule.scala Thu Nov 23 11:30:43 2023 +0100 @@ -67,18 +67,36 @@ data.by_threads.toList.map((threads, data) => threads -> Timing_Data.median_time(unify_hosts(data))).sortBy(_._1) - val ((threads0, time0), (threads1, time1)) = - if (entries.head._1 <= threads && threads <= entries.last._1) { - val split = entries.partition(_._1 <= threads) - (split._1.last, split._2.head) - } else { - val piece = if (threads < entries.head._1) entries.take(2) else entries.takeRight(2) - (piece.head, piece.last) - } + val monotone_prefix = + entries.zip(entries.sortBy(_._2.ms).reverse).takeWhile((e1, e2) => e1 == e2).map(_._1) + + if (monotone_prefix.length > 1 && threads <= monotone_prefix.last._1) { + // Model with Amdahl's law + val t_p = + Timing_Data.median_time(for { + (n, t0) <- monotone_prefix + (m, t1) <- monotone_prefix + if m != n + } yield (t0 - t1).scale(n.toDouble * m / (m - n))) + val t_c = + Timing_Data.median_time(for ((n, t) <- monotone_prefix) yield t - t_p.scale(1.0 / n)) - val a = (time1 - time0).scale(1.0 / (threads1 - threads0)) - val b = time0 - a.scale(threads0) - Time.ms((a.scale(threads) + b).ms max 0) + t_c + t_p.scale(1.0 / threads) + } else { + // Piecewise linear + val ((threads0, time0), (threads1, time1)) = + if (entries.head._1 <= threads && threads <= entries.last._1) { + val split = entries.partition(_._1 <= threads) + (split._1.last, split._2.head) + } else { + val piece = if (threads < entries.head._1) entries.take(2) else entries.takeRight(2) + (piece.head, piece.last) + } + + val a = (time1 - time0).scale(1.0 / (threads1 - threads0)) + val b = time0 - a.scale(threads0) + Time.ms((a.scale(threads) + b).ms max 0) + } } if (approximations.isEmpty) None else Some(Timing_Data.mean_time(approximations)) }