Skip to content

Commit 2538854

Browse files
authored
feat: add a Selectable.one benchmark (#14251)
This PR adds a benchmark for an instantly succeeding `Selectable.one`.
1 parent 390cdf5 commit 2538854

3 files changed

Lines changed: 45 additions & 0 deletions

File tree

tests/compile_bench/select.lean

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
import Std.Async.Select
2+
3+
/-!
4+
Benchmarks `Selectable.one` on a pair of custom `Selectable`s that resolve
5+
instantly via their non-blocking `tryFn`, exercising the fast path of the
6+
selection protocol in a configurable iteration loop.
7+
-/
8+
9+
open Std Async
10+
11+
/-- A `Selector` that instantly resolves with `value` through its non-blocking `tryFn`. -/
12+
def instantSelector (value : α) : Selector α where
13+
tryFn := pure (some value)
14+
registerFn _ := pure ()
15+
unregisterFn := pure ()
16+
17+
/-- A `Selectable` built from `instantSelector` that yields `value` unchanged. -/
18+
def instantSelectable (value : Nat) : Selectable Nat :=
19+
.case (instantSelector value) pure
20+
21+
def bench (iterations : Nat) : Async Nat := do
22+
let mut acc := 0
23+
for i in *...iterations do
24+
acc := acc + (← Selectable.one #[instantSelectable i, instantSelectable (i + 1)])
25+
return acc
26+
27+
def run (name : String) (iterations : Nat) : IO Unit := do
28+
let t1 ← IO.monoMsNow
29+
let acc ← (bench iterations).block
30+
let t2 ← IO.monoMsNow
31+
let time : Float := (t2 - t1).toFloat / 1000.0
32+
IO.println s!"measurement: {name} {time} s"
33+
-- Consume `acc` so the loop cannot be optimized away; the bound is never hit.
34+
if acc > iterations * iterations + iterations then
35+
throw <| .userError "unreachable"
36+
37+
def main (args : List String) : IO Unit := do
38+
let iterations := args[0]!.toNat!
39+
run "select_one_two" iterations
Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
TEST_ARGS=( 1000 )
2+
3+
if [[ -n $TEST_BENCH ]]; then
4+
TEST_ARGS=( 400000 )
5+
fi
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
measurement: select_one_two ...

0 commit comments

Comments
 (0)