Improve benchmark programs and Makefile

.github/workflows/docker-action.yml

@@ -27,7 +27,12 @@ jobs:
           - 'mathcomp/mathcomp:1.13.0-coq-8.13'
           - 'mathcomp/mathcomp:1.13.0-coq-8.14'
           - 'mathcomp/mathcomp:1.13.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.13.0-coq-dev'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.11'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.12'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.13'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.14'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.15'
+          - 'mathcomp/mathcomp:1.14.0-coq-dev'
           - 'mathcomp/mathcomp-dev:coq-8.11'
           - 'mathcomp/mathcomp-dev:coq-8.12'
           - 'mathcomp/mathcomp-dev:coq-8.13'

.gitignore

@@ -13,8 +13,10 @@ Make*.coq.conf
 # OCaml
 _build
 benchmark/ocaml/benchmark.native
+benchmark/ocaml/benchmark_exp.native
 
 # Haskell
 *.hi
 *.o
 benchmark/haskell/Benchmark
+benchmark/haskell/BenchmarkExp

Makefile.benchmark.coq.local

@@ -1,43 +1,70 @@
+# Workaround for the issue that building the benchmark programs require two
+# versions of OCaml.
+OCAML_OPAMSWITCH?=
+ifeq (,$(OCAML_OPAMSWITCH))
+OCAMLBUILD?= ocamlbuild
+else
+OCAMLBUILD?= opam exec --switch $(OCAML_OPAMSWITCH) -- ocamlbuild
+endif
+
+HSDIR := benchmark/haskell
+MLDIR := benchmark/ocaml
+
 EXTRACTED_HS_FILES := \
-  benchmark/haskell/MergesortCoqCbn.hs \
-  benchmark/haskell/MergesortCoqCbnAcc.hs \
-  benchmark/haskell/MergesortCoqCbv.hs \
-  benchmark/haskell/MergesortCoqCbvAcc.hs
+  $(HSDIR)/MergesortCoqCbn.hs \
+  $(HSDIR)/MergesortCoqCbnAcc.hs \
+  $(HSDIR)/MergesortCoqCbv.hs \
+  $(HSDIR)/MergesortCoqCbvAcc.hs
+
+HS_FLAGS := -with-rtsopts="-T -I0 -A8G -G1 -m1" -O2
 
 EXTRACTED_ML_FILES := \
-  benchmark/ocaml/mergesort_coq_cbn.ml \
-  benchmark/ocaml/mergesort_coq_cbnacc.ml \
-  benchmark/ocaml/mergesort_coq_cbv.ml \
-  benchmark/ocaml/mergesort_coq_cbvacc.ml
+  $(MLDIR)/mergesort_coq_cbn.ml \
+  $(MLDIR)/mergesort_coq_cbnacc.ml \
+  $(MLDIR)/mergesort_coq_cbv.ml \
+  $(MLDIR)/mergesort_coq_cbvacc.ml \
+  $(MLDIR)/mergesort_coq_cbn_tmc.ml \
+  $(MLDIR)/mergesort_coq_cbnacc_tmc.ml
 
-HS_FILES := $(EXTRACTED_HS_FILES) benchmark/haskell/Benchmark.hs
+ML_FLAGS := -cflags -w,a -verbose 0 -package unix -tag 'optimize(3)'
 
-ML_FILES := $(EXTRACTED_ML_FILES) benchmark/ocaml/benchmark.ml
+EXTRACTED_BINARIES := $(HSDIR)/Benchmark $(HSDIR)/BenchmarkExp \
+  $(MLDIR)/benchmark.native $(MLDIR)/benchmark_exp.native
 
-EXTRACTED_BINARIES := \
-  benchmark/haskell/Benchmark \
-  benchmark/ocaml/benchmark.native
+$(HSDIR)/Benchmark: $(HSDIR)/Benchmark.hs $(HSDIR)/Benchlib.hs \
+                    $(EXTRACTED_HS_FILES)
+	cd $(HSDIR) && stack ghc Benchmark.hs -- $(HS_FLAGS)
 
-benchmark/haskell/Benchmark: $(HS_FILES)
-	cd benchmark/haskell && \
-	  stack ghc Benchmark.hs -- -with-rtsopts="-T -I0 -A8G -G1 -m1" -O2
+$(HSDIR)/BenchmarkExp: $(HSDIR)/BenchmarkExp.hs $(HSDIR)/Benchlib.hs \
+                       $(EXTRACTED_HS_FILES)
+	cd $(HSDIR) && stack ghc BenchmarkExp.hs -- $(HS_FLAGS)
 
-benchmark/ocaml/benchmark.native: $(ML_FILES)
-	cd benchmark/ocaml && \
-	  ocamlbuild benchmark.native -package unix -tag 'optimize(3)'
+$(MLDIR)/benchmark.native: $(MLDIR)/benchmark.ml $(MLDIR)/benchlib.ml \
+                           $(EXTRACTED_ML_FILES) $(EXTRACTED_ML_FILES:.ml=.mli)
+	cd $(MLDIR) && $(OCAMLBUILD) benchmark.native $(ML_FLAGS)
 
-benchmark/haskell/MergesortCoqCbn.hs benchmark/ocaml/mergesort_coq_cbn.ml: \
+$(MLDIR)/benchmark_exp.native: $(MLDIR)/benchmark_exp.ml $(MLDIR)/benchlib.ml \
+                               $(EXTRACTED_ML_FILES) $(EXTRACTED_ML_FILES:.ml=.mli)
+	cd $(MLDIR) && $(OCAMLBUILD) benchmark_exp.native $(ML_FLAGS)
+
+$(HSDIR)/MergesortCoqCbn.hs $(MLDIR)/mergesort_coq_cbn.ml: \
     benchmark/extraction_cbn.vo
 
-benchmark/haskell/MergesortCoqCbnAcc.hs benchmark/ocaml/mergesort_coq_cbnacc.ml: \
+$(HSDIR)/MergesortCoqCbnAcc.hs $(MLDIR)/mergesort_coq_cbnacc.ml: \
     benchmark/extraction_cbnacc.vo
 
-benchmark/haskell/MergesortCoqCbv.hs benchmark/ocaml/mergesort_coq_cbv.ml: \
+$(HSDIR)/MergesortCoqCbv.hs $(MLDIR)/mergesort_coq_cbv.ml: \
     benchmark/extraction_cbv.vo
 
-benchmark/haskell/MergesortCoqCbvAcc.hs benchmark/ocaml/mergesort_coq_cbvacc.ml: \
+$(HSDIR)/MergesortCoqCbvAcc.hs $(MLDIR)/mergesort_coq_cbvacc.ml: \
     benchmark/extraction_cbvacc.vo
 
+$(MLDIR)/%_tmc.ml: $(MLDIR)/%.ml $(MLDIR)/%_tmc.patch
+	patch $^ -o $@
+
+$(MLDIR)/%_tmc.mli: $(MLDIR)/%.mli
+	cp $< $@
+
 post-all:: $(EXTRACTED_BINARIES)
 
 clean::

README.md

@@ -45,7 +45,7 @@ by providing a lemma corresponding to the binary tree construction.
 - Compatible Coq versions: 8.10 or later
 - Additional dependencies:
   - [MathComp](https://math-comp.github.io) 1.12.0 or later
-  - [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.2 or later
+  - [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later
 - Coq namespace: `stablesort`
 - Related publication(s): none
 

benchmark/benchmark.v

@@ -86,9 +86,9 @@ time-median N P Time Words :- !, time-median-rec N P [] [] Time Words.
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 pred benchmark-case
-  i:string, i:(term -> term -> term -> prop),
-  i:list (pair string term), i:term, i:int, o:list string, o:list string.
-benchmark-case RedStr Red Config Preproc Size TS MS :- std.do! [
+  i:string, i:(term -> term -> term -> prop), i:int, i:list (pair string term),
+  i:term, i:term, i:int, o:list string, o:list string.
+benchmark-case RedStr Red MedianOf Config Preproc SizeC Size TS MS :- std.do! [
   coq.env.begin-section "Sec",
   coq.reduction.vm.norm
     (app [Preproc, {random-N-list Size Size}]) {{ list N }} Input,
@@ -98,55 +98,50 @@ benchmark-case RedStr Red Config Preproc Size TS MS :- std.do! [
       Red (global (const C)) _ _)
      (@local! => coq.env.add-const "input" Input {{ list N }} @transparent! C),
   std.map Config
-    (c\ r\ sigma Name Func Comp CompTy Time Words Mem TStr MStr\ std.do! [
-      c = pr Name Func,
-      Comp = {{ lp:Func lp:{{ global (const C) }} }},
-      std.assert-ok! (coq.typecheck Comp CompTy) "bad term",
-      time-median 5 (Red Comp CompTy _) Time Words,
-      std.any->string Time TStr,
-      Mem is Words / (128.0 * 1024.0), % memory consumption in MBs
-      std.any->string Mem MStr,
-      r is triple Name TStr MStr
-    ]) RS,
+    (c\ r\ sigma Name Func Comp SimplComp CompTy Time Words Mem TStr MStr\
+      std.do! [
+        c = pr Name Func,
+        Comp = {{ lp:Func lp:SizeC lp:{{ global (const C) }} }},
+        std.assert-ok! (coq.typecheck Comp CompTy) "bad term",
+        hd-beta-zeta-reduce Comp SimplComp,
+        time-median MedianOf (Red SimplComp CompTy _) Time Words,
+        std.any->string Time TStr,
+        Mem is Words / (128.0 * 1024.0), % memory consumption in MBs
+        std.any->string Mem MStr,
+        r is triple Name TStr MStr
+      ]) RS,
   std.any->string Size SizeStr,
   Str is RedStr ^ ", size: " ^ SizeStr ^ "; " ^
          {std.string.concat "; "
             {std.map RS (r\ s\ sigma Name TStr MStr\
                r = triple Name TStr MStr,
                s is Name ^ ": " ^ TStr ^ "s, " ^ MStr ^ "MB")} },
   coq.say Str,
-  std.map RS (r\ s\ sigma Name TStr MStr\
-    r = triple Name TStr MStr,
-    s is "(" ^ SizeStr ^ ", " ^ TStr ^ ")"
-  ) TS,
-  std.map RS (r\ s\ sigma Name TStr MStr\
-    r = triple Name TStr MStr,
-    s is "(" ^ SizeStr ^ ", " ^ MStr ^ ")"
-  ) MS,
+  std.map RS (r\ s\ r = triple _ s _) TS,
+  std.map RS (r\ s\ r = triple _ _ s) MS,
   coq.env.end-section
 ].
 
 pred benchmark
-  i:string, i:(term -> term -> term -> prop), i:list (pair string term),
+  i:string, i:(term -> term -> term -> prop), i:int, i:list (pair string term),
   i:term, i:term, o:list (list string), o:list (list string).
-benchmark RedStr Red Config Preproc Size TSS MSS :- !,
-  benchmark_aux RedStr Red Config Preproc
+benchmark RedStr Red MedianOf Config Preproc Size TSS MSS :- !,
+  benchmark_aux RedStr Red MedianOf Config Preproc
                 {coq.reduction.lazy.whd_all Size} TSS MSS.
 
 pred benchmark_aux
-  i:string, i:(term -> term -> term -> prop), i:list (pair string term),
+  i:string, i:(term -> term -> term -> prop), i:int, i:list (pair string term),
   i:term, i:term, o:list (list string), o:list (list string).
-benchmark_aux _ _ Config _ {{ @nil _ }} SS SS :- !,
-  std.map Config (_\ r\ r = []) SS.
-benchmark_aux RedStr Red Config Preproc
-              {{ @cons _ lp:SizeH lp:Size }} TSS' MSS' :- std.do! [
-  n-constant SizeH' {coq.reduction.cbv.norm SizeH},
-  benchmark-case RedStr Red Config Preproc SizeH' TS MS,
-  benchmark RedStr Red Config Preproc Size TSS MSS,
-  std.map2 TS TSS (t\ ts\ ts'\ ts' = [t|ts]) TSS',
-  std.map2 MS MSS (m\ ms\ ms'\ ms' = [m|ms]) MSS'
+benchmark_aux _ _ _ _ _ {{ @nil _ }} [] [] :- !.
+benchmark_aux RedStr Red MedianOf Config Preproc {{ @cons _ lp:SizeH lp:Size }}
+              [[SizeHStr|TS]|TSS] [[SizeHStr|MS]|MSS] :- std.do! [
+  coq.reduction.cbv.norm SizeH SizeH',
+  n-constant SizeH'' SizeH',
+  std.any->string SizeH'' SizeHStr,
+  benchmark-case RedStr Red MedianOf Config Preproc SizeH' SizeH'' TS MS,
+  benchmark RedStr Red MedianOf Config Preproc Size TSS MSS
 ].
-benchmark_aux _ _ _ _ _ _ _ :-
+benchmark_aux _ _ _ _ _ _ _ _ :-
   coq.error "benchmark_aux: the head symbol of Size is not a constructor".
 
 pred get-reduction-machine i:string, o:(term -> term -> term -> prop).
@@ -155,50 +150,56 @@ get-reduction-machine "lazy" Red :- !,
 get-reduction-machine "compute"  Red :- !,
   Red = t\ _\ tred\ coq.reduction.cbv.norm t tred.
 get-reduction-machine "vm_compute" coq.reduction.vm.norm :- !.
-get-reduction-machine "native_compute" coq.reduction.native.norm :- !,
-  coq.reduction.native.available?.
+get-reduction-machine "native_compute" coq.reduction.native.norm :-
+  coq.reduction.native.available?, !.
+get-reduction-machine M _ :-
+  coq.error "Reduction machine" M "is not available".
 
 pred parse-config i:list argument, o: list (pair string term).
 parse-config [] [] :- !.
 parse-config [str Name, trm Func | ConfList] [pr Name Func | Conf] :- !,
   parse-config ConfList Conf.
 parse-config _ _ :- coq.error "ill-formed arguments".
 
-main [str FileName, str RedStr, trm Size, trm Preproc | ConfList] :- std.do! [
+main [str FileName, str RedStr, int MedianOf, trm Size, trm Preproc |
+      ConfList] :- std.do! [
   std.assert-ok! (coq.typecheck Size {{ seq N }}) "bad term",
   std.assert-ok! (coq.typecheck Preproc {{ seq N -> seq N }}) "bad term",
   parse-config ConfList Config,
-  % enlarge the minor heap to 4GB
+  % enlarge the minor heap to 16GB
   gc.get Minor _ _ _ _ _ _ _,
-  gc.set {calc (512 * 1024 * 1024)} _ _ _ _ _ _ _,
+  gc.set {calc (2 * 1024 * 1024 * 1024)} _ _ _ _ _ _ _,
   % benchmark
-  benchmark RedStr {get-reduction-machine RedStr} Config Preproc Size TSS MSS,
+  benchmark RedStr {get-reduction-machine RedStr} MedianOf Config Preproc Size
+            TSS MSS,
   % restore the initial size of the minor heap
   gc.set Minor _ _ _ _ _ _ _,
   % pgfplot
-  open_out {calc (FileName ^ ".time.out")} TStream,
-  output TStream "% time consumption\n",
-  std.forall TSS (ts\ sigma Str\
-    output TStream "\\addplot coordinates {",
-    std.string.concat " " ts Str,
-    output TStream Str,
-    output TStream "};\n"),
-  output TStream "\\legend{",
-  output TStream
-    {std.string.concat ", " {std.map Config (c\ n\ sigma T\ c = pr n T)} },
-  output TStream "}\n",
+  open_out {calc (FileName ^ ".time.csv")} TStream,
+  output TStream "Size",
+  std.forall Config (conf\ sigma Name\
+    conf = pr Name _,
+    output TStream ", ",
+    output TStream Name),
+  output TStream "\n",
+  std.forall TSS (ts\ sigma T TS\
+    ts = [T|TS],
+    output TStream T,
+    std.forall TS (t\ output TStream ", ", output TStream t),
+    output TStream "\n"),
   close_out TStream,
-  open_out {calc (FileName ^ ".mem.out")} MStream,
-  output MStream "% memory consumption\n",
-  std.forall MSS (ms\ sigma Str\
-    output MStream "\\addplot coordinates {",
-    std.string.concat " " ms Str,
-    output MStream Str,
-    output MStream "};\n"),
-  output MStream "\\legend{",
-  output MStream
-    {std.string.concat ", " {std.map Config (c\ n\ sigma T\ c = pr n T)} },
-  output MStream "}\n",
+  open_out {calc (FileName ^ ".mem.csv")} MStream,
+  output MStream "Size",
+  std.forall Config (conf\ sigma Name\
+    conf = pr Name _,
+    output MStream ", ",
+    output MStream Name),
+  output MStream "\n",
+  std.forall MSS (ms\ sigma M MS\
+    ms = [M|MS],
+    output MStream M,
+    std.forall MS (m\ output MStream ", ", output MStream m),
+    output MStream "\n"),
   close_out MStream
 ].
 main _ :- !, coq.error "ill-formed arguments".
@@ -209,13 +210,11 @@ Elpi Typecheck.
 Definition N_iota (n m : N) : seq N :=
   N.iter m (fun f n => n :: f (N.succ n)) (fun => [::]) n.
 
-Definition lazy_bench
-  (sort : forall T : Type, rel T -> seq T -> seq T) (xs : seq N) :=
-  sorted N.leb (take 10 (sort _ N.leb xs)).
+Notation lazy_bench sort :=
+  (fun n xs => sorted N.leb (take 10 (sort _ N.leb xs))).
 
-Definition eager_bench
-  (sort : forall T : Type, rel T -> seq T -> seq T) (xs : seq N) :=
-  sorted N.leb (sort _ N.leb xs).
+Notation eager_bench sort :=
+  (fun n xs => sorted N.leb (sort _ N.leb xs)).
 
 Fixpoint sort_blocks (T : Type) (leT : rel T) (n : nat) (xs : seq T) :=
   if xs is x :: xs' then

benchmark/benchmark_compute.v

@@ -5,7 +5,7 @@ From benchmark Require Import benchmark.
 
 Elpi sort_benchmark
   "compute1" "compute"
-  (map (N.mul 100) (N_iota 1 40)) (id)
+  5 (map (N.mul 100) (N_iota 1 40)) (id)
   "CBN.sort1"    (eager_bench CBN.sort1)
   "CBN.sort2"    (eager_bench CBN.sort2)
   "CBN.sort3"    (eager_bench CBN.sort3)
@@ -25,7 +25,7 @@ Elpi sort_benchmark
 
 Elpi sort_benchmark
   "compute2" "compute"
-  (map (N.mul 100) (N_iota 1 40)) (sort_blocks N.leb 50)
+  5 (map (N.mul 100) (N_iota 1 40)) (sort_blocks N.leb 50)
   "CBN.sort1"    (eager_bench CBN.sort1)
   "CBN.sort2"    (eager_bench CBN.sort2)
   "CBN.sort3"    (eager_bench CBN.sort3)

benchmark/benchmark_exp_compute.v

@@ -0,0 +1,24 @@
+From Coq Require Import NArith List.
+From mathcomp Require Import all_ssreflect.
+From stablesort Require Import stablesort.
+From benchmark Require Import benchmark.
+
+Elpi sort_benchmark
+  "compute-total-random" "compute"
+  9 (map (N.pow 2) (N_iota 3 10)) (id)
+  "CBN.sort2"    (eager_bench CBN.sort2)
+  "CBN.sort3"    (eager_bench CBN.sort3)
+  "CBN.sortN"    (eager_bench CBN.sortN)
+  "CBV.sort2"    (eager_bench CBV.sort2)
+  "CBV.sort3"    (eager_bench CBV.sort3)
+  "CBV.sortN"    (eager_bench CBV.sortN).
+
+Elpi sort_benchmark
+  "compute-total-smooth" "compute"
+  9 (map (N.pow 2) (N_iota 3 10)) (sort_blocks N.leb 50)
+  "CBN.sort2"    (eager_bench CBN.sort2)
+  "CBN.sort3"    (eager_bench CBN.sort3)
+  "CBN.sortN"    (eager_bench CBN.sortN)
+  "CBV.sort2"    (eager_bench CBV.sort2)
+  "CBV.sort3"    (eager_bench CBV.sort3)
+  "CBV.sortN"    (eager_bench CBV.sortN).