java-topology/docs/tickets/lean4-0004-irinterpreter-double-checked-locking-race.md

lean4-0004: ir_interpreter.cpp — double-checked locking without memory barrier in symbol lookup

Target: leanprover/lean4 Severity: HIGH CWE: CWE-362 (Concurrent Execution Using Shared Resource with Improper Synchronization) MOAD: MOAD-0005 (A Thundering Herd) File: src/library/ir_interpreter.cpp:828–869 Language: C++ Status: open

Description

lookup_symbol in the IR interpreter uses a double-checked locking pattern without memory barriers. A first check on m_symbol_cache runs without any lock. A second check on g_native_symbol_cache runs under shared lock. Between the two, the lock is released and re-acquired as exclusive. On weakly-ordered architectures, two concurrent threads can both pass the unguarded first check, both acquire exclusive lock in sequence, and insert duplicate entries — or worse, observe partially-constructed cache entries.

Root Cause

// ir_interpreter.cpp:828–869 (simplified)
auto e = m_symbol_cache.find(fn);       // (1) unguarded check
if (e != m_symbol_cache.end()) {
    return e->second;
}
std::shared_lock<std::shared_mutex> lock(*g_native_symbol_cache_mutex);
auto ne = g_native_symbol_cache->find(fn);  // (2) shared-locked check
if (ne != g_native_symbol_cache->end()) {
    m_symbol_cache.insert({ fn, e_new });   // inserts without exclusive lock
    return e_new;
}
lock.unlock();
std::unique_lock<std::shared_mutex> unique_lock(*g_native_symbol_cache_mutex);
ne = g_native_symbol_cache->find(fn);   // (3) double-check under exclusive lock
if (ne == g_native_symbol_cache->end()) {
    // ... compute ...
    g_native_symbol_cache->insert({ fn, e_new.m_native });
}

Step (1) reads m_symbol_cache without synchronization. On x86 this is generally safe due to TSO, but on ARM/RISC-V reordering can expose partially-initialized entries from another thread's prior insert.

Fix

Use std::atomic<bool> or ensure m_symbol_cache access is guarded by the same mutex. Alternatively, use a single-phase double-check under the exclusive lock:

{
    std::shared_lock lock(*g_native_symbol_cache_mutex);
    auto e = m_symbol_cache.find(fn);
    if (e != m_symbol_cache.end()) return e->second;
}
std::unique_lock lock(*g_native_symbol_cache_mutex);
// recheck under exclusive lock, then compute+insert