60 lines
1.9 KiB
Markdown
60 lines
1.9 KiB
Markdown
# 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
|
|
|
|
```lean
|
|
-- 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
|
|
|
|
```lean
|
|
-- 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`:
|
|
|
|
```lean
|
|
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.
|