42 lines
1.5 KiB
Markdown
42 lines
1.5 KiB
Markdown
# 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
|
|
|
|
```cpp
|
|
// 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.
|