java-topology/docs/tickets/lean4-0006-kernel-trace-thread-local-options-leak.md

lean4-0006: kernel/trace.cpp — LEAN_THREAD_PTR(g_opts) leaks trace options across tasks on thread pool reuse

Target: leanprover/lean4 Severity: MEDIUM CWE: CWE-668 (Exposure of Resource to Wrong Sphere) MOAD: MOAD-0003 (A Leaked Context) File: src/kernel/trace.cpp:16 Language: C++ Status: open

Description

g_opts — the trace options pointer — is stored as a thread-local variable via LEAN_THREAD_PTR. Lean's async task system uses a thread pool. When a thread finishes one elaboration task and picks up a new one, the thread-local g_opts from the previous task remains set. The new task inherits the old trace configuration, causing incorrect trace output (silence when tracing expected, or noise when silence expected).

Root Cause

// kernel/trace.cpp:16
LEAN_THREAD_PTR(const options, g_opts);

// kernel/trace.cpp:25
bool is_trace_class_enabled(name const & n) {
    if (!g_opts) return false;
    return is_trace_class_enabled_core(*g_opts, n);
}

g_opts is set per-elaboration invocation but never explicitly cleared on task completion. Thread pool threads reuse their g_opts across tasks.

Fix

Reset g_opts to nullptr at task boundaries (on task start/end in the thread pool scheduler), or pass options explicitly via context rather than thread-local. The pattern of setting thread-locals before a task and clearing after is already used in other parts of the runtime (reset_thread_local()). Apply the same discipline here.