From 71a5144de93cb2eb18998fb0715570fb05447f8d Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Wed, 12 Feb 2014 15:28:35 +0100
Subject: [PATCH] Improve timers collection, usage and display
---
src/main/scala/leon/LeonContext.scala | 2 +-
src/main/scala/leon/Main.scala | 16 +-
.../frontends/scalac/ExtractionPhase.scala | 4 +
.../leon/solvers/EnumerationSolver.scala | 2 +
.../leon/solvers/z3/AbstractZ3Solver.scala | 6 +-
.../scala/leon/solvers/z3/FairZ3Solver.scala | 4 +
.../scala/leon/synthesis/SimpleSearch.scala | 12 +-
.../scala/leon/synthesis/Synthesizer.scala | 11 +-
.../search/AndOrGraphParallelSearch.scala | 11 --
src/main/scala/leon/utils/Timer.scala | 184 ++++++++++++------
10 files changed, 154 insertions(+), 98 deletions(-)
diff --git a/src/main/scala/leon/LeonContext.scala b/src/main/scala/leon/LeonContext.scala
index 633ba2d4e..8eea31aa7 100644
--- a/src/main/scala/leon/LeonContext.scala
+++ b/src/main/scala/leon/LeonContext.scala
@@ -16,5 +16,5 @@ case class LeonContext(
settings: Settings = Settings(),
options: Seq[LeonOption] = Seq(),
files: Seq[File] = Seq(),
- timers: TimerCollections = new TimerCollections
+ timers: TimerStorage = new TimerStorage
)
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 1b7377975..461db366c 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -222,8 +222,6 @@ object Main {
}
def main(args : Array[String]) {
- val timer = new Timer().start
-
val argsl = args.toList
// By default we add --library from Main
@@ -256,12 +254,10 @@ object Main {
try {
ctx.interruptManager.registerSignalHandler()
- ctx.timers.get("Leon Opts") += timer
-
// Compute leon pipeline
val pipeline = computePipeline(ctx.settings)
- timer.restart
+ val timer = ctx.timers.total.start()
// Run pipeline
pipeline.run(ctx)(args.toList) match {
@@ -274,16 +270,10 @@ object Main {
case _ =>
}
- ctx.timers.get("Leon Run") += timer
+ timer.stop()
ctx.reporter.whenDebug(DebugSectionTimers) { debug =>
- debug("-"*80)
- debug("Times:")
- debug("-"*80)
- for ((name, swc) <- ctx.timers.getAll.toSeq.sortBy(_._1)) {
- debug(swc.toString)
- }
- debug("-"*80)
+ ctx.timers.outputTable(debug)
}
} catch {
diff --git a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
index 6200332b8..c91b55826 100644
--- a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
+++ b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
@@ -18,6 +18,7 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
implicit val debug = DebugSectionTrees
def run(ctx: LeonContext)(args: List[String]): Program = {
+ val timer = ctx.timers.frontend.start()
val settings = new NSCSettings
@@ -55,11 +56,14 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
// )
// }
+
val compiler = new ScalaCompiler(settings, ctx)
val run = new compiler.Run
run.compile(command.files)
+ timer.stop()
+
val pgm = Program(FreshIdentifier("__program"), compiler.leonExtraction.modules)
ctx.reporter.debug(pgm.asString(ctx))
pgm
diff --git a/src/main/scala/leon/solvers/EnumerationSolver.scala b/src/main/scala/leon/solvers/EnumerationSolver.scala
index 39203125c..79a7dba86 100644
--- a/src/main/scala/leon/solvers/EnumerationSolver.scala
+++ b/src/main/scala/leon/solvers/EnumerationSolver.scala
@@ -47,6 +47,7 @@ class EnumerationSolver(val context: LeonContext, val program: Program) extends
private var modelMap = Map[Identifier, Expr]()
def check: Option[Boolean] = {
+ val timer = context.timers.solvers.enum.check.start()
val res = try {
datagen = Some(new VanuatooDataGen(context, program))
if (interrupted) {
@@ -71,6 +72,7 @@ class EnumerationSolver(val context: LeonContext, val program: Program) extends
None
}
datagen = None
+ timer.stop()
res
}
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 06a94d7dd..077602062 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -181,7 +181,8 @@ trait AbstractZ3Solver
var isInitialized = false
protected[leon] def initZ3() {
if (!isInitialized) {
- val initTime = new Timer().start
+ val timer = context.timers.solvers.z3.init.start()
+
counter = 0
z3 = new Z3Context(z3cfg)
@@ -199,8 +200,7 @@ trait AbstractZ3Solver
isInitialized = true
- initTime.stop
- context.timers.get("Z3Solver init") += initTime
+ timer.stop()
}
}
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index e220314d5..208f8f18c 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -414,9 +414,11 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
//reporter.debug("Unroll. Assumptions:\n"+unrollingBank.z3CurrentZ3Blockers.mkString(" && "))
//reporter.debug("Userland Assumptions:\n"+assumptionsAsZ3.mkString(" && "))
+ val timer = context.timers.solvers.z3.check.start()
solver.push() // FIXME: remove when z3 bug is fixed
val res = solver.checkAssumptions((assumptionsAsZ3 ++ unrollingBank.z3CurrentZ3Blockers) :_*)
solver.pop() // FIXME: remove when z3 bug is fixed
+ timer.stop()
reporter.debug(" - Finished search with blocked literals")
@@ -503,9 +505,11 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
reporter.debug(" - Running search without blocked literals (w/o lucky test)")
}
+ val timer = context.timers.solvers.z3.check.start()
solver.push() // FIXME: remove when z3 bug is fixed
val res2 = solver.checkAssumptions(assumptionsAsZ3 : _*)
solver.pop() // FIXME: remove when z3 bug is fixed
+ timer.stop
res2 match {
case Some(false) =>
diff --git a/src/main/scala/leon/synthesis/SimpleSearch.scala b/src/main/scala/leon/synthesis/SimpleSearch.scala
index 8f4ebf4ea..35f7f1ce5 100644
--- a/src/main/scala/leon/synthesis/SimpleSearch.scala
+++ b/src/main/scala/leon/synthesis/SimpleSearch.scala
@@ -149,9 +149,9 @@ class SimpleSearch(synth: Synthesizer,
def searchStep() {
- val t = new Timer().start
+ val timer = synth.context.timers.synthesis.nextLeaf.start()
val nl = nextLeaf()
- synth.context.timers.get("Synthesis NextLeaf") += t
+ timer.stop()
nl match {
case Some(l) =>
@@ -159,15 +159,15 @@ class SimpleSearch(synth: Synthesizer,
case al: g.AndLeaf =>
val sub = expandAndTask(al.task)
- t.restart
+ val timer = synth.context.timers.synthesis.expand.start()
onExpansion(al, sub)
- synth.context.timers.get("Synthesis Expand") += t
+ timer.stop()
case ol: g.OrLeaf =>
val sub = expandOrTask(ol.task)
- t.restart
+ val timer = synth.context.timers.synthesis.expand.start()
onExpansion(ol, sub)
- synth.context.timers.get("Synthesis Expand") += t
+ timer.stop()
}
case None =>
stop()
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 643855a77..238c893e8 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -41,18 +41,11 @@ class Synthesizer(val context : LeonContext,
}
}
- val ts = System.currentTimeMillis()
+ val t = context.timers.synthesis.search.start()
val res = search.search()
- search match {
- case pr: ParallelSearch =>
- context.timers.add(pr.expandTimers)
- context.timers.add(pr.sendWorkTimers)
- case _ =>
- }
-
- val diff = System.currentTimeMillis()-ts
+ val diff = t.stop()
reporter.info("Finished in "+diff+"ms")
if (options.generateDerivationTrees) {
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala b/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
index f486d385d..75124787e 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
@@ -22,9 +22,6 @@ abstract class AndOrGraphParallelSearch[WC,
var system: ActorSystem = _
- val sendWorkTimers = new TimerCollection("Synthesis-par SendWork")
- val expandTimers = new TimerCollection("Synthesis-par Expand")
-
def search(): Option[(S, Boolean)] = {
system = ActorSystem("ParallelSearch")
@@ -96,8 +93,6 @@ abstract class AndOrGraphParallelSearch[WC,
assert(idleWorkers.size > 0)
- val t = new Timer().start
-
getNextLeaves(idleWorkers, workingWorkers) match {
case Nil =>
if (workingWorkers.isEmpty) {
@@ -118,8 +113,6 @@ abstract class AndOrGraphParallelSearch[WC,
}
}
}
-
- sendWorkTimers += t
}
context.setReceiveTimeout(10.seconds)
@@ -136,9 +129,7 @@ abstract class AndOrGraphParallelSearch[WC,
case WorkerAndTaskDone(w, res) =>
workers.get(w) match {
case Some(Some(l: g.AndLeaf)) =>
- val t = new Timer().start
onExpansion(l, res)
- expandTimers += t
workers += w -> None
case _ =>
}
@@ -147,9 +138,7 @@ abstract class AndOrGraphParallelSearch[WC,
case WorkerOrTaskDone(w, res) =>
workers.get(w) match {
case Some(Some(l: g.OrLeaf)) =>
- val t = new Timer().start
onExpansion(l, res)
- expandTimers += t
workers += w -> None
case _ =>
}
diff --git a/src/main/scala/leon/utils/Timer.scala b/src/main/scala/leon/utils/Timer.scala
index 8dc3c54c3..842a508b1 100644
--- a/src/main/scala/leon/utils/Timer.scala
+++ b/src/main/scala/leon/utils/Timer.scala
@@ -3,42 +3,13 @@
package leon
package utils
-class TimerCollection(val name: String) {
- var min: Long = 0L
- var tot: Long = 0L
- var max: Long = 0L
- var n: Int = 0
-
- def +=(sw: Timer) = synchronized {
- val ms = sw.getMillis
- if(n == 0 || ms < min) {
- min = ms
- }
- if(n == 0 || ms > max) {
- max = ms
- }
- n += 1
- tot += ms
- }
-
- override def toString = {
- if (n == 0) {
- "%-30s N/A".format(name+":")
- } else if (n > 1) {
- "%-30s %6d ms (min: %d, avg: %d, max: %d, n: %d)".format(name+":", tot, min, tot/n, max, n)
- } else {
- "%-30s %6d ms".format(name+":", tot)
- }
- }
-
- def getMillis = tot
-}
+import scala.language.dynamics
/** Implements a timer for profiling purposes */
-class Timer(name: String = "Timer") {
+class Timer() {
var beginning: Long = 0L
var end: Long = 0L
- var acc: Long = 0L
+ var runs: List[Long] = Nil
def start: this.type = {
beginning = System.currentTimeMillis
@@ -46,45 +17,148 @@ class Timer(name: String = "Timer") {
this
}
- def restart: this.type = {
+ def restart: this.type = {
beginning = 0L
end = 0L
- acc = 0L
+ runs = Nil
start
}
- def stop {
- end = System.currentTimeMillis
- acc += (end - beginning)
- beginning = 0L
+ def stop = {
+ end = System.currentTimeMillis
+ runs ::= (end - beginning)
+ beginning = 0L
+ runs.head
}
- def getMillis: Long = {
- if (isRunning) {
- acc + (System.currentTimeMillis-beginning)
+ def isRunning = beginning != 0L
+
+ override def toString = {
+ val n = runs.size
+
+ if (n == 0) {
+ "N/A"
+ } else if (n > 1) {
+ val tot = runs.sum
+ val min = runs.min
+ val max = runs.max
+
+ "(min: %3d, avg: %3d, max: %3d, n: %3d) %6d ms".format(min, tot/n, max, n, tot)
} else {
- acc
+ val tot = runs.sum
+
+ "%6d ms".format(tot)
}
}
+}
- def isRunning = beginning != 0L
+class TimerStorage extends Dynamic {
+ var keys = List[String]()
+ var fields = Map[String, TimerStorage]()
+ var selfTimer: Option[Timer] = None
+
+ def get(name: String): TimerStorage = {
+ fields.get(name) match {
+ case Some(t) =>
+ t
+
+ case None =>
+ val t = new TimerStorage()
+ fields += name -> t
+ keys ::= name
+ t
+ }
+ }
- override def toString = "%20s: %5d%sms".format(name, getMillis, if (isRunning) "..." else "")
-}
+ private def isLastKeys(n: String) = Some(n) == keys.headOption
-class TimerCollections {
- private var all = Map[String, TimerCollection]()
+ def selectDynamic(name: String): TimerStorage = get(name)
- def get(name: String): TimerCollection = all.getOrElse(name, {
- val sw = new TimerCollection(name)
- all += name -> sw
- sw
- })
- def add(swc: TimerCollection) {
- all += swc.name -> swc
+ def start() = {
+ if (selfTimer.isEmpty) {
+ selfTimer = Some(new Timer)
+ }
+ selfTimer.get.start
+
+ this
+ }
+
+ def stop() = {
+ selfTimer.get.stop
}
- def getAll = all
+ def outputTable(printer: String => Unit) = {
+ import utils.ASCIITables._
+
+ var table = Table("Timers")
+
+ table += Row(Seq(
+ Cell("name"),
+ Cell("min"),
+ Cell("avg"),
+ Cell("max"),
+ Cell("n"),
+ Cell("total")
+ ))
+ table += Separator
+
+ var closed = Set[TimerStorage]()
+
+ def output(ts: TimerStorage, path: List[(TimerStorage, String)]): Unit = {
+ val indent = path.map { case (from, name) =>
+ if (closed(from)) {
+ " "
+ } else if (from.isLastKeys(name)) {
+ closed += from
+ "└ "
+ } else {
+ "├ "
+ }
+ }.reverse.mkString
+
+ (path, ts.selfTimer) match {
+ case ((_, name) :: _, Some(t)) =>
+ val n = t.runs.size
+ val tot = t.runs.sum
+
+ val (min: String, avg: String, max: String, total: String) = if (n == 0) {
+ ("", "", "", "N/A")
+ } else if (n > 1) {
+ val min = t.runs.min
+ val max = t.runs.max
+ val avg = tot/n
+ (f"$min%d", f"$avg%d", f"$max%d", f"$tot%d")
+ } else {
+ ("", "", "", f"$tot%d")
+ }
+
+ table += Row(Seq(
+ Cell(indent+name),
+ Cell(min),
+ Cell(avg),
+ Cell(max),
+ Cell(n),
+ Cell(tot)
+ ))
+ case ((_, name) :: _, None) =>
+ table += Row(Seq(
+ Cell(indent+name, 6)
+ ))
+ case _ =>
+
+ }
+
+ ts.keys.reverse.map(n => n -> ts.fields(n)).foreach { case (name, nts) =>
+ output(nts, (ts -> name) :: path)
+ }
+ }
+
+ if (fields.nonEmpty) {
+ output(this, Nil)
+ }
+
+ printer(table.render)
+ }
}
--
GitLab