Skip to content

Bench: Std.Http.Server reference — reactor is 44x faster#4

Merged
junjihashimoto merged 1 commit into
mainfrom
feat/http-backends
Jul 2, 2026
Merged

Bench: Std.Http.Server reference — reactor is 44x faster#4
junjihashimoto merged 1 commit into
mainfrom
feat/http-backends

Conversation

@junjihashimoto

Copy link
Copy Markdown
Contributor

Follow-up measurement on PR #3.

What this adds

  • examples/BenchStdHttp/Main.lean — same three routes (`/health`, `/json`, `/echo`) but implemented on top of Lean 4.31's stock `Std.Http.Server` (Sofia Rodrigues, 2025). Compiled as `lean_exe bench_std_http`.
  • New "Reference: `Std.Http.Server` (Lean 4.31 stock)" section in `docs/BENCHMARKS.md` with numbers side-by-side against the reactor and nginx.

Result

Same wrk load, same box (M-series, 16 core), same run:

server /health RPS /json RPS p99 (ms)
`Std.Http.Server` 1 652 1 622 178–196
lean-tea reactor 73 533 69 069 2.1
nginx 72 183 66 384 2.0

Reactor is ~44 × the throughput of the stock Std server at ~1/80 the p99 latency.

Why

Two overlapping causes:

  1. `Std.Async.TCP` per-syscall hop. Same reason our own libuv `LeanTea.Net.Server` topped out at 6 k — every recv/send round-trips through the async task scheduler. `Std.Http.Server` inherits this ceiling directly.
  2. Extra per-connection bookkeeping. `Std.Http.Server` layers `Std.Semaphore` (connection limit) + `Std.Mutex Nat` (active-conn counter) + `Std.CancellationContext` (shutdown coord) + the full RFC-9112 `Std.Http.Protocol.H1` streaming codec on top. The 178 ms p99 is characteristic of semaphore/mutex contention under keep-alive load.

That said: `Std.Http.Server` is the correct implementation — HTTP/1.1 pipelining, `Expect: 100-continue`, chunked streaming request bodies, graceful shutdown across in-flight requests, proper cancellation. The reactor gives up all of that for the 44×. Both belong in the framework; pick by workload. The BENCHMARKS.md prose says this.

Test plan

  • `lake build bench_std_http` clean.
  • Sanity: `curl /health` returns `OK`, `curl /json` returns the payload, `curl -X POST -d hello /echo` echoes.
  • wrk numbers reproduced above.
  • CI `bench.yml` — this PR doesn't touch the workflow; `Std.Http.Server` isn't in the tracker (yet). If we want it long-term as a trend series, add it as a separate follow-up.

examples/BenchStdHttp/Main.lean serves the same three routes
(/health, /json, /echo) through Lean 4.31's stock Std.Http.Server
so docs/BENCHMARKS.md can show a like-for-like comparison against
the reactor and nginx.

Result on the M-series box, wrk t=8 c=128 15s:

  Std.Http.Server (stock)   1 652 RPS   p99 178 ms
  lean-tea reactor         73 533 RPS   p99   2.1 ms
  nginx                    72 183 RPS   p99   2.0 ms

The 44x gap is not the codec: it's the same Std.Async.TCP hop
per-syscall that capped our own libuv Server at 6 k, plus extra
per-connection bookkeeping (Semaphore + Mutex + CancellationContext
+ full RFC-9112 streaming H1 codec). The 178 ms p99 is
characteristic of semaphore/mutex contention under keep-alive load.

Std.Http.Server is the *correct* implementation — full HTTP/1.1
pipelining, Expect: 100-continue, chunked streaming bodies,
graceful shutdown across in-flight requests, cancellation. The
reactor gives up all of that for the 44x. Both belong; pick by
workload.
@junjihashimoto junjihashimoto merged commit 0a0afcc into main Jul 2, 2026
1 check passed
@junjihashimoto junjihashimoto deleted the feat/http-backends branch July 2, 2026 01:06
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant