Some scripts for visualizing profiling results

eval/cp/scripts/base-gnuplot-script

+set terminal postscript color
+set key autotitle columnhead
+set style fill solid 1.00 border -1
+set style data histogram
+set style histogram cluster gap 1
+#set boxwidth 0.75 absolute

eval/cp/scripts/generate-graph

+#!/bin/sh
+
+filename=$1
+title=`basename ${1}`
+graphName=../graphs/${title}.ps
+trans=transposed
+cat ${filename} | grep "GRAPH: " | sed 's/GRAPH: '// | ./transpose.awk > ${trans}
+
+cat base-gnuplot-script > plotscript
+echo "set title \"${title}\"" >> plotscript
+echo "set output \"${graphName}\"" >> plotscript
+echo "set xlabel \"Invocations\"" >> plotscript
+echo "set ylabel \"Execution time (s)\"" >> plotscript
+echo "plot \"${trans}\" using 1, '' using 2, '' using 3, '' using 4, '' using 5" >> plotscript
+gnuplot plotscript
+rm plotscript
+rm ${trans}

eval/cp/scripts/run-cp-evaluation

+#!/bin/bash
+
+cd ../../..
+
+ts=`date +%F-%R`
+evalFolder="eval/cp/data"
+demoFolder="cp-demo"
+
+#classes=( "RedBlackTree" "SortedList" )
+
+if [ "$#" -lt "3" ]
+then
+  echo "Please provide a class name and bounds for problem size"
+  exit 1
+fi
+
+class=${1}
+base=${2}
+limit=${3}
+
+mkdir -p ${evalFolder}
+
+evalFileBase=${evalFolder}/${class}-${ts}-CAV
+./cp CAV ${demoFolder}/${class}.scala || (echo "Could not compile..." && exit 1)
+
+for (( i=${base}; i<=${limit}; i++ ))
+do
+  currentFile=${evalFileBase}-${i}
+  ./cp-runner ${class} $i | tee -a ${currentFile}
+  cd eval/cp/scripts
+  ./generate-graph ../../../${currentFile}
+  cd ../../..
+done

eval/cp/scripts/transpose.awk

+#!/usr/bin/gawk -f
+# ___  _  _ ____ ___ ___ ____ ___  ____ 
+# |  \ |  | |     |   |  |__| |__] |___ 
+# |__/ |__| |___  |   |  |  | |    |___ 
+#
+# The scripts were written to be usefull in
+# a research enviornment, but anyone is welcome
+# to use them.  Happy awking.  -Tim Sherwood
+
+BEGIN {
+	FS = " ";
+	max_x =0;
+	max_y =0;
+}
+
+{
+	max_y++;
+	for( i=1; i<=NF; i++ )
+	{
+		if (i>max_x) max_x=i;
+		A[i,max_y] = $i;
+	}
+}
+
+END {
+	for ( x=1; x<=max_x; x++ )
+	{
+		for ( y=1; y<=max_y; y++ )
+		{
+			if ( (x,y) in A ) printf "%s",A[x,y];
+			if ( y!=max_y ) printf " ";
+		}
+		printf "\n";
+	}
+}

run-evaluation → eval/funcheck/scripts/run-evaluation

 #!/bin/bash
 
+cd ../../..
+
 ts=`date +%F-%R`
 demoFolder="demo"
 files=( ${demoFolder}"/AssociativeList.scala" ${demoFolder}/"InsertionSort.scala" ${demoFolder}"/RedBlackTree.scala" ${demoFolder}"/PropositionalLogic.scala" "${demoFolder}/ListWithSize.scala")
-#files=( ${pldi}"/RedBlackTree.scala" )
+
+dataFolder="eval/funcheck/data"
+
 if [ "$#" -lt "1" ]
 then
   echo "Please provide an unrolling value"
@@ -17,18 +21,18 @@ do
   ./funcheck CAV $f
 done
 
-mv summary summary-CAV-${ts}
+mv summary ${dataFolder}/summary-CAV-${ts}
 
 for f in ${files[@]}
 do
   ./funcheck CAV prune $f
 done
 
-mv summary summary-CAV-prune-${ts}
+mv summary ${dataFolder}/summary-CAV-prune-${ts}
 
 for f in ${files[@]}
 do
   ./funcheck PLDI unrolling=${1} $f
 done
 
-mv summary summary-PLDI-${ts}
+mv summary ${dataFolder}/summary-PLDI-${ts}

src/cp/RuntimeMethods.scala

@@ -330,6 +330,7 @@ object RuntimeMethods {
           val stopwatch = new Stopwatch("hasNext", true).start
           val (outcome, model) = solver.decideWithModel(toCheck, false)
           stopwatch.stop
+          stopwatch.writeToSummary
           val toReturn = (outcome match {
             case Some(false) =>
               // there is a solution, we need to complete model for nonmentioned variables
@@ -366,9 +367,7 @@ object RuntimeMethods {
       override def next() : Map[Identifier, Expr] = nextModel match {
         case None => {
           // Let's compute the next model
-          val stopwatch = new Stopwatch("next", true).start
           val (outcome, model) = solver.decideWithModel(toCheck, false)
-          stopwatch.stop
           val toReturn = (outcome match {
             case Some(false) =>
               // there is a solution, we need to complete model for nonmentioned variables

src/purescala/FairZ3Solver.scala

@@ -254,7 +254,14 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
   }
 
   def decideWithModel(vc: Expr, forValidity: Boolean): (Option[Boolean], Map[Identifier,Expr]) = {
-    val initializationStopwatch = new Stopwatch("decideWithModel init", true).start
+    val initializationStopwatch = new Stopwatch("init", true)
+    val blocking2Z3Stopwatch    = new Stopwatch("blocking-set-to-z3", true)
+    val z3SearchStopwatch       = new Stopwatch("z3-search-1", true)
+    val secondZ3SearchStopwatch = new Stopwatch("z3-search-2", true)
+    val unrollingStopwatch      = new Stopwatch("unrolling", true)
+
+    initializationStopwatch.start
+
     var forceStop : Boolean = false
 
     var foundDefinitiveAnswer : Boolean = false
@@ -312,12 +319,11 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
     while(!foundDefinitiveAnswer && !forceStop) {
       iterationsLeft -= 1
 
-      val blocking2Z3Stopwatch = new Stopwatch("Blocking to Z3 conv").start
+      blocking2Z3Stopwatch.start
       val blockingSetAsZ3 : Seq[Z3AST] = blockingSet.map(toZ3Formula(z3, _).get).toSeq
       // println("Blocking set : " + blockingSet)
       blocking2Z3Stopwatch.stop
 
-      val assertBlockingStopwatch = new Stopwatch("Assert blocking set").start
       if(Settings.useCores) {
         // NOOP
       } else {
@@ -325,16 +331,15 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
         if(!blockingSetAsZ3.isEmpty)
           z3.assertCnstr(z3.mkAnd(blockingSetAsZ3 : _*))
       }
-      assertBlockingStopwatch.stop
 
       reporter.info(" - Running Z3 search...")
       val (answer, model, core) : (Option[Boolean], Z3Model, Seq[Z3AST]) = if(Settings.useCores) {
         println(blockingSetAsZ3)
         z3.checkAssumptions(blockingSetAsZ3 : _*)
       } else {
-        val stopwatch = new Stopwatch("Z3 search", true).start
+        z3SearchStopwatch.start
         val (a, m) = z3.checkAndGetModel()
-        stopwatch.stop
+        z3SearchStopwatch.stop
         (a, m, Seq.empty[Z3AST])
       }
 
@@ -385,9 +390,9 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
           if(!Settings.useCores) {
             z3.pop(1)
             
-            val stopwatch = new Stopwatch("Second Z3 search", true).start
+            secondZ3SearchStopwatch.start
             val (result2,m2) = z3.checkAndGetModel()
-            stopwatch.stop
+            secondZ3SearchStopwatch.stop
 
             if (result2 == Some(false)) {
               foundAnswer(Some(true))
@@ -407,7 +412,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
           if(!foundDefinitiveAnswer) { 
             reporter.info("- We need to keep going.")
 
-            val unrollingStopwatch = new Stopwatch("Unrolling", true).start
+            unrollingStopwatch.start
 
             val toRelease : Set[Expr] = if(Settings.useCores) {
               core.map(ast => fromZ3Formula(ast) match {
@@ -491,6 +496,12 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
       }
     }
 
+    initializationStopwatch.writeToSummary
+    blocking2Z3Stopwatch.writeToSummary
+    z3SearchStopwatch.writeToSummary
+    secondZ3SearchStopwatch.writeToSummary
+    unrollingStopwatch.writeToSummary
+
     if(forceStop) {
       (None, Map.empty)
     } else {

src/purescala/Stopwatch.scala

@@ -4,27 +4,36 @@ package purescala
 class Stopwatch(description : String, verbose : Boolean = false) {
   var beginning: Long = 0L
   var end: Long = 0L
+  var acc: Long = 0L
+
   def start : Stopwatch = {
     beginning = System.currentTimeMillis
     this
   }
+
   def stop : Double = {
     end = System.currentTimeMillis
+    acc += (end - beginning)
     val seconds = (end - beginning) / 1000.0
     if (verbose) println("Stopwatch %-25s: %-3.3fs" format (description, seconds))
-    Stopwatch.timeLog += 
-      (description -> (Stopwatch.timeLog.getOrElse(description, Nil) :+ seconds))
     seconds
   }
+
+  def writeToSummary : Unit = {
+    Stopwatch.timeLog += 
+      (description -> (Stopwatch.timeLog.getOrElse(description, Nil) :+ ((end - beginning) / 1000.0)))
+  }
 }
 
 object Stopwatch {
   val timeLog = scala.collection.mutable.Map[String, Seq[Double]]()
 
   def printSummary : Unit = {
-    val toPrint = timeLog.map{case (k, v) => ("%-25s" format k, v.foldLeft(0.0){case (a, b) => a + b})}.mkString("\n")
+    val toPrint = timeLog.map{case (k, v) => ("%-25s" format k) + "(" + v.size + ") Total: " + v.foldLeft(0.0){case (a, b) => a + b} + "\n" + v.mkString(" ")}.mkString("\n")
+    val forGraph = timeLog.map{ case (k, v) => "GRAPH: " + k + " " + v.mkString(" ")}.mkString("\n")
 
     println("Total times per stopwatch description")
     println(toPrint)
+    println(forGraph)
   }
 }