From 8e9da7a1bcfbfc313301df86274f9c93f1cc66db Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Mon, 14 Apr 2025 13:53:54 +0200 Subject: [PATCH] feat: wait on dedicated tasks after main is finished (#7958) This PR ensures that after `main` is finished we still wait on dedicated tasks instead of exiting forcefully. If users wish to violently kill their dedicated tasks at the end of main instead they can run `IO.Process.exit` at the end of `main` instead. --- src/runtime/object.cpp | 5 +++++ tests/compiler/wait_dedicated.lean | 10 ++++++++++ tests/compiler/wait_dedicated.lean.expected.out | 1 + 3 files changed, 16 insertions(+) create mode 100644 tests/compiler/wait_dedicated.lean create mode 100644 tests/compiler/wait_dedicated.lean.expected.out diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index 3096e0d153..204aa5b382 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -666,6 +666,7 @@ class task_manager { unsigned m_max_prio{0}; condition_variable m_queue_cv; condition_variable m_task_finished_cv; + condition_variable m_dedicated_finished_cv; bool m_shutting_down{false}; lean_task_object * dequeue() { @@ -762,6 +763,7 @@ class task_manager { unique_lock lock(m_mutex); run_task(lock, t); m_num_dedicated_workers--; + m_dedicated_finished_cv.notify_all(); }); // `lthread` will be implicitly freed, which frees up its control resources but does not terminate the thread } @@ -863,6 +865,9 @@ public: // wait for all workers to finish for (auto & t : m_std_workers) t->join(); + + unique_lock lock(m_mutex); + m_dedicated_finished_cv.wait(lock, [&]() { return m_num_dedicated_workers == 0; }); // never seems to terminate under Emscripten #endif } diff --git a/tests/compiler/wait_dedicated.lean b/tests/compiler/wait_dedicated.lean new file mode 100644 index 0000000000..47d5ee0702 --- /dev/null +++ b/tests/compiler/wait_dedicated.lean @@ -0,0 +1,10 @@ +/- Ensure we wait on dedicated tasks even after main is finished -/ + +def stuff : IO Unit := do + IO.sleep 100 + IO.println "Hi there" + + +def main : IO Unit := do + discard <| IO.asTask (prio := .dedicated) stuff + diff --git a/tests/compiler/wait_dedicated.lean.expected.out b/tests/compiler/wait_dedicated.lean.expected.out new file mode 100644 index 0000000000..6530b63ec9 --- /dev/null +++ b/tests/compiler/wait_dedicated.lean.expected.out @@ -0,0 +1 @@ +Hi there