From 9450e911c59dd22379d473752028425816faa2f5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ali=20Sinan=20K=C3=B6ksal?= <alisinan@gmail.com>
Date: Tue, 26 Apr 2011 13:34:57 +0000
Subject: [PATCH] Some scripts for visualizing profiling results
---
eval/cp/scripts/base-gnuplot-script | 6 ++++
eval/cp/scripts/generate-graph | 17 +++++++++
eval/cp/scripts/run-cp-evaluation | 33 +++++++++++++++++
eval/cp/scripts/transpose.awk | 35 +++++++++++++++++++
.../funcheck/scripts/run-evaluation | 12 ++++---
src/cp/RuntimeMethods.scala | 3 +-
src/purescala/FairZ3Solver.scala | 29 ++++++++++-----
src/purescala/Stopwatch.scala | 15 ++++++--
8 files changed, 132 insertions(+), 18 deletions(-)
create mode 100644 eval/cp/scripts/base-gnuplot-script
create mode 100755 eval/cp/scripts/generate-graph
create mode 100755 eval/cp/scripts/run-cp-evaluation
create mode 100755 eval/cp/scripts/transpose.awk
rename run-evaluation => eval/funcheck/scripts/run-evaluation (73%)
diff --git a/eval/cp/scripts/base-gnuplot-script b/eval/cp/scripts/base-gnuplot-script
new file mode 100644
index 000000000..693f1b269
--- /dev/null
+++ b/eval/cp/scripts/base-gnuplot-script
@@ -0,0 +1,6 @@
+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
diff --git a/eval/cp/scripts/generate-graph b/eval/cp/scripts/generate-graph
new file mode 100755
index 000000000..245939fa9
--- /dev/null
+++ b/eval/cp/scripts/generate-graph
@@ -0,0 +1,17 @@
+#!/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}
diff --git a/eval/cp/scripts/run-cp-evaluation b/eval/cp/scripts/run-cp-evaluation
new file mode 100755
index 000000000..139df7cdf
--- /dev/null
+++ b/eval/cp/scripts/run-cp-evaluation
@@ -0,0 +1,33 @@
+#!/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
diff --git a/eval/cp/scripts/transpose.awk b/eval/cp/scripts/transpose.awk
new file mode 100755
index 000000000..5f6bdd6ab
--- /dev/null
+++ b/eval/cp/scripts/transpose.awk
@@ -0,0 +1,35 @@
+#!/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";
+ }
+}
diff --git a/run-evaluation b/eval/funcheck/scripts/run-evaluation
similarity index 73%
rename from run-evaluation
rename to eval/funcheck/scripts/run-evaluation
index d3f994c1b..76f913e11 100755
--- a/run-evaluation
+++ b/eval/funcheck/scripts/run-evaluation
@@ -1,9 +1,13 @@
#!/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}
diff --git a/src/cp/RuntimeMethods.scala b/src/cp/RuntimeMethods.scala
index 6ecf0096b..d16b4d82e 100644
--- a/src/cp/RuntimeMethods.scala
+++ b/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
diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index 9adb24518..cf440d8f5 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/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 {
diff --git a/src/purescala/Stopwatch.scala b/src/purescala/Stopwatch.scala
index ee71110f5..f1f876354 100644
--- a/src/purescala/Stopwatch.scala
+++ b/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)
}
}
--
GitLab