Merge pull request #22 from h0nzZik/nicer-benchmarks

Nicer benchmarks

examples-hybrid/test.sh

@@ -5,7 +5,7 @@ set -e
 # https://stackoverflow.com/a/246128/6209703
 SCRIPT_DIR=$( cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )
 
-pushd "$SCRIPT_DIR"
+pushd "$SCRIPT_DIR" > /dev/null
 
 TIME=$(which time)
 
@@ -24,17 +24,18 @@ testInCoq() {
   minuska gt2coq ./imp-ast/count-6.imp coqfiles/count6.v
   minuska gt2coq ./imp-ast/count-7.imp coqfiles/count7.v
 
+  echo "Compiling *.v files"
   pushd coqfiles > /dev/null
   for vfile in *.v; do
-    echo "Compiling $vfile"
-    coqc -R . Test "$vfile" > /dev/null
+    echo "Compiling $vfile" > /dev/null
+    coqc -R . Test "$vfile" > /dev/null 2>/dev/null
   done 
   popd > /dev/null
   cp test-imp/testCount*.v ./coqfiles/
   pushd coqfiles > /dev/null
   for testvfile in testCount*.v; do
     echo "coqc $testvfile"
-    "$TIME" --output "$testvfile.time" --format "%e" coqc -R . Test "$testvfile" 2> /dev/null
+    "$TIME" --output "$testvfile.time" --format "%e" coqc -R . Test "$testvfile" 2> /dev/null | grep 'Finished transaction'
     cat "$testvfile.time"
   done
   popd > /dev/null

examples-standalone/README.md

@@ -0,0 +1,49 @@
+# Standalone benchmarks
+
+This directory contains benchmarks for the OCaml-extracted interpreters generated from the language definitions in the [../languages](../languages) directory.
+The script [test.sh](./test.sh) executes the benchmarks and yields an output similar to the following:
+```
+== Compilation
+Compiling fail-invalid-semantics
+Compiling decrement
+Compiling decrement-builtin
+Compiling arith
+Compiling imp
+Compiling two-counters
+
+== Native (via OCaml extraction) benchmarks
+name, total, parsing, execution
+dec-into-2,  0.13,  0.06,  0.00
+dec-into-1,  0.13,  0.06,  0.00
+dec-builtin-into--1,  0.13,  0.06,  0.00
+arith-01,  0.12,  0.06,  0.00
+imp-01,  0.12,  0.06,  0.00
+imp-count-1,  0.14,  0.06,  0.01
+imp-count-2,  0.15,  0.06,  0.02
+imp-count-3,  0.16,  0.06,  0.03
+imp-count-4,  0.17,  0.06,  0.04
+imp-count-5,  0.17,  0.06,  0.04
+imp-count-6,  0.18,  0.06,  0.05
+imp-count-7,  0.18,  0.06,  0.06
+imp-count-10,  0.21,  0.06,  0.08
+two-counters.10,  0.13,  0.06,  0.00
+two-counters.100,  0.14,  0.06,  0.00
+two-counters.1'000,  0.15,  0.06,  0.01
+two-counters.10'000,  0.16,  0.06,  0.04
+two-counters.100'000,  0.50,  0.06,  0.37
+two-counters.1'000'000,  3.83,  0.06,  3.70
+```
+The table in the section titled `Native (via OCaml extraction) benchmarks` contains the results.
+Each row contains one benchmark. The first column contains the name of the benchmark;
+the second column the total time to execute the interpreter (generated by the `time` utility); the third column the time needed to execute the parser on the given input;
+and the last column the time of the actual execution.
+The last two columns are measured by the [OCaml Benchmark package](https://ocaml.org/p/benchmark/latest/doc/Benchmark/index.html).
+The last column is the one most interesting one, because it indicates something about the performance of the actual generated interpreter.
+The total time is higher than the sum of parsing and execution time: the difference is overhead caused by filesystem manipulation, program loading, etc.
+The overhead is non-negligible (over 120 milliseconds in the above example) because Minuska generates a semi-portable executable using the [AppImage technology](https://appimage.org/).
+All times are wall clock, in seconds.
+
+
+
+
+

examples-standalone/test.sh

@@ -5,11 +5,15 @@ set -e
 # https://stackoverflow.com/a/246128/6209703
 SCRIPT_DIR=$( cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )
 
-pushd "$SCRIPT_DIR"
+pushd "$SCRIPT_DIR" > /dev/null
 
 TEMPDIR="$(pwd)/_temp"
 LOGFILEOUT="$TEMPDIR/log-stdout.txt"
 LOGFILEERR="$TEMPDIR/log-stderr.txt"
+if [[ -n "$VERBOSE" ]]; then
+  LOGFILEOUT=/dev/stdout
+  LOGFILEERR=/dev/stderr
+fi
 TIME=$(which time)
 
 rm -rf "$TEMPDIR"
@@ -36,24 +40,27 @@ runCase() {
   local depth="$4"
   local expout="$5"
 
-  output=$(mktemp)
-  echo "Running test '$name'"
-  "$TIME" --output "$output.time" --format "%e" "$interpreter" --depth "$depth" --output-file "$output" "$input" 2>>"$LOGFILEERR" >>"$LOGFILEOUT"
+  local output=$(mktemp)
+  #echo "Running test '$name'"
+  "$TIME" --output "$output.time" --format "%e" "$interpreter" --bench --depth "$depth" --output-file "$output" "$input" >>"$LOGFILEOUT" 2>>"$output".err
   if [[ -e "$expout" ]]; then
     diff "$output" "$expout"
   fi
-  cat "$output.time"
+  local extime=$(cat "$output".err | grep 'Execution' | cut -d ':' -f 2 | xargs)
+  local parsetime=$(cat "$output".err | grep 'Parsing' | cut -d ':' -f 2 | xargs)
+  local mytime=$(cat "$output.time")
+  echo "$name,  $mytime,  $parsetime,  $extime"
   rm -f "$output"
 }
 
 doCompile() {
   local lang="$1"
-  echo "Compiling: minuska generate-interpreter $lang" 
+  echo "Compiling $lang" 
   mkdir -p interpreters
-  pushd interpreters
-  minuska generate-interpreter ../languages/$lang/lang.scm 2>>"$LOGFILEERR" >>"$LOGFILEOUT" && echo "Compilation finished."
+  pushd interpreters > /dev/null
+  minuska generate-interpreter ../languages/$lang/lang.scm 2>>"$LOGFILEERR" >>"$LOGFILEOUT" #&& echo "Compilation finished."
   local state=$?
-  popd
+  popd > /dev/null
   return $state
 }
 
@@ -62,31 +69,44 @@ testNative() {
   rm -rf ./interpreters
   mkdir -p ./interpreters
 
+  echo "== Compilation"
   if doCompile fail-invalid-semantics ; then
     echo "ERROR: an invalid language definition compiles!"
     exit 1
   fi
 
-
   doCompile decrement
-  echo "Decrement tests"
-  runCase "dec into 2" ./interpreters/decrement-interpreter ./languages/decrement/tests/three.dec 2 DONOTTTEST
-  runCase "dec into 1" ./interpreters/decrement-interpreter ./languages/decrement/tests/three.dec 3 DONOTTTEST
+  doCompile decrement-builtin
+  doCompile arith
+  doCompile imp
+  doCompile two-counters
 
 
-  doCompile decrement-builtin
-  runCase "dec builtin into -1" ./interpreters/decrement-builtin-interpreter ./languages/decrement-builtin/tests/cfg_3.decb 5 ./languages/decrement-builtin/tests/cfg_minus_1
+  echo
+  echo "== Native (via OCaml extraction) benchmarks"
+  echo "name, total, parsing, execution"
+
+  #echo "Decrement tests"
+  runCase "dec-into-2" ./interpreters/decrement-interpreter ./languages/decrement/tests/three.dec 2 DONOTTTEST
+  runCase "dec-into-1" ./interpreters/decrement-interpreter ./languages/decrement/tests/three.dec 3 DONOTTTEST
+
+
+  runCase "dec-builtin-into--1" ./interpreters/decrement-builtin-interpreter ./languages/decrement-builtin/tests/cfg_3.decb 5 ./languages/decrement-builtin/tests/cfg_minus_1
 
-  doCompile arith
   runCase "arith-01" ./interpreters/arith-interpreter ./languages/arith/tests/01.arith 20 ./languages/arith/tests/01.result
 
-  doCompile imp
   runCase "imp-01" ./interpreters/imp-interpreter ./languages/imp/tests/01.imp 20 ./languages/imp/tests/01.result
   #runCase "imp-lookup" ./interpreters/imp-interpreter ./languages/imp/tests/00-assign-lookup-trivial.imp 20 ./languages/imp/tests/00-assign-lookup-trivial.result
-  runCase "imp-count-10" ./interpreters/imp-interpreter ./languages/imp/tests/03-count-10.imp 1000 ./languages/imp/tests/03-count-10.result
 
+  runCase "imp-count-1" ./interpreters/imp-interpreter ./languages/imp/tests/count-1.imp 1000000 DONTTEST
+  runCase "imp-count-2" ./interpreters/imp-interpreter ./languages/imp/tests/count-2.imp 1000000 DONTTEST
+  runCase "imp-count-3" ./interpreters/imp-interpreter ./languages/imp/tests/count-3.imp 1000000 DONTTEST
+  runCase "imp-count-4" ./interpreters/imp-interpreter ./languages/imp/tests/count-4.imp 1000000 DONTTEST
+  runCase "imp-count-5" ./interpreters/imp-interpreter ./languages/imp/tests/count-5.imp 1000000 DONTTEST
+  runCase "imp-count-6" ./interpreters/imp-interpreter ./languages/imp/tests/count-6.imp 1000000 DONTTEST
+  runCase "imp-count-7" ./interpreters/imp-interpreter ./languages/imp/tests/count-7.imp 1000000 DONTTEST
+  runCase "imp-count-10" ./interpreters/imp-interpreter ./languages/imp/tests/03-count-10.imp 1000000 ./languages/imp/tests/03-count-10.result
 
-  doCompile two-counters
   runCase "two-counters.10"        ./interpreters/two-counters-interpreter ./languages/two-counters/tests/10.tc      50000000 ./languages/two-counters/tests/10.result
   runCase "two-counters.100"       ./interpreters/two-counters-interpreter ./languages/two-counters/tests/100.tc     50000000 ./languages/two-counters/tests/100.result
   runCase "two-counters.1'000"     ./interpreters/two-counters-interpreter ./languages/two-counters/tests/1000.tc    50000000 ./languages/two-counters/tests/1000.result

flake.nix

@@ -21,6 +21,10 @@
             ln -s ${nix-appimage.outputs.packages.${system}.runtime} $out/libexec/appimage-runtime
           ''
         ;
+        appimagetool-wrapper = pkgs.writeShellScriptBin "appimagetool" ''
+	  export PATH="${pkgs.appimagekit}/bin:$PATH"
+          ${pkgs.appimagekit}/bin/appimagetool --runtime-file "${runtime}/libexec/appimage-runtime" $@
+        '';
 
         minuskaFun = { coqPackages }: (
            let coqVersion = coqPackages.coq.coq-version; in
@@ -40,6 +44,7 @@
               coqPackages.coq.ocamlPackages.core_unix
               coqPackages.coq.ocamlPackages.ppx_jane
               coqPackages.coq.ocamlPackages.ppx_sexp_conv
+              coqPackages.coq.ocamlPackages.benchmark
            ] ++ coqLibraries ; in
            let wrapped = coqPackages.callPackage  ( { coq, stdenv }: coqPackages.mkCoqDerivation {
 
@@ -52,7 +57,8 @@
             nativeBuildInputs = [
               pkgs.makeWrapper
               pkgs.dune_3
-              pkgs.appimagekit
+              appimagetool-wrapper
+              #pkgs.appimagekit
               coqPackages.coq.ocamlPackages.menhir
               coqPackages.coq.ocamlPackages.odoc
             ] ++ bothNativeAndOtherInputs;
@@ -70,8 +76,7 @@
               substituteInPlace bin/main.ml \
                 --replace-fail "/coq/user-contrib/Minuska" "/coq/${coqVersion}/user-contrib/Minuska" \
                 --replace-fail "ocamlfind" "${coqPackages.coq.ocamlPackages.findlib}/bin/ocamlfind" \
-                --replace-fail "coqc" "${coqPackages.coq}/bin/coqc" \
-                --replace-fail "appimagetool" "${pkgs.appimagekit}/bin/appimagetool --runtime-file ${runtime}/libexec/appimage-runtime"
+                --replace-fail "coqc" "${coqPackages.coq}/bin/coqc"
             '';
 
 

minuska/coq-minuska.opam

@@ -12,6 +12,7 @@ homepage: "https://github.com/h0nzZik/minuska"
 bug-reports: "https://github.com/h0nzZik/minuska/issues"
 depends: [
   "dune" {>= "3.14"}
+  "benchmark"
   "coq"
   "menhir"
   "core"

minuska/dune-project

@@ -21,6 +21,7 @@
 (package
  (name coq-minuska)
  (depends
+    benchmark
     coq
     menhir
     core

minuska/lib/dune

@@ -23,6 +23,7 @@
  (public_name coq-minuska)
  (modules syntax parser lexer miparse micoqprint miunparse miskeleton libminuska dsm)
  (libraries
+    benchmark
     core
     zarith
     core_unix

minuska/lib/miskeleton.ml

@@ -90,12 +90,22 @@ let rec run_n_steps step max_depth curr_depth gterm =
         run_n_steps step max_depth (curr_depth + 1) gterm2
   )
 
-let parse_gt_and_print lexbuf oux step depth output_file =
+let parse_gt_and_run lexbuf oux step depth output_file bench =
   match Miparse.parse_groundterm_with_error lexbuf with
   | Some gterm ->
     (* fprintf oux "%s\n" (Miunparse.groundterm_to_string gterm); *)
+
+
+    let t0 = Benchmark.make 0L in
     let cg = (convert_groundterm gterm) in
     let res = run_n_steps step depth 0 (wrap_init cg) in (
+    let b = Benchmark.sub (Benchmark.make 0L) t0 in
+    if bench then (
+      fprintf stderr "Execution wall clock time: %.02f\n" (b.wall);
+      (*fprintf oux "Execution times:\n";
+      fprintf oux "%s\n" (Benchmark.to_string b);*)
+      ()
+    ) else ();
     match res with
     | (actual_depth,result) ->
       fprintf oux "Taken %d steps\n" actual_depth;
@@ -109,27 +119,37 @@ let parse_gt_and_print lexbuf oux step depth output_file =
     exit (-1)
 
 
-let run step input_filename depth output_file () =
+let run step input_filename depth output_file bench () =
   let inx = In_channel.create input_filename in
   let lexbuf = Lexing.from_channel inx in
   lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = input_filename };
-  parse_gt_and_print lexbuf stdout step depth output_file;
+  parse_gt_and_run lexbuf stdout step depth output_file bench;
   In_channel.close inx;
   ()
 
 
 (* TODO cleanup after execution *)
-let parse_first (path_to_parser : string option) input_file : string =
+let parse_first bench (path_to_parser : string option) input_file (f : string -> unit) : unit =
   match path_to_parser with
   | Some s -> (
       let astdir = (Filename_unix.temp_dir "language-interpreter" ".minuska") in
       let astfile = Filename.concat astdir "input.ast" in
       let c = (s ^ " " ^ input_file ^ " " ^ astfile) in
-      (*fprintf stderr "command: %s" c;*)
+      let t0 = Benchmark.make 0L in
       let _ = Sys_unix.command c in
-      astfile
+      let b = Benchmark.sub (Benchmark.make 0L) t0 in
+      if bench then (
+        fprintf stderr "Parsing wall clock time: %.02f\n" (b.wall);
+        (*fprintf oux "Execution times:\n";
+        fprintf oux "%s\n" (Benchmark.to_string b);*)
+        ()
+      ) else ();
+
+      (*fprintf stderr "command: %s" c;*)
+
+      (f astfile)
     )
-  | None -> input_file
+  | None -> (f input_file)
 
 let command_run (path_to_parser : string option) step =
   Command.basic
@@ -138,12 +158,13 @@ let command_run (path_to_parser : string option) step =
     (let%map_open.Command
         program = anon (("program" %: Filename_unix.arg_type)) and
         depth = flag "--depth" (required int) ~doc:"maximal number of steps to execute" and
+        bench = flag "--bench" (no_arg) ~doc:"measure the time to parse and execute the program" and
         output_file = flag "--output-file" (optional string) ~doc:"filename to put the final configuration to"
      in
-     fun () -> run step (parse_first path_to_parser program) depth output_file ())
+     fun () -> (parse_first bench path_to_parser program (fun fname -> run step fname depth output_file bench ()) ))
 
 let main (path_to_parser : string option) step =
   Printexc.record_backtrace true;
-    try (Command_unix.run ~version:"0.2" (command_run path_to_parser step)) with
+    try (Command_unix.run ~version:"0.3" (command_run path_to_parser step)) with
     | Stack_overflow -> (printf "Stack overflow.\n%s" (Printexc.get_backtrace ()));;