diff --git a/tests/bench/Makefile b/tests/bench/Makefile index 649bbd798a..f46b9801e4 100644 --- a/tests/bench/Makefile +++ b/tests/bench/Makefile @@ -1,7 +1,7 @@ ## CONFIG -LEAN_BENCHES = binarytrees deriv const_fold parser qsort rbmap rbmap_10 rbmap_1 unionfind -CROSS_BENCHES = binarytrees deriv const_fold qsort rbmap rbmap_10 rbmap_1 +LEAN_BENCHES = binarytrees binarytrees.st deriv const_fold parser qsort rbmap rbmap_10 rbmap_1 unionfind +CROSS_BENCHES = binarytrees binarytrees.st deriv const_fold 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 .swift .gc.swift .swift.perf @@ -71,6 +71,7 @@ all: report_lean.tex report_cross.tex report binarytrees.hs: binarytrees.ghc-6.hs; ln -f $< $@ # NOTE: changed `-N4` rtsopt to `-N` to be less system-dependent binarytrees%hs.out: GHC_FLAGS += --make -O2 -XBangPatterns -dynamic -threaded -rtsopts -with-rtsopts='-N -K128M -H' +binarytrees.st%hs.out: GHC_FLAGS += --make -O2 -XBangPatterns -dynamic -rtsopts -with-rtsopts='-K128M -H' %.ml.out: %.ml $(OCAML) $(OCAML_FLAGS) $< -o $@ @@ -78,9 +79,11 @@ binarytrees%hs.out: GHC_FLAGS += --make -O2 -XBangPatterns -dynamic -threaded -r %.flambda.ml: %.ml; ln -f $< $@ binarytrees.ml: binarytrees5_multicore.ml; ln -f $< $@ +binarytrees.st.ml: binarytrees5.ml; ln -f $< $@ binarytrees%ml.out: OCAML_FLAGS += -noassert -fPIC -nodynlink -inline 100 -O3 -package domainslib -linkpkg binarytrees%ml.out: OCAML = ocamlfind ocamlopt +binarytrees.st.sml: binarytrees.st.mlton-2.sml; ln -f $< $@ %.mlton.out: %.sml $(MLTON_BIN)/mlton $(MLTON_FLAGS) -output $@ $< %.gc.mlton.out: MLTON_FLAGS = -profile time @@ -158,10 +161,12 @@ bench/%.perf.bench: %.out | bench --runner output --out $@ # no benchmarksgame versions -bench/binarytrees%mlton.bench: ; touch $@ -bench/binarytrees%mlton.perf.bench: ; touch $@ -bench/binarytrees%mlkit.bench: ; touch $@ -bench/binarytrees%mlkit.perf.bench: ; touch $@ +bench/binarytrees.mlton.bench: ; touch $@ +bench/binarytrees.gc.mlton.bench: ; touch $@ +bench/binarytrees.mlton.perf.bench: ; touch $@ +bench/binarytrees.mlkit.bench: ; touch $@ +bench/binarytrees.gc.mlkit.bench: ; touch $@ +bench/binarytrees.mlkit.perf.bench: ; touch $@ bench_lean: $(LEAN_INPUTS:%=bench/%.bench) bench_cross: $(CROSS_INPUTS:%=bench/%.bench) diff --git a/tests/bench/binarytrees.st.hs b/tests/bench/binarytrees.st.hs new file mode 100644 index 0000000000..66a1db2abc --- /dev/null +++ b/tests/bench/binarytrees.st.hs @@ -0,0 +1,66 @@ +import System.Environment +import Data.Bits +import Text.Printf +import Control.Parallel.Strategies + +-- +-- an artificially strict tree. +-- +-- normally you would ensure the branches are lazy, but this benchmark +-- requires strict allocation. +-- +data Tree = Nil | Node !Tree !Tree + +minN = 4 + +io s n t = printf "%s of depth %d\t check: %d\n" s n t + +main = do + n <- getArgs >>= readIO . head + let maxN = max (minN + 2) n + stretchN = maxN + 1 + + -- stretch memory tree + let c = check (make stretchN) + io "stretch tree" stretchN c + + -- allocate a long lived tree + let !long = make maxN + + -- allocate, walk, and deallocate many bottom-up binary trees + let vs = (depth minN maxN) + mapM_ (\((m,d,i)) -> io (show m ++ "\t trees") d i) vs + + -- confirm the long-lived binary tree still exists + io "long lived tree" maxN (check long) + +-- generate many trees +depth :: Int -> Int -> [(Int, Int, Int)] +depth d m + | d <= m = (n, d, sumT d n 0) : depth (d+2) m + | otherwise = [] + where n = 1 `shiftL` (m - d + minN) + +-- allocate and check lots of trees +sumT :: Int -> Int -> Int -> Int +sumT d 0 t = t +sumT d i t = sumT d (i-1) (t + a) + where a = check (make d) + +-- traverse the tree, counting up the nodes +check :: Tree -> Int +check t = tailCheck t 0 + +tailCheck :: Tree -> Int -> Int +tailCheck Nil !a = a +tailCheck (Node l r) !a = tailCheck l $ tailCheck r $ a + 1 + +-- build a tree +make :: Int -> Tree +make d = make' d d + +-- This function has an extra argument to suppress the +-- Common Sub-expression Elimination optimization +make' :: Int -> Int -> Tree +make' _ 0 = Node Nil Nil +make' !n d = Node (make' (n - 1) (d - 1)) (make' (n + 1) (d - 1)) diff --git a/tests/bench/binarytrees.st.lean b/tests/bench/binarytrees.st.lean new file mode 100644 index 0000000000..f28a73e3af --- /dev/null +++ b/tests/bench/binarytrees.st.lean @@ -0,0 +1,53 @@ +inductive Tree + | nil + | node (l r : Tree) +instance : Inhabited Tree := ⟨.nil⟩ + +-- This function has an extra argument to suppress the +-- common sub-expression elimination optimization +partial def make' (n d : UInt32) : Tree := + if d = 0 then .node .nil .nil + else .node (make' n (d - 1)) (make' (n + 1) (d - 1)) + +-- build a tree +def make (d : UInt32) := make' d d + +def check : Tree → UInt32 + | .nil => 0 + | .node l r => 1 + check l + check r + +def minN := 4 + +def out (s : String) (n : Nat) (t : UInt32) : IO Unit := + IO.println s!"{s} of depth {n}\t check: {t}" + +-- allocate and check lots of trees +partial def sumT (d i t : UInt32) : UInt32 := + if i = 0 then t + else + let a := check (make d) + sumT d (i-1) (t + a) + +def main : List String → IO UInt32 + | [s] => do + let n := s.toNat! + let maxN := Nat.max (minN + 2) n + let stretchN := maxN + 1 + + -- stretch memory tree + let c := check (make $ UInt32.ofNat stretchN) + out "stretch tree" stretchN c + + -- allocate a long lived tree + let long := make $ UInt32.ofNat maxN + + -- allocate, walk, and deallocate many bottom-up binary trees + for d in [minN:maxN+1:2] do + let n := 2 ^ (maxN - d + minN) + let i := sumT (.ofNat d) (.ofNat n) 0 + out s!"{n}\t trees" d i + + -- confirm the long-lived binary tree still exists + out "long lived tree" maxN (check long) + return 0 + | _ => return 1 diff --git a/tests/bench/binarytrees.st.mlton-2.sml b/tests/bench/binarytrees.st.mlton-2.sml index d5b7a53791..4008e49528 100644 --- a/tests/bench/binarytrees.st.mlton-2.sml +++ b/tests/bench/binarytrees.st.mlton-2.sml @@ -1,4 +1,5 @@ (* from https://smlnj-gitlab.cs.uchicago.edu/manticore/benchmarks/blob/master/benchmarks/programs/shootout-binarytrees/binarytrees.mlton-2.sml *) +(* adjusted to match computation of other versions *) (* binarytrees.mlton * * The Computer Language Shootout @@ -9,24 +10,22 @@ * Optimized and compressed by Vesa Karvonen. * De-optimized by Isaac Gouy *) -datatype 'a tree = Nil | Node of 'a tree * 'a * 'a tree -(* fun mk 0 i = Nil | mk d i = Node (mk (d-1) (i*2-1), i, mk (d-1) (i*2)) *) -fun mk 0 i = Node (Nil, i, Nil) | mk d i = Node (mk (d-1) (i*2-1), i, mk (d-1) (i*2)) -fun chk Nil = 0 | chk (Node (l, i, r)) = i + chk l - chk r +datatype tree = Nil | Node of tree * tree +fun mk 0 = Node (Nil, Nil) | mk d = Node (mk (d-1), mk (d-1)) +fun chk Nil = 0 | chk (Node (l, r)) = 1 + chk l + chk r val n = valOf (Int.fromString (hd (CommandLine.arguments ()))) handle _ => 10 val min' = 4 val max' = Int.max (min' + 2, n) val stretch' = max' + 1 -val i2s = String.translate (fn #"~" => "-" | c => str c) o Int.toString -fun msg h d t = app print [h, Int.toString d, "\t check: ", i2s t, "\n"] -val () = msg "stretch tree of depth " stretch' (chk (mk stretch' 0)) -val longLivedTree = mk max' 0 +fun msg h d t = app print [h, Int.toString d, "\t check: ", Int.toString t, "\n"] +val () = msg "stretch tree of depth " stretch' (chk (mk stretch')) +val longLivedTree = mk max' fun loopDepths d = if d > max' then () else let val n = Word.toInt (Word.<< (0w1, Word.fromInt (max'-d+min'))) - fun lp (i, c) = if i=n then c - else lp (i+1, c + chk (mk d i) + chk (mk d (~i))) - in msg (Int.toString (2*n)^"\t trees of depth ") d (lp (0, 0)) + fun lp (i, c) = if i>n then c + else lp (i+1, c + chk (mk d)) + in msg (Int.toString n^"\t trees of depth ") d (lp (1, 0)) ; loopDepths (d + 2) end val () = loopDepths min' val () = msg "long lived tree of depth " max' (chk longLivedTree) diff --git a/tests/bench/binarytrees.st.sml b/tests/bench/binarytrees.st.sml new file mode 100644 index 0000000000..4008e49528 --- /dev/null +++ b/tests/bench/binarytrees.st.sml @@ -0,0 +1,31 @@ +(* from https://smlnj-gitlab.cs.uchicago.edu/manticore/benchmarks/blob/master/benchmarks/programs/shootout-binarytrees/binarytrees.mlton-2.sml *) +(* adjusted to match computation of other versions *) +(* binarytrees.mlton + * + * The Computer Language Shootout + * http://shootout.alioth.debian.org/ + * + * Contributed by Troestler Christophe + * Ported to MLton/SML by sweeks@sweeks.com. + * Optimized and compressed by Vesa Karvonen. + * De-optimized by Isaac Gouy + *) +datatype tree = Nil | Node of tree * tree +fun mk 0 = Node (Nil, Nil) | mk d = Node (mk (d-1), mk (d-1)) +fun chk Nil = 0 | chk (Node (l, r)) = 1 + chk l + chk r +val n = valOf (Int.fromString (hd (CommandLine.arguments ()))) handle _ => 10 +val min' = 4 +val max' = Int.max (min' + 2, n) +val stretch' = max' + 1 +fun msg h d t = app print [h, Int.toString d, "\t check: ", Int.toString t, "\n"] +val () = msg "stretch tree of depth " stretch' (chk (mk stretch')) +val longLivedTree = mk max' +fun loopDepths d = + if d > max' then () + else let val n = Word.toInt (Word.<< (0w1, Word.fromInt (max'-d+min'))) + fun lp (i, c) = if i>n then c + else lp (i+1, c + chk (mk d)) + in msg (Int.toString n^"\t trees of depth ") d (lp (1, 0)) + ; loopDepths (d + 2) end +val () = loopDepths min' +val () = msg "long lived tree of depth " max' (chk longLivedTree) diff --git a/tests/bench/binarytrees.st.swift b/tests/bench/binarytrees.st.swift new file mode 100644 index 0000000000..b6b2ee68c6 --- /dev/null +++ b/tests/bench/binarytrees.st.swift @@ -0,0 +1,64 @@ +// see binarytrees.swift for original + +import Dispatch +import Foundation + +class TreeNode { + var left, right: TreeNode? + + init(left: TreeNode?, right: TreeNode?) { + self.left = left + self.right = right + } + + func check() -> Int { + if left != nil { + return left!.check() + right!.check() + 1 + } else { + return 1 + } + } +} + +func createTree(_ depth: Int) -> TreeNode? { + if depth > 0 { + let node = TreeNode(left: createTree(depth-1), + right: createTree(depth-1)) + return node + } else { + let node = TreeNode(left: nil, right: nil) + return node + } +} + +let n: Int +if CommandLine.argc > 1 { + n = Int(CommandLine.arguments[1]) ?? 10 +} else { + n = 10 +} +let minDepth = 4 +let maxDepth = (n > minDepth + 2) ? n : minDepth + 2 + +// Create big tree in first pool +let tree = createTree(maxDepth+1) +let check = tree!.check() +print("stretch tree of depth \(maxDepth+1)\t check: \(check)") + +// Cleal first pool and allocate long living tree +let longLivingTree = createTree(maxDepth) + +// Allocate binary trees of increasing depth up to maxDepth depth +for currentDepth in stride(from: minDepth, through: maxDepth, by: 2) { + let iterations = 1 << (maxDepth - currentDepth + minDepth) + var totalChecksum = 0 + for _ in 1...iterations { + let tree1 = createTree(currentDepth) + totalChecksum += tree1!.check() + } + print("\(iterations)\t trees of depth \(currentDepth)\t check: \(totalChecksum)") +} + +// Check long living tree and print out check info +print("long lived tree of depth \(maxDepth)\t check: \(longLivingTree!.check())") + diff --git a/tests/bench/binarytrees5.ml b/tests/bench/binarytrees5.ml new file mode 100644 index 0000000000..4f3c54aa4c --- /dev/null +++ b/tests/bench/binarytrees5.ml @@ -0,0 +1,44 @@ +(* The Computer Language Benchmarks Game + * https://salsa.debian.org/benchmarksgame-team/benchmarksgame/ + * + * Contributed by Troestler Christophe + * Modified by Fabrice Le Fessant + * *reset* + *) + +type 'a tree = Empty | Node of 'a tree * 'a tree + +let rec make d = +(* if d = 0 then Empty *) + if d = 0 then Node(Empty, Empty) + else let d = d - 1 in Node(make d, make d) + +let rec check = function Empty -> 0 | Node(l, r) -> 1 + check l + check r + +let min_depth = 4 +let max_depth = (let n = try int_of_string(Array.get Sys.argv 1) with _ -> 10 in + max (min_depth + 2) n) +let stretch_depth = max_depth + 1 + +let () = + (* GC param suggestion: + Gc.set { (Gc.get()) with Gc.minor_heap_size = 1024 * 1024; max_overhead = -1; }; *) + let c = check (make stretch_depth) in + Printf.printf "stretch tree of depth %i\t check: %i\n" stretch_depth c + +let long_lived_tree = make max_depth + +let rec loop_depths d = + for i = 0 to ((max_depth - d) / 2 + 1) - 1 do + let d = d + i * 2 in + let niter = 1 lsl (max_depth - d + min_depth) in + let c = ref 0 in + for i = 1 to niter do c := !c + check(make d) done; + Printf.printf "%i\t trees of depth %i\t check: %i\n" niter d !c; + done + +let () = + flush stdout; + loop_depths min_depth; + Printf.printf "long lived tree of depth %i\t check: %i\n" + max_depth (check long_lived_tree) diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml index a45e0e25fc..6e8cf8baeb 100644 --- a/tests/bench/speedcenter.exec.velcom.yaml +++ b/tests/bench/speedcenter.exec.velcom.yaml @@ -80,6 +80,14 @@ cmd: ./binarytrees.lean.out 21 build_config: cmd: ./compile.sh binarytrees.lean +- attributes: + description: binarytrees.st + tags: [fast, suite] + run_config: + <<: *time + cmd: ./binarytrees.st.lean.out 21 + build_config: + cmd: ./compile.sh binarytrees.st.lean - attributes: description: const_fold tags: [fast, suite]