perf: avoid taking mutex on already-resolved promises

leanprover · Feb 7, 2025 · ee398e2 · ee398e2
1 parent b01ca8e
commit ee398e2
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
@@ -838,6 +838,10 @@ class task_manager {
     }
 
     void resolve(lean_task_object * t, object * v) {
+        if (t->m_value) {
+            dec(v);
+            return;
+        }
         unique_lock<mutex> lock(m_mutex);
         if (t->m_value) {
             lock.unlock(); // `dec(v)` could lead to `deactivate_task` trying to take the lock