Selectable.one + TCP.recvSelector retains RSS on repeated wait-for-read (not recv?)

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.
• Official x86_64-unknown-linux-gnu nightly-2026-08-22 still reproduces (see numbers). Not applicable on live.lean-lang.org (needs native TCP + ab).

Not a duplicate of #14918 (ContextAsync accept while / Task chain). This repro uses an IO accept loop. Closing that loop does not remove the retain.

Related:

• PR 8003: recursive Async Task chains. This repro uses Async while (EAsync trampoline ForIn) and still retains.
• PR 14253: Selectable.one unregister-on-error / combine. Present in 4.34.0-rc2 and nightly-2026-08-22; the retain remains. This is a steady keep-alive wait, not a rare registerFn throw.
• Issue 13469: HTTP speed, not RSS.

Description

Repeated Selectable.one on TCP.Socket.Client.recvSelector retains heap under keep-alive traffic. The same server with client.recv? instead plateaus.

No Std.Http. The server only scans for \r\n\r\n and writes a fixed 200 so ab -k stays on the socket.

Keep-alive wait has no bytes yet, so recvSelector.tryFn returns none (waitReadable + cancelRecv) and every request hits registerFn.

Pin:

1. Trigger: Selectable.one #[.case (client.recvSelector 4096) pure]
2. Control: client.recv? 4096
3. Register path: recvSelector.registerFn in Std/Async/TCP.lean (waitReadable, then discarded IO.mapTask on readableWaiter.result?; unregisterFn is cancelRecv)
4. Mux: Selectable.one / Selectable.combine in Std/Async/Select.lean

Kernel objects do not grow (fds / kqueue / thread count were flat on the native build). RSS does not drop after idle. MIMALLOC_PURGE_DELAY=0 does not stop it.

Std.Http.Server.Connection.pollNextEvent is one production caller of this path. The leak is not HTTP-specific.

Steps to Reproduce

Lake exe, stdlib only. lean-toolchain: leanprover/lean4:v4.33.1 (also 4.34.0-rc2 / nightly).

lakefile.toml:

name = "tcp-keepalive-rss"
defaultTargets = ["tcp-keepalive-rss"]

[[lean_exe]]
name = "tcp-keepalive-rss"
root = "TcpKeepalive"

TcpKeepalive.lean:

module
public import Std.Async
public import Std.Async.TCP
public import Std.Async.Select
public import Std.Net

open Std Async
open Std.Net
open Std.Async.TCP

def canned : ByteArray :=
  "HTTP/1.1 200 OK\r\nContent-Type: text/plain; charset=utf-8\r\nContent-Length: 3\r\nConnection: keep-alive\r\n\r\nok\n".toUTF8

partial def headerEnd? (b : ByteArray) : Option Nat :=
  let rec go (i : Nat) : Option Nat :=
    if i + 4 > b.size then none
    else if b.get! i == (13 : UInt8) &&
            b.get! (i + 1) == (10 : UInt8) &&
            b.get! (i + 2) == (13 : UInt8) &&
            b.get! (i + 3) == (10 : UInt8) then
      some (i + 4)
    else
      go (i + 1)
  go 0

partial def drain (c : Socket.Client) (buf : ByteArray) : Async ByteArray := do
  match headerEnd? buf with
  | none => return buf
  | some e =>
    c.send canned
    drain c (buf.extract e buf.size)

def loopRecv (c : Socket.Client) : Async Unit := do
  let mut buf := ByteArray.empty
  try
    while true do
      buf ← drain c buf
      match ← c.recv? 4096 with
      | none => break
      | some chunk =>
        if chunk.size == 0 then break
        buf := buf ++ chunk
  catch _ =>
    pure ()

def loopSelect (c : Socket.Client) : Async Unit := do
  let mut buf := ByteArray.empty
  try
    while true do
      buf ← drain c buf
      match ← Selectable.one #[.case (c.recvSelector 4096) pure] with
      | none => break
      | some chunk =>
        if chunk.size == 0 then break
        buf := buf ++ chunk
  catch _ =>
    pure ()

inductive Mode where
  | recv
  | select

def parse : List String → UInt16 × Mode
  | p :: "select" :: _ => (portOf p, .select)
  | p :: "recv" :: _ => (portOf p, .recv)
  | p :: _ => (portOf p, .recv)
  | [] => (8084, .recv)
where
  portOf (s : String) : UInt16 :=
    match s.toNat? with
    | some n => if n = 0 || n > 65535 then 8084 else n.toUInt16
    | none => 8084

def serve (port : UInt16) (mode : Mode) : IO Unit := do
  let addr : SocketAddress := .v4 ⟨.ofParts 127 0 0 1, port⟩
  let tcp ← Socket.Server.mk
  tcp.bind addr
  tcp.listen 1024
  tcp.noDelay
  discard <| IO.asTask (prio := .dedicated) do
    while true do
      let client ← Async.block tcp.accept
      client.noDelay
      let loop := match mode with
        | .recv => loopRecv
        | .select => loopSelect
      discard <| IO.asTask (prio := .dedicated) (Async.block (loop client))
  while true do
    IO.sleep 3600000

public def main (args : List String) : IO Unit := do
  let (port, mode) := parse args
  serve port mode

Then:

lake exe tcp-keepalive-rss 8084 recv
# other terminal:
ab -c 50 -k -n 800000 -q http://127.0.0.1:8084/ping
# sample `ps -o rss= -p <pid>` at 0 / 200k / 400k / 800k
# repeat with: lake exe tcp-keepalive-rss 8084 select

Expected: RSS plateaus after warmup under fixed concurrency, same as recv?.

Actual: RSS kB, last column is 400k→800k. Child process (not lake).

Official x86_64-unknown-linux-gnu (Linux ELF):

nightly-2026-08-22 (4.35.0, fd0efc4306a7)
  recv?                          5524 → 11048 → 11320 → 11128    last 400k  -192
  Selectable.one + recvSelector  5600 → 23708 → 25164 → 26372    last 400k +1208

v4.33.1 (819816b2e0a3)
  recv?                          5300 → 12516 → 14864 → 15440    last 400k  +576
  Selectable.one + recvSelector  5544 → 24576 → 27764 → 28708    last 400k  +944

Native x86_64-unknown-freebsd15.0 (same program):

v4.34.0-rc2 (6a10ac8c22be, includes #14253)
  recv?                         13844 → 26768 → 28020 → 28500    last 400k  +480
  Selectable.one + recvSelector 14144 → 37800 → 41896 → 43956    last 400k +2060

v4.33.1 (819816b2e0a3)
  recv?                         13660 → 27840 → 32072 → 31888    last 400k  -184
  Selectable.one + recvSelector 14360 → 41328 → 47548 → 50356    last 400k +2808

Versions

Lean 4.35.0-nightly-2026-08-22, x86_64-unknown-linux-gnu, commit fd0efc4306a7773c2cd4e079ddaa907426d0f5da
Lean 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6
Lean 4.34.0-rc2, x86_64-unknown-freebsd15.0, commit 6a10ac8c22beadecabdbb0919c2b50214762f91d
Lean 4.33.1, x86_64-unknown-freebsd15.0, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6

linux-gnu numbers are the official release tarballs (Linux ELF, interpreter /lib64/ld-linux-x86-64.so.2). Host is FreeBSD 15 / amd64; those binaries ran under linux(4). Native freebsd15.0 builds of the same program show the same shape.

Additional Information

Workaround for a single socket wait: use recv?, not Selectable.one / recvSelector. Std.Http cannot do that today because pollNextEvent multiplexes socket, body, handler channel, timeouts, and cancellation.

Exact retained objects (Promise vs Task vs closure vs uv waiter) were not named. Heap grows; sockets/fds do not.

Impact

Any long-lived process that waits for the next TCP read with Selectable.one + recvSelector (including Std.Http.Server keep-alive via pollNextEvent) grows RSS with request count. Easy to misread as a handler leak or an allocator bug.

Start with the minimal TcpKeepalive.lean reproducer and compare the recv? and Selectable.one modes under repeated keep-alive requests. Read recvSelector.registerFn in Std/Async/TCP.lean, then follow Selectable.one and Selectable.combine in Std/Async/Select.lean, including the waitReadable, cancelRecv, and discarded task paths. Done means repeated selector waits no longer grow RSS while sockets and request behavior remain stable.