fix: lake: open config trace as read-only first & avoid deadlock (lea…

…nprover#3254)

Lake previously opened the configuration trace as read-write even if it
does not update the configuration. This meant it failed if the trace was
read-only. With this change, it now first acquires a read-only handle
and then, if and only if it determines the need for a reconfigure, does
it re-open the file with a read-write handle. Also, this change fixes a
potential deadlock (Lake will error instead) and generally clarifies the
trace locking code.

src/lake/Lake/Load/Elab.lean

@@ -151,10 +151,6 @@ structure ConfigTrace where
   options : NameMap String
   deriving ToJson, FromJson
 
-inductive ConfigLock
-| olean (h : IO.FS.Handle)
-| lean (h : IO.FS.Handle) (lakeOpts : NameMap String)
-
 /--
 Import the `.olean` for the configuration file if `reconfigure` is not set and
 an up-to-date one exists (i.e., one with matching configuration and on the same
@@ -166,55 +162,63 @@ def importConfigFile (pkgDir lakeDir : FilePath) (lakeOpts : NameMap String)
     | error "invalid configuration file name"
   let olean := lakeDir / configName.withExtension "olean"
   let traceFile := lakeDir / configName.withExtension "olean.trace"
+  let lockFile := lakeDir / configName.withExtension "olean.lock"
   /-
-  Remark: To prevent race conditions between the `.olean` and its trace file
+  Remark:
+  To prevent race conditions between the `.olean` and its trace file
   (i.e., one process writes a new configuration while another reads an old one
-  and vice versa), Lake takes opens a single handle on the trace file and
-  acquires a lock on it. The lock is held while the lock data is read and
-  the olean is either imported or a new one is written with new lock data.
+  and vice versa), Lake performs file locking to ensure exclusive access.
+
+  To check if the trace is up-to-date, Lake opens a read-only handle on the
+  trace file and acquires a shared lock on it. The lock is held while the
+  trace is read and compared to the expected value. If it matches, the olean is
+  imported and the (shared) lock is then released.
+
+  If the trace is out-of-date, Lake upgrades the trace to read-write handle
+  with an exclusive lock. Lake does this by first acquiring a exclusive lock to
+  configuration's lock file (i.e. `olean.lock`). While holding this lock, Lake
+  releases the shared lock on the trace, re-opens the trace with a read-write
+  handle, and acquires an exclusive lock on the trace. It then releases its
+  lock on the lock file. writes the new lock data.
   -/
-  let configHash ← computeTextFileHash configFile
-  let configLock : ConfigLock ← id do
-    let validateTrace h : IO ConfigLock := id do
-      if reconfigure then
-        h.lock; return .lean h lakeOpts
-      h.lock (exclusive := false)
-      let contents ← h.readToEnd; h.rewind
-      let .ok (trace : ConfigTrace) := Json.parse contents >>= fromJson?
-        | error "compiled configuration is invalid; run with `-R` to reconfigure"
-      let upToDate :=
-        (← olean.pathExists) ∧ trace.platform = System.Platform.target ∧
-        trace.leanHash = Lean.githash ∧ trace.configHash = configHash
-      if upToDate then
-        return .olean h
-      else
-        -- Upgrade to an exclusive lock
-        let lockFile := lakeDir / configName.withExtension "olean.lock"
-        let hLock ← IO.FS.Handle.mk lockFile .write
-        hLock.lock; h.unlock; h.lock; hLock.unlock
-        return .lean h trace.options
-    if (← traceFile.pathExists) then
-      validateTrace <| ← IO.FS.Handle.mk traceFile .readWrite
+
+  let acquireTrace h : IO IO.FS.Handle := id do
+    let hLock ← IO.FS.Handle.mk lockFile .write
+    /-
+    Remark:
+    We do not wait for a lock here, because that can lead to deadlock.
+
+    This is because we are already holding a shared lock on the trace.
+    If multiple process race for this lock, one will get it and then
+    wait for an exclusive lock one the trace file, but be blocked by the
+    other process with a shared lock waiting on this file.
+
+    While there is likely a way to sequence this to avoid erroring,
+    simultaneous reconfigures are likely to produce unexpected results
+    anyway, so the error seems wise nonetheless.
+    -/
+    if (← hLock.tryLock) then
+      h.unlock
+      let h ← IO.FS.Handle.mk traceFile .readWrite
+      h.lock
+      hLock.unlock
+      return h
     else
-      IO.FS.createDirAll lakeDir
-      match (← IO.FS.Handle.mk traceFile .writeNew |>.toBaseIO) with
-      | .ok h =>
-        h.lock; return .lean h lakeOpts
-      | .error (.alreadyExists ..) =>
-        validateTrace <| ← IO.FS.Handle.mk traceFile .readWrite
-      | .error e => error e.toString
-  match configLock with
-  | .olean h =>
-    let env ← importConfigFileCore olean leanOpts
-    h.unlock
-    return env
-  | .lean h lakeOpts =>
+      h.unlock
+      error <| s!"could not acquire an exclusive configuration lock; " ++
+        "another process may already be reconfiguring the package"
+  let configHash ← computeTextFileHash configFile
+  let elabConfig h (lakeOpts : NameMap String) : LogIO Environment := id do
     /-
-    NOTE: We write the trace before elaborating the configuration file
+    Remark:
+    We write the trace before elaborating the configuration file
     to enable automatic reconfiguration on the next `lake` invocation if
     elaboration fails. To ensure a failure triggers a reconfigure, we must also
     remove any previous out-of-date `.olean`. Otherwise, Lake will treat the
     older `.olean` as matching the new trace.
+
+    See the related PR and Zulip discussion for more details:
+    [leanprover/lean4#3069](https://github.com/leanprover/lean4/pull/3069).
     -/
     match (← IO.FS.removeFile olean |>.toBaseIO) with
     | .ok _ | .error (.noFileOrDirectory ..) =>
@@ -231,3 +235,30 @@ def importConfigFile (pkgDir lakeDir : FilePath) (lakeOpts : NameMap String)
       h.unlock
       IO.FS.removeFile traceFile
       failure
+  let validateTrace h : LogIO Environment := id do
+    if reconfigure then
+      elabConfig (← acquireTrace h) lakeOpts
+    else
+      h.lock (exclusive := false)
+      let contents ← h.readToEnd
+      let .ok (trace : ConfigTrace) := Json.parse contents >>= fromJson?
+        | error "compiled configuration is invalid; run with '-R' to reconfigure"
+      let upToDate :=
+        (← olean.pathExists) ∧ trace.platform = System.Platform.target ∧
+        trace.leanHash = Lean.githash ∧ trace.configHash = configHash
+      if upToDate then
+        let env ← importConfigFileCore olean leanOpts
+        h.unlock
+        return env
+      else
+        elabConfig (← acquireTrace h) trace.options
+  if (← traceFile.pathExists) then
+    validateTrace <| ← IO.FS.Handle.mk traceFile .read
+  else
+    IO.FS.createDirAll lakeDir
+    match (← IO.FS.Handle.mk traceFile .writeNew |>.toBaseIO) with
+    | .ok h =>
+      h.lock; elabConfig h lakeOpts
+    | .error (.alreadyExists ..) =>
+      validateTrace <| ← IO.FS.Handle.mk traceFile .read
+    | .error e => error e.toString