bench

Benchmarks, run by heff bench, as Go’s testing.B runs them.

A benchmark is a top-level definition of type Bench, found by its type as a test is, and named by its groups’ names and its own. Its body is given a count, n, and does the work measured n times; heff bench runs it with 1, then with a count predicted from the run before, until a run takes the bench time (a second, --time), and says the last run: its count, and per time it did the work, its nanoseconds, the bytes it made and how many objects.

import bench as Bench

fib : Int -> Int fib n = if n < 2 then n else fib (n - 1) + fib (n - 2)

fibs : Bench.Bench fibs = Bench.group “fib” [ Bench.bench “10” (\n -> Bench.times n (\i -> fib (Bench.keep 10))) , Bench.bench “20” (\n -> Bench.times n (\i -> fib (Bench.keep 20))) ]

The work’s result is kept (times keeps each, keep one): the compiler drops what is computed and never used, and computes once what is made of what it knows — fib 20 is the same each time, but fib (keep 20) is computed each time, as keep 20 is not known. What a body does before its \n -> is done once, when the benchmark is made, not measured. A body may check what it computed (check’s assert, failure, skip): a run that fails ends the benchmark, which heff bench says failed.

heff bench builds a file’s benchmarks into a program through C, at heff install’s level (benchMain), its objects counted as they are made, and runs each benchmark in it.

keep

keep : {a : Type} -> a -> a

The value, as it is; but no pass of the compiler, nor the C compiler after it, knows what it is, nor drops it, its result unused: what a benchmark’s work is kept by, which the compiler would otherwise drop, its result unused, or compute once, what it is made of known. times keeps each result; keep the work’s arguments too (fib (keep 20), not computed once). It costs nothing: no instruction.

>>> keep 20 + 1
21

Ran

data Ran = RanThrough | RanFailed Check.Failure | RanSkipped String

What came of a run of a benchmark: it went through, it failed (why), or it was skipped (why: what it needs is not there).

Sample

data Sample = MkSample Int Int Int

What a run took: its nanoseconds, and the objects it made and their bytes (0 where they are not counted, not built by heff bench).

TimerF

data TimerF (m : Type -> Type) x
  = StartTimer Int (Int -> x)
  | StopTimer Ran (Sample -> x)

The timer, the world’s (its provider’s, in C): started with the run’s count, which it gives back, so that the work made of it comes after; stopped with what came of the run, so that the work comes before — what the run took.

timer

timer : HFunctor

For timing a benchmark: a timer started before a run and stopped after it, the run’s sample.

startTimer

startTimer : {e : HFunctor} -> {{tm : timer <: e}} -> Int -> Co e Int

The timer started, for a run of this count: the count, given back.

stopTimer

stopTimer : {e : HFunctor} -> {{tm : timer <: e}} -> Ran -> Co e Sample

The timer stopped, the run come to this: what it took.

Bench

data Bench
  = Benchmark String (Int -> Co Check.check Unit)
  | Group String (List Bench)

A benchmark: its body, given the count, in checking’s effect; or benchmarks under a name.

bench

bench : String
      -> ({e : HFunctor} -> {{chk : Check.check <: e}} -> Int -> Co e Unit)
      -> Bench

A benchmark: its body does the work as many times as it is given, and may check what it computed. What it does before its \n -> is done once, when the benchmark is made.

group

group : String -> List Bench -> Bench

Benchmarks under a name.

times

times : {a : Type} -> {e : HFunctor} -> Int -> (Int -> a) -> Co e Unit

The work done n times, f 0 to f (n - 1), each result kept: a benchmark’s body, as Go’s for i := 0; i < b.N; i++.

Step

data Step a = Goes a | Ends Ran

A run, as far as it went: going on, or ended (failed, skipped).

checker

checker : Handler Check.check

Checking, as a benchmark is run: a failure ends the run, as a skip does; a label and a note are passed over.

ranOf

ranOf : Step Unit -> Ran

runOnce

runOnce : {e : HFunctor}
        -> {{tm : timer <: e}}
        -> (Int -> Co Check.check Unit)
        -> Int
        -> Co e (Ran, Sample)

A run of the body, of this count, timed: the timer started, the body run on the count it gives back, and stopped with what came of it.

Goal

data Goal = ForNanos Int | ForCount Int

How long a benchmark is run: until a run takes these nanoseconds, its count grown; or once, of this count (Go’s -benchtime 100x).

Measured

data Measured = MeasuredAt Int Sample | Unmeasured Ran

What came of a benchmark: its last run’s count and what it took, or a run that did not go through.

maxCount

maxCount : Int

the most a run counts: a billion, as Go’s

grownTo

grownTo : Int -> Int -> Int

nextCount

nextCount : Int -> Int -> Int -> Int

The count of the next run, as Go predicts it: the goal over what the last took per time, a fifth more — but a hundred times the last at most, one more at least, and a billion at most.

>>> nextCount 1000000000 1 1000
100
>>> nextCount 1000000000 100 1000000
10000
>>> nextCount 1000000000 10000 50000000
240000
>>> nextCount 1000000000 500000000 900000000
666666666
>>> nextCount 1000000000 7 0
700

grow

grow : {e : HFunctor}
     -> {{tm : timer <: e}}
     -> Int
     -> (Int -> Co Check.check Unit)
     -> Int
     -> (Ran, Sample)
     -> Co e Measured

measuredOf

measuredOf : Int -> (Ran, Sample) -> Measured

measure

measure : {e : HFunctor}
        -> {{tm : timer <: e}}
        -> Goal
        -> (Int -> Co Check.check Unit)
        -> Co e Measured

A benchmark measured, as Go measures one: run once, then again, its count grown, until a run takes the goal (or of the count given).

benchmarksUnder

benchmarksUnder : List String
                -> Bench
                -> List (List String, Int -> Co Check.check Unit)

Each benchmark under these groups, by its names, its groups’ and its own, and its body.

benchmarksOf

benchmarksOf : List Bench -> List (List String, Int -> Co Check.check Unit)

selectedNames

selectedNames : List Regex.Regex -> List Bench -> List (List String)

The names of each benchmark the levels of a pattern select, as heff test --run selects tests (check’s selectedBy).

sameNames

sameNames : List String -> List String -> Bool

benchmarkNamed

benchmarkNamed : List String -> List Bench -> Maybe (Int -> Co Check.check Unit)

the benchmark of these names

failureText

failureText : Check.Failure -> String

measuredJson

measuredJson : Measured -> JSON.Json

What came of a benchmark, as its program says it: JSON, its count, nanoseconds, objects and bytes; or why it failed, or was skipped.

goalOf

goalOf : Int -> Int -> Goal

measuredSaid

measuredSaid : {e : HFunctor}
             -> {{tm : timer <: e}}
             -> {{sys : Process.process <: e}}
             -> {{io : stdio <: e}}
             -> Goal
             -> Maybe (Int -> Co Check.check Unit)
             -> Co e Unit

asked

asked : {e : HFunctor}
      -> {{tm : timer <: e}}
      -> {{sys : Process.process <: e}}
      -> {{io : stdio <: e}}
      -> List Bench
      -> List String
      -> Co e Unit

measured

measured : HFunctor

The effects a file’s benchmarks are run in: the timer, the program’s arguments and its output.

Benchmarks

type Benchmarks = Co measured Unit

What a file’s benchmarks are run by: benchMain’s.

benchMain

benchMain : List Bench -> Benchmarks

The program heff bench builds of a file’s benchmarks: asked for them by its arguments, it says the names of those a pattern selects (list PATTERN), or measures the one its names name (run NANOS COUNT NAME..., a count above 0 run once, else until a run takes the nanoseconds) and says what came of it, a line of JSON.