Std.Http.Server.serve accept loop leaks RSS: ContextAsync `while` chains Tasks until shutdown

Std.Http.Server.serve accept loop leaks RSS: ContextAsync while chains Tasks until shutdown

--- paste below this line into the GitHub issue body ---

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Tested on live.lean-lang.org nightly: not applicable (needs a native HTTP server plus ab).
  Please confirm on master that Std.Http.Server.serve still runs while true inside ContextAsync.

Related but not the same:

• PR 8003 (Async monad): authors already noted infinite Task chains in HTTP servers; point 3 was explicitly not shipped.
• Issue 13469: Std.Http throughput, not a per-connection RSS leak.
• No issue found for ContextAsync while / Server.serve accept-loop RSS.

Description

Std.Http.Server.serve accepts connections with while true in ContextAsync.

EAsync has a trampoline ForIn (chainTask plus Promise). ContextAsync has no ForIn instance, so while/repeat use the generic instance

instance [Monad m] : ForIn m Loop Unit

which is Loop.forIn to repeatM to recursive bind. ContextAsync.bind is Async.bind to Task.bind. Continuations are released only when that whole computation returns. The accept loop is not supposed to return, so each accepted connection adds a live frame until process exit.

maxRequests default 100 makes this easy to hit with ab -k: keep-alive looks like 8 connections, but the server closes every 100 requests and ab reconnects. ab -c 8 -k -n 1000000 is about 10,000 accept/close cycles, not 8 long-lived sockets.

A handler that returns (for example GET / serving a static HTML string) is not the leak. Connection churn is.

Context

Observed on a small Lean 4.33.1 Std.Http.Server (hello-page plus optional long-lived stream). Same machine: replacing only the accept loop with IO while true plus Async.block tcp.accept plus background (serveConnection ...) stopped the growth.

Same underlying footgun as user-level partial def loop : Async Unit := do ...; loop (hour-scale stream). That is expected from PR 8003. The new fact is that the stdlib accept loop is itself a ContextAsync while.

OS is FreeBSD 15 / amd64. This is not a FreeBSD or mimalloc bug: the Task.bind chain is in Std.Async / Std.Http (same argument as issue 14246).

Steps to Reproduce

Minimal server (Lake exe, Lean 4.33.1+ Std.Http):

import Std.Http
import Std.Async

open Std.Http.Server
open Std.Async

def handle (_ : Request Body.Stream) : ContextAsync (Response Body.Any) :=
  Response.ok |>.text "ok\n"

def main : IO Unit := do
  let addr : Std.Net.SocketAddress := .v4 ⟨.ofParts 127 0 0 1, 8081⟩
  -- default Config.maxRequests = 100
  let server ← Async.block <| Server.serve addr handle
  IO.println "listening 127.0.0.1:8081"
  Async.block server.waitShutdown

Then:

# many new connections (clearest RSS slope)
ab -c 8 -n 20000 -q http://127.0.0.1:8081/

# keep-alive still churns because maxRequests = 100
ab -c 8 -k -n 20000 -q http://127.0.0.1:8081/

Sample RSS (ps -o rss= -p <pid>) before/after.

Expected behavior: RSS plateaus under a fixed concurrency (8 connections or 8 workers). Closing a connection frees the accept-loop frame.

Actual behavior: RSS climbs with accepted connection count and does not drop when clients disconnect (server still running). On this host, library Server.serve: about +17 MiB per 5,000 new connections. Same handler with an IO accept loop: about +0.5 MiB per 20,000 new connections.

Versions

Lean 4.33.1

FreeBSD 15.0 / amd64

(lean --version on the machine that ran ab.)

Additional Information

What would actually help (not a CPS rewrite of Async):

1. Give ContextAsync the same trampoline ForIn as EAsync (chainTask plus Promise), or rewrite Server.serve's accept loop in IO while (the workaround that plateaus).
2. A short warning on Server.serve / ContextAsync: unbounded while/repeat chains Tasks until return; maxRequests default 100 closes keep-alive and multiplies accepts.

Please do not treat this as a request to trampoline all of Async.bind (already declined in PR 8003 because of IR size).

Workaround for applications: do not use Server.serve's accept loop; Socket.Server.accept in IO while plus serveConnection. Raising maxRequests only hides ab -k; it does not fix ab without -k.

Impact

Any long-lived Std.Http.Server under connection churn (benchmarks, reverse proxies, clients that do not keep-alive, default maxRequests) will grow RSS for the life of the process. Easy to misread as a handler leak or an allocator bug.

Start at Std.Http.Server.serve and the ContextAsync generic ForIn implementation described in the issue, then reproduce the RSS slope with the provided server and ab commands. Done means the accept loop no longer retains an unbounded Task chain and RSS plateaus during connection churn; compare against the stated IO-loop workaround.