chore(tests/bench): rename benchmarks
This commit is contained in:
Sebastian Ullrich
parent
8a2c2ffe84
commit
9ec570416d
8 changed files with 8 additions and 141 deletions
|
|
@ -1,7 +1,7 @@
|
|||
## CONFIG
|
||||
|
||||
LEAN_BENCHES = binarytrees deriv expr_const_folding frontend qsort rbmap rbmap_checkpoint_10 rbmap_shared unionfind2
|
||||
CROSS_BENCHES = binarytrees deriv expr_const_folding qsort rbmap rbmap_checkpoint_10 rbmap_shared
|
||||
LEAN_BENCHES = binarytrees deriv const_fold frontend qsort rbmap rbmap_10 rbmap_1 unionfind
|
||||
CROSS_BENCHES = binarytrees deriv const_fold qsort rbmap rbmap_10 rbmap_1
|
||||
|
||||
LEAN_CATS = .lean .no_reuse.lean .no_borrow.lean .no_st.lean
|
||||
CROSS_CATS = .lean .gc.lean .lean.perf .hs .gc.hs .hs.perf .ml .gc.ml .ml.perf .mlton .gc.mlton .mlton.perf .mlkit .gc.mlkit .mlkit.perf
|
||||
|
|
@ -100,14 +100,13 @@ bench/qsort.%.bench: BENCH_PARAMS = 400
|
|||
|
||||
bench/rbmap.%.bench: BENCH_PARAMS = 2000000
|
||||
|
||||
rbmap_shared.%.out: rbmap_checkpoint.%.out; ln -f $< $@
|
||||
bench/rbmap_shared.%.bench: BENCH_PARAMS = 2000000 1
|
||||
rbmap_1.%.out: rbmap_checkpoint.%.out; ln -f $< $@
|
||||
bench/rbmap_1.%.bench: BENCH_PARAMS = 2000000 1
|
||||
|
||||
rbmap_checkpoint_10.%.out: rbmap_checkpoint.%.out; ln -f $< $@
|
||||
bench/rbmap_checkpoint_10.%.bench: BENCH_PARAMS = 2000000 10
|
||||
rbmap_10.%.out: rbmap_checkpoint.%.out; ln -f $< $@
|
||||
bench/rbmap_10.%.bench: BENCH_PARAMS = 2000000 10
|
||||
|
||||
bench/unionfind1.%.bench: BENCH_PARAMS = 3000000
|
||||
bench/unionfind2.%.bench: BENCH_PARAMS = 3000000
|
||||
bench/unionfind.%.bench: BENCH_PARAMS = 3000000
|
||||
|
||||
bench/%gc.lean.bench: %lean.out | bench
|
||||
ulimit -s unlimited && $(TEMCI) short exec $(TEMCI_FLAGS)\
|
||||
|
|
@ -186,7 +185,7 @@ report_cross.csv: bench_cross
|
|||
BENCHES=$(subst $(space),:,$(CROSS_BENCHES)) CATS=$(subst $(space),:,$(CROSS_CATS)) ./report.py > $@
|
||||
column -s';' -t < $@
|
||||
|
||||
TO_TEX = 's/unionfind2/unionfind/;s/expr_const_folding/const_fold/;s/rbmap_checkpoint/rbmap/;s/rbmap_shared/rbmap_1/;s/-/---/g;s/%/\\%/g;s/\.$$//g;s/(\([0-9]\)\([0-9]\))/\\ensuremath{\\tilde{\1}\\tilde{\2}}/g;s/(\([0-9]\))/\\ensuremath{\\tilde{\1}}/g;s/;/ \& /g;s/$$/\\\\/'
|
||||
TO_TEX = 's/-/---/g;s/%/\\%/g;s/\.$$//g;s/(\([0-9]\)\([0-9]\))/\\ensuremath{\\tilde{\1}\\tilde{\2}}/g;s/(\([0-9]\))/\\ensuremath{\\tilde{\1}}/g;s/;/ \& /g;s/$$/\\\\/'
|
||||
report_%.tex: report_%.csv
|
||||
tail -n +2 $< | head -n -1 | sed 's/^\([^;]\+\)/\\verb!\1!/;'$(TO_TEX) > $@
|
||||
echo -n '\midrule ' >> $@
|
||||
|
|
|
|||
|
|
@ -1,132 +0,0 @@
|
|||
def StateT' (m : Type → Type) (σ : Type) (α : Type) := (Unit × σ) → m (α × σ)
|
||||
namespace StateT'
|
||||
variables {m : Type → Type} [Monad m] {σ : Type} {α β : Type}
|
||||
@[inline] protected def pure (a : α) : StateT' m σ α := λ ⟨_, s⟩, pure (a, s)
|
||||
@[inline] protected def bind (x : StateT' m σ α) (f : α → StateT' m σ β) : StateT' m σ β := λ p, do (a, s') ← x p, f a ((), s')
|
||||
@[inline] def read : StateT' m σ σ := λ ⟨_, s⟩, pure (s, s)
|
||||
@[inline] def write (s' : σ) : StateT' m σ Unit := λ ⟨_, s⟩, pure ((), s')
|
||||
@[inline] def updt (f : σ → σ) : StateT' m σ Unit := λ ⟨_, s⟩, pure ((), f s)
|
||||
instance : Monad (StateT' m σ) :=
|
||||
{pure := @StateT'.pure _ _ _, bind := @StateT'.bind _ _ _}
|
||||
end StateT'
|
||||
|
||||
def ExceptT' (m : Type → Type) (ε : Type) (α : Type) := Except Unit Unit → m (Except ε α)
|
||||
namespace ExceptT'
|
||||
variables {m : Type → Type} [Monad m] {ε : Type} {α β : Type}
|
||||
@[inline] protected def pure (a : α) : ExceptT' m ε α :=
|
||||
λ e, match e with
|
||||
| Except.ok _ := pure (Except.ok a)
|
||||
| Except.error _ := pure (Except.ok a)
|
||||
@[inline] protected def bind (x : ExceptT' m ε α) (f : α → ExceptT' m ε β) : ExceptT' m ε β :=
|
||||
λ e, do v ← x e, match v with
|
||||
| Except.error e := pure (Except.error e)
|
||||
| Except.ok a := f a (Except.ok ())
|
||||
@[inline] def error (e : ε) : ExceptT' m ε α :=
|
||||
λ e', match e' with
|
||||
| Except.ok _ := pure (Except.error e)
|
||||
| Except.error _ := pure (Except.error e)
|
||||
@[inline] def lift (x : m α) : ExceptT' m ε α := λ e, do {a ← x, pure (Except.ok a)}
|
||||
instance : Monad (ExceptT' m ε) :=
|
||||
{pure := @ExceptT'.pure _ _ _, bind := @ExceptT'.bind _ _ _}
|
||||
end ExceptT'
|
||||
|
||||
abbreviation Node := Nat
|
||||
|
||||
structure nodeData :=
|
||||
(find : Node) (rank : Nat := 0)
|
||||
|
||||
abbreviation ufData := Array nodeData
|
||||
|
||||
abbreviation M (α : Type) := ExceptT' (StateT' Id ufData) String α
|
||||
@[inline] def read : M ufData := ExceptT'.lift StateT'.read
|
||||
@[inline] def write (s : ufData) : M Unit := ExceptT'.lift (StateT'.write s)
|
||||
@[inline] def updt (f : ufData → ufData) : M Unit := ExceptT'.lift (StateT'.updt f)
|
||||
@[inline] def error {α : Type} (e : String) : M α := ExceptT'.error e
|
||||
def run {α : Type} (x : M α) (s : ufData := ∅) : Except String α × ufData :=
|
||||
x (Except.ok ()) ((), s)
|
||||
|
||||
def capacity : M Nat :=
|
||||
do d ← read, pure d.size
|
||||
|
||||
def findEntryAux : Nat → Node → M nodeData
|
||||
| 0 n := error "out of fuel"
|
||||
| (i+1) n :=
|
||||
do s ← read,
|
||||
if h : n < s.size then
|
||||
do { let e := s.fget ⟨n, h⟩,
|
||||
if e.find = n then pure e
|
||||
else do e₁ ← findEntryAux i e.find,
|
||||
updt (λ s, s.set n e₁),
|
||||
pure e₁ }
|
||||
else error "invalid Node"
|
||||
|
||||
def findEntry (n : Node) : M nodeData :=
|
||||
do c ← capacity,
|
||||
findEntryAux c n
|
||||
|
||||
def find (n : Node) : M Node :=
|
||||
do e ← findEntry n, pure e.find
|
||||
|
||||
def mk : M Node :=
|
||||
do n ← capacity,
|
||||
updt $ λ s, s.push {find := n, rank := 1},
|
||||
pure n
|
||||
|
||||
def union (n₁ n₂ : Node) : M Unit :=
|
||||
do r₁ ← findEntry n₁,
|
||||
r₂ ← findEntry n₂,
|
||||
if r₁.find = r₂.find then pure ()
|
||||
else updt $ λ s,
|
||||
if r₁.rank < r₂.rank then s.set r₁.find { find := r₂.find }
|
||||
else if r₁.rank = r₂.rank then
|
||||
let s₁ := s.set r₁.find { find := r₂.find } in
|
||||
s₁.set r₂.find { rank := r₂.rank + 1, .. r₂}
|
||||
else s.set r₂.find { find := r₁.find }
|
||||
|
||||
|
||||
def mkNodes : Nat → M Unit
|
||||
| 0 := pure ()
|
||||
| (n+1) := mk *> mkNodes n
|
||||
|
||||
def checkEq (n₁ n₂ : Node) : M Unit :=
|
||||
do r₁ ← find n₁, r₂ ← find n₂,
|
||||
unless (r₁ = r₂) $ error "nodes are not equal"
|
||||
|
||||
def mergePackAux : Nat → Nat → Nat → M Unit
|
||||
| 0 _ _ := pure ()
|
||||
| (i+1) n d :=
|
||||
do c ← capacity,
|
||||
if (n+d) < c
|
||||
then union n (n+d) *> mergePackAux i (n+1) d
|
||||
else pure ()
|
||||
|
||||
def mergePack (d : Nat) : M Unit :=
|
||||
do c ← capacity, mergePackAux c 0 d
|
||||
|
||||
def numEqsAux : Nat → Node → Nat → M Nat
|
||||
| 0 _ r := pure r
|
||||
| (i+1) n r :=
|
||||
do c ← capacity,
|
||||
if n < c
|
||||
then do { n₁ ← find n, numEqsAux i (n+1) (if n = n₁ then r else r+1) }
|
||||
else pure r
|
||||
|
||||
def numEqs : M Nat :=
|
||||
do c ← capacity,
|
||||
numEqsAux c 0 0
|
||||
|
||||
def test (n : Nat) : M Nat :=
|
||||
if n < 2 then error "input must be greater than 1"
|
||||
else do
|
||||
mkNodes n,
|
||||
mergePack 50000,
|
||||
mergePack 10000,
|
||||
mergePack 5000,
|
||||
mergePack 1000,
|
||||
numEqs
|
||||
|
||||
def main (xs : List String) : IO UInt32 :=
|
||||
let n := xs.head.toNat in
|
||||
match run (test n) with
|
||||
| (Except.ok v, s) := IO.println ("ok " ++ toString v) *> pure 0
|
||||
| (Except.error e, s) := IO.println ("Error : " ++ e) *> pure 1
|
||||
Loading…
Add table
Reference in a new issue