java-topology/docs/tickets/lean4-0005-lake-job-registration-concurrent-race.md

lean4-0005: Lake/Build/Run.lean — concurrent job registration races on JobQueue IO.Ref

Target: leanprover/lean4 Severity: HIGH CWE: CWE-362 (Concurrent Execution Using Shared Resource with Improper Synchronization) MOAD: MOAD-0005 (A Thundering Herd) Files: src/lake/Lake/Build/Job/Register.lean:43, src/lake/Lake/Build/Run.lean:157 Language: Lean 4 Status: open

Description

Multiple async build tasks call registerJob concurrently. Each calls registeredJobs.modify (·.push job) on a shared IO.Ref (Array OpaqueJob) without a mutex. Lean's IO.Ref.modify is not atomic with respect to concurrent tasks — two tasks can both read the same array, both push their job, and one registration gets lost.

Root Cause

-- Lake/Build/Context.lean:42
public def JobQueue := IO.Ref (Array OpaqueJob)

-- Lake/Build/Job/Register.lean:43
(← getBuildContext).registeredJobs.modify (·.push job)
-- ↑ read-modify-write on shared IO.Ref, no mutex

Concurrently spawned tasks (via Job.async) all share the same BuildContext.registeredJobs. Each calls .modify independently:

• Task A reads array [j1, j2]
• Task B reads array [j1, j2]
• Task A writes [j1, j2, jA]
• Task B writes [j1, j2, jB] ← overwrites Task A's registration
• jA is lost from the monitor

-- Lake/Build/Run.lean:157 — monitor reads the same ref
let newJobs ← (← read).jobs.modifyGet ((·, #[]))

The monitor drain races with concurrent registrations.

Fix

Wrap JobQueue with a Mutex or use IO.Mutex:

public def JobQueue := IO.Mutex (Array OpaqueJob)

-- register:
(← getBuildContext).registeredJobs.atomically (·.push job)

-- poll:
let newJobs ← (← read).jobs.atomically (fun arr => (arr, #[]))

Or use a Channel/Queue abstraction that is safe for concurrent push from producers and drain from the monitor consumer.