Std.Http.Server: idle keep-alive timeout is not scheduled, exhausting maxConnections

[counter2015]

Prerequisites

• Searched existing issues and PRs for this problem, including keepAliveTimeout, keep-alive timeout, maxConnections, and HTTP idle connections.
• Reduced the issue to a self-contained reproduction using only Lean's standard library and Python's standard library.
• Reproduced on the latest nightly tested: 4.35.0-nightly-2026-09-05, commit 9de86005af5061b5ccf438d01134ee6d3ecea6b3 (also the current master when checked).

Description

Std.Http.Server does not close idle keep-alive connections after Config.keepAliveTimeout. Once these connections occupy maxConnections, a fresh TCP connection can complete its handshake and send a request, but receives no HTTP response until an existing connection closes. Requests on existing connections still succeed.

For example, with maxConnections := 8 and keepAliveTimeout := 200 milliseconds, all eight connections remain open after completing a request and idling for one second. A ninth connection gets no response during a 750 ms observation window. Closing one of the original connections lets that same pending ninth request complete immediately.

Context

This was found while investigating health-check timeouts in a service using Std.Http.Server. The reproduction below uses a constant response handler and loopback sockets, with no application or database dependencies.

Steps to Reproduce

1. Save this as Main.lean:

import Std.Http
import Std.Http.Server
import Std.Net

open Std.Http Std.Http.Server Std.Net Std.Async

def main (args : List String) : IO Unit := do
  let port := ((args[0]?.getD "0").toNat?.getD 0).toUInt16
  let closeAfterResponse := args[1]? == some "close"
  let handler := Handler.ofFn fun _ => (Response.ok).text "ok\n"
  let config : Std.Http.Config := {
    maxConnections := 8
    keepAliveTimeout := if args[1]? == some "default" then
      ⟨12000, by decide⟩ else ⟨200, by decide⟩
    enableKeepAlive := !closeAfterResponse
  }
  let server ← (Std.Http.Server.serve
    (SocketAddressV4.mk (IPv4Addr.ofParts 127 0 0 1) port) handler config).block
  IO.println "READY"
  (← IO.getStdout).flush
  server.waitShutdown.block

2. With the nightly toolchain installed through Elan, compile and run in one terminal:

elan toolchain install leanprover/lean4-nightly:nightly-2026-09-05
elan run leanprover/lean4-nightly:nightly-2026-09-05 lean -c Main.c Main.lean
elan run leanprover/lean4-nightly:nightly-2026-09-05 leanc -O2 -o server Main.c
./server 18080

Wait for READY. The server binds to 127.0.0.1.

3. Save this as client.py and run python3 client.py 18080 in another terminal. Each initial response body is fully consumed before the idle wait starts.

import contextlib
import http.client
import select
import socket
import sys
import time

port = int(sys.argv[1]) if len(sys.argv) > 1 else 18080
request = (b"GET /health HTTP/1.1\r\nHost: localhost\r\n"
           b"Connection: keep-alive\r\n\r\n")


def response(conn):
    reply = http.client.HTTPResponse(conn)
    reply.begin()
    assert reply.read() == b"ok\n"  # Fully consume the response body.
    assert reply.status == 200
    return reply.status


with contextlib.ExitStack() as stack:
    def connect():
        return stack.enter_context(
            socket.create_connection(("127.0.0.1", port), timeout=3))

    old = []
    for _ in range(8):
        conn = connect()
        old.append(conn)
        conn.sendall(request)
        response(conn)
    print("initial responses: 8 x 200")

    time.sleep(1)  # Five times the configured keepAliveTimeout.
    still_open = 0
    for conn in old:
        if select.select([conn], [], [], 0)[0]:
            assert conn.recv(1) == b""  # EOF from the server.
        else:
            still_open += 1
    print("connections still open after 1s:", still_open)

    ninth = connect()
    ninth.sendall(request)
    ready = bool(select.select([ninth], [], [], 0.75)[0])
    print("new connection responds within 750ms:", ready)
    if ready:
        print("new connection response:", response(ninth))
    else:
        old[0].sendall(request)
        print("existing connection response:", response(old[0]))
        old[0].close()
        print("new connection response after closing one old connection:",
              response(ninth))

Expected behavior: The server closes the eight idle connections after approximately 200 ms, freeing their connection permits. After the one-second wait, the ninth request receives a 200 response without requiring the client to close an older connection.

Actual behavior: On the nightly above, the client prints:

initial responses: 8 x 200
connections still open after 1s: 8
new connection responds within 750ms: False
existing connection response: 200
new connection response after closing one old connection: 200

As a control, stop the server and restart it with ./server 18080 close, which sets enableKeepAlive := false. The same client reports zero surviving connections and an immediate 200 response on the new connection.

Versions

Latest nightly tested, from lean --version:

Lean (version 4.35.0-nightly-2026-09-05, arm64-apple-darwin24.6.0, commit 9de86005af5061b5ccf438d01134ee6d3ecea6b3, Release)

Host: macOS 26.5.1, ARM64. Tests used native executables compiled with each official toolchain's lean -c and leanc -O2.

The same Lean server and black-box test sequence were also run across these versions:

Version	Repeated failing trials	Idle connections remaining after 1 s	Ninth request
v4.31.0	3/3	8/8	No response until one old connection closes
v4.32.0	3/3	8/8	Same
v4.32.1	3/3	8/8	Same
v4.33.0	3/3	8/8	Same
v4.33.1	3/3	8/8	Same
4.35.0-nightly-2026-09-05	3/3	8/8	Same

Each version also passed the keep-alive-disabled control. The smaller standalone client printed above was additionally run against v4.33.1 and the nightly, with the output shown above.

Additional Information

The code appears to omit the idle timer in Connection.pollNextEvent:

    if sources.keepAliveTimeout.isNone then
      if let some timeout := sources.headerTimeout then
        selectables := selectables.push (.case (← Selector.sleep (timeout - (← Timestamp.now)).toMilliseconds) (fun _ => pure .timeout))
      else
        selectables := selectables.push (.case (← Selector.sleep sources.timeout) (fun _ => pure .timeout))

After a completed request, the keep-alive state sets keepAliveTimeout := some config.keepAliveTimeout.val and currentTimeout := config.keepAliveTimeout.val. Therefore the condition above is false during the idle period, and no sleep selector is registered for that timeout.

The server accept loop acquires a connection permit before accepting, and releases it when the connection task exits. Idle connections keep their permits, which explains why closing one immediately unblocks the pending new request.

As a causal check, two isolated copies of the v4.33.1 server were compiled with identical namespace/import changes. The only behavioral difference between the copies was adding this branch alongside if sources.keepAliveTimeout.isNone then:

    else
      selectables := selectables.push (.case (← Selector.sleep sources.timeout) (fun _ => pure .close))

The unmodified control failed in all three trials. The copy with the added idle timer closed all eight idle connections and served the ninth request in all three trials. This is a diagnostic patch; it has not been validated against the full Lean test suite.

The behavior also reproduces at the default scale on v4.33.1: with 1024 connections and the 12000 ms keep-alive timeout, all 1024 remained open after a 13-second idle wait. Request 1025 received no response until an old connection closed, then returned 200 in about 3 ms. With the idle timer added, all 1024 idle connections closed and request 1025 returned 200.

The same missing idle branch exists in the server's original implementation in #12151. v4.30.0 did not contain this HTTP server implementation, so it is not a known-good version of this server.

Related reports #14918 and #14924 describe RSS growth in the accept/selector paths. This report demonstrates idle sockets retaining connection permits; the evidence does not establish that they share a root cause.

AI assistance: Codex was used for source investigation, preparing the reproduction, executing the local tests, and drafting this report. The reported observations come from executed native binaries and captured client output.

Impact

Idle keep-alive connections can consume the server's connection limit even after the configured timeout. Fresh requests, including health checks, then stop receiving responses while existing connections remain usable. This can cause a supervisor to restart a service that is otherwise still processing requests.