diff --git a/examples-hybrid/test.sh b/examples-hybrid/test.sh index a638c148..23fa5742 100755 --- a/examples-hybrid/test.sh +++ b/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 diff --git a/examples-standalone/README.md b/examples-standalone/README.md new file mode 100644 index 00000000..82bb9b22 --- /dev/null +++ b/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. + + + + + diff --git a/examples-standalone/test.sh b/examples-standalone/test.sh index 41e29d0b..4be4ca2d 100755 --- a/examples-standalone/test.sh +++ b/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 diff --git a/flake.nix b/flake.nix index 9b641254..06757645 100644 --- a/flake.nix +++ b/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" ''; diff --git a/minuska/coq-minuska.opam b/minuska/coq-minuska.opam index c01b1d29..72af1356 100644 --- a/minuska/coq-minuska.opam +++ b/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" diff --git a/minuska/dune-project b/minuska/dune-project index e7706514..6df31b98 100644 --- a/minuska/dune-project +++ b/minuska/dune-project @@ -21,6 +21,7 @@ (package (name coq-minuska) (depends + benchmark coq menhir core diff --git a/minuska/lib/dune b/minuska/lib/dune index 07300568..3e80b9bc 100644 --- a/minuska/lib/dune +++ b/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 diff --git a/minuska/lib/miskeleton.ml b/minuska/lib/miskeleton.ml index be7bae8e..671e0ed1 100644 --- a/minuska/lib/miskeleton.ml +++ b/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 ()));;