russell@unturf.com
ae6e04c5bd
lean4-0004: collapse 3-phase lock in ir_interpreter lookup_symbol to single unique_lock lean4-0005: replace IO.Ref JobQueue with Std.Mutex in Lake job registry lean4-0006: register thread-local reset for g_opts in kernel/trace.cpp lean4-0007: build unordered_set of override keys outside env-var loop (Windows)
53 lines
2.3 KiB
Diff
53 lines
2.3 KiB
Diff
# UNDF: UNDF-2026-000001263
|
||
# CWE-362: Race Condition -- registerJob IO.Ref.modify without mutex
|
||
#
|
||
# Defect: registeredJobs : IO.Ref (Array OpaqueJob). Multiple concurrent async
|
||
# tasks call .modify (·.push job) simultaneously. IO.Ref.modify is not atomic
|
||
# across tasks -- concurrent pushes lose registrations.
|
||
#
|
||
# Fix: IO.Mutex (Array OpaqueJob) with .atomically for all register + poll ops.
|
||
#
|
||
# Complexity gate: correctness -- no lost registrations under -j 8 parallel build
|
||
--- a/src/lake/Lake/Build/Context.lean
|
||
+++ b/src/lake/Lake/Build/Context.lean
|
||
@@ -6,6 +6,8 @@ module
|
||
|
||
prelude
|
||
+public import Std.Sync.Mutex
|
||
public import Lake.Config.Cache
|
||
public import Lake.Config.Context
|
||
public import Lake.Build.Job.Basic
|
||
@@ -40,10 +42,10 @@ public def BuildConfig.showProgress (cfg : BuildConfig) : Bool :=
|
||
(cfg.noBuild ∧ cfg.verbosity == .verbose) ∨ cfg.verbosity != .quiet
|
||
|
||
-/-- Mutable reference of registered build jobs. -/
|
||
+/-- Mutex-guarded queue of registered build jobs. -/
|
||
@[expose] -- for codegen
|
||
-public def JobQueue := IO.Ref (Array OpaqueJob)
|
||
+public def JobQueue := Std.Mutex (Array OpaqueJob)
|
||
|
||
-/-- Returns a new empty job queue. -/
|
||
+/-- Returns a new empty job queue (mutex-guarded). -/
|
||
@[inline] public def mkJobQueue : BaseIO JobQueue :=
|
||
- IO.mkRef #[]
|
||
+ Std.Mutex.new #[]
|
||
--- a/src/lake/Lake/Build/Job/Register.lean
|
||
+++ b/src/lake/Lake/Build/Job/Register.lean
|
||
@@ -38,7 +38,9 @@ public def Job.renew (self : Job α) : Job α :=
|
||
@[inline] public def registerJob
|
||
[Monad m] [MonadLiftT (ST IO.RealWorld) m] [MonadBuild m]
|
||
+ [MonadLiftT BaseIO m] [MonadFinally m]
|
||
(caption : String) (job : Job α) (optional := false)
|
||
: m (Job α) := do
|
||
let job : Job α := {job with caption, optional}
|
||
- (← getBuildContext).registeredJobs.modify (·.push job)
|
||
+ (← getBuildContext).registeredJobs.atomically (·.modify (·.push job))
|
||
return job.renew
|
||
--- a/src/lake/Lake/Build/Run.lean
|
||
+++ b/src/lake/Lake/Build/Run.lean
|
||
@@ -156,7 +156,7 @@ where
|
||
def poll (unfinished : Array OpaqueJob) : MonitorM (Array OpaqueJob × Array OpaqueJob) := do
|
||
- let newJobs ← (← read).jobs.modifyGet ((·, #[]))
|
||
+ let newJobs ← (← read).jobs.atomically (·.modifyGet ((·, #[])))
|
||
modify fun s => {s with totalJobs := s.totalJobs + newJobs.size}
|
||
let pollJobs := fun (running, unfinished) job => do
|