diff --git a/120s-experiments.sh b/120s-experiments.sh new file mode 100755 index 000000000..567766f17 --- /dev/null +++ b/120s-experiments.sh @@ -0,0 +1,15 @@ +#!/bin/bash +set -x +RESTART_AFTER=10 +export CATRA_TIMEOUT=120000 +export CATRA_CONFIGS="baseline,lazy" +export CATRA_THREADS=1 +LOGFILE="${CATRA_CONFIGS}-catra-${RESTART_AFTER}.${CATRA_TIMEOUT}.log" +JARFILE=$(ls -1t benchmark/target/scala-2.13/*.jar | head -1) + +echo "" > "$LOGFILE" + +find 120s-experiments.d -type f | xargs -n $RESTART_AFTER -- \ + java -Xmx10G -jar "$JARFILE" | tee -a "$LOGFILE" + +echo "Done with all experiments!" >> "$LOGFILE" diff --git a/Makefile b/Makefile index 8a3ccaa52..39fbf0cb2 100644 --- a/Makefile +++ b/Makefile @@ -1,10 +1,21 @@ -current_version = $(shell git rev-parse --short HEAD) +current_version = $(shell sbt -Dsbt.supershell=false -error "print version") TIMEOUT_MS = 30000 EXPERIMENT_DIR = parikh-plus .PHONY: all all: experiments +catra-experiments.zip: build.sbt + sbt benchmark/assembly + zip catra-experiments.zip \ + -r 120s-experiments.* \ + $(shell ls -1t benchmark/target/scala-2.13/*.jar | head -1) + +catra-${current_version}.zip: + sbt assembly + zip catra-${current_version}.zip bin/catra target/scala-2.13/uuverifiers/catra-assembly-${current_version}.jar + + clean: sbt clean diff --git a/benchmark/src/main/scala/RunBenchmarks.scala b/benchmark/src/main/scala/RunBenchmarks.scala index 923e0293d..27c3a0532 100644 --- a/benchmark/src/main/scala/RunBenchmarks.scala +++ b/benchmark/src/main/scala/RunBenchmarks.scala @@ -10,54 +10,43 @@ import scala.util.{Failure, Random, Success, Try} object RunBenchmarks extends App { import catra.SolveRegisterAutomata.measureTime - private val regularTimeout = sys.env.getOrElse("CATRA_TIMEOUT", "30000").toInt - private val nrMaterialiseEager = 500 + private val timeout = + sys.env.getOrElse("CATRA_TIMEOUT", "30000").toInt + private val nrMaterialiseEager = 200 private val nrMaterialiseLazy = 1 - private val cactusTimeout = "120000" private val baseConfigurations = Map( "nuxmv" -> Array("--backend", "nuxmv"), "baseline" -> Array("--backend", "baseline"), - "lazy-new" -> Array("--backend", "lazy"), - "lazy-old" -> Array("--backend", "lazy", "--old-behaviour") /*, - // Cactus plot entries: - - "baseline-cactus" -> Array( + "lazy" -> Array("--backend", "lazy"), + "lazy-no-clauselearning" -> Array( "--backend", - "baseline", - "--timeout", - cactusTimeout + "lazy", + "--no-clause-learning" ), - "lazy-cactus" -> Array("--backend", "lazy", "--timeout", cactusTimeout), - "lazy-no-clauselearning" -> Array( + "lazy-no-clauselearning-no-restarts" -> Array( "--backend", "lazy", "--no-restarts", - "--no-clause-learning", - "--timeout", - cactusTimeout + "--no-clause-learning" ), s"lazy-eager-$nrMaterialiseEager" -> Array( "--backend", "lazy", "--nr-unknown-to-start-materialise", - nrMaterialiseEager.toString, - "--timeout", - cactusTimeout + nrMaterialiseEager.toString ), s"lazy-lazy-$nrMaterialiseLazy" -> Array( "--backend", "lazy", "--nr-unknown-to-start-materialise", - nrMaterialiseLazy.toString, - "--timeout", - cactusTimeout - )*/ + nrMaterialiseLazy.toString + ) ).view .mapValues( c => catra.CommandLineOptions .parse( - Array("solve-satisfy", "--timeout", regularTimeout.toString) ++ c + Array("solve-satisfy", "--timeout", timeout.toString) ++ c ) .get ) @@ -67,8 +56,8 @@ object RunBenchmarks extends App { .getOrElse("CATRA_CONFIGS", baseConfigurations.keys.mkString(",")) .split(",") .toSet - private val filteredConfigurations = baseConfigurations - // baseConfigurations.view.filterKeys(selectConfigurations).toMap + private val filteredConfigurations = + baseConfigurations.view.filterKeys(selectConfigurations.contains).toMap private val instanceFiles = args.flatMap(catra.CommandLineOptions.expandFileNameOrDirectoryOrGlob) @@ -104,8 +93,7 @@ object RunBenchmarks extends App { }.toSeq) private val runtime = Runtime.getRuntime -// private val nrWorkers = runtime.availableProcessors / 4 - private val nrWorkers = 1 + private val nrWorkers = sys.env.getOrElse("CATRA_THREADS", "6").toInt print( s"INFO ${Calendar.getInstance().getTime} JVM version: ${System.getProperty("java.version")}" @@ -123,7 +111,7 @@ object RunBenchmarks extends App { .solveSatisfy(instances(0)._2) println("...warm-up done!") - private val (_, totalTimeSpent) = measureTime { + private val (exitCode, totalTimeSpent) = measureTime { val runner = new ExperimentRunner(experiments, nrWorkers) println(s"CONFIGS ${configNames.mkString("\t")}") @@ -131,33 +119,42 @@ object RunBenchmarks extends App { case (name, config) => println(s"CONFIG $name IS $config") } - println(s"TIMEOUT $regularTimeout") + println(s"TIMEOUT $timeout") val safetyMargin = 1000 * experiments.length val maxTimeout = Duration( - (experiments.length * regularTimeout) + safetyMargin, + (experiments.length * timeout) + safetyMargin, duration.MILLISECONDS ) println(s"HARD TIMEOUT $maxTimeout FOR ALL") - runner.results(maxTimeout) match { - case Failure(_: TimeoutException) => + val exitCode = runner.results(maxTimeout) match { + case Failure(_: TimeoutException) => { println("ERR hard timeout, some experiment is misbehaving!") - case Failure(e) => println(s"ERR unknown error running experiments: $e") - case Success(outcomes) => + 1 + } + case Failure(e) => { + println(s"ERR unknown error running experiments: $e") + 1 + } + case Success(outcomes) => { for ((instance, rs) <- outcomes) { val rsMap = rs.toMap println( s"RESULT $instance\t${configNames.map(c => fmtResult(rsMap(c))).mkString("\t")}" ) } + 0 + } } runner.stop() + exitCode } println( s"INFO ${Calendar.getInstance().getTime} Executed ${experiments.length} experiments with ${filteredConfigurations.size} configurations and ${instances.length} instances in $totalTimeSpent." ) + System.exit(exitCode) } diff --git a/bin/experiments.sh b/bin/experiments.sh index 90952aa0b..900957df1 100755 --- a/bin/experiments.sh +++ b/bin/experiments.sh @@ -11,6 +11,6 @@ echo "" > $LOGFILE echo "${CURRENT_VERSION}: Executing experiments in parallel, logging to ${LOGFILE}" find "$@" -type f | xargs -n $RESTART_AFTER -- \ - java -XX:MaxRAMPercentage=90.0 -jar "$JARFILE" | tee -a "$LOGFILE" + java -Xmx100G -jar "$JARFILE" | tee -a "$LOGFILE" echo "Done with all experiments!" >> "$LOGFILE" diff --git a/build.sbt b/build.sbt index 4360bed61..35e654d23 100644 --- a/build.sbt +++ b/build.sbt @@ -45,7 +45,7 @@ lazy val root = (project in file(".")) lazy val benchmark = (project in file("benchmark")) .settings( name := "catra-benchmark", - version := s"${version.value}-7", // Version scheme is CATRA version - benchmark version + version := s"${version.value}-9", // Version scheme is CATRA version - benchmark version assembly / mainClass := Some( "uuverifiers.RunBenchmarks" )