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.
This commit is contained in:
parent
ac738a8e81
commit
8e9da7a1bc
3 changed files with 16 additions and 0 deletions
|
|
@ -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<mutex> 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<mutex> lock(m_mutex);
|
||||
m_dedicated_finished_cv.wait(lock, [&]() { return m_num_dedicated_workers == 0; });
|
||||
// never seems to terminate under Emscripten
|
||||
#endif
|
||||
}
|
||||
|
|
|
|||
10
tests/compiler/wait_dedicated.lean
Normal file
10
tests/compiler/wait_dedicated.lean
Normal file
|
|
@ -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
|
||||
|
||||
1
tests/compiler/wait_dedicated.lean.expected.out
Normal file
1
tests/compiler/wait_dedicated.lean.expected.out
Normal file
|
|
@ -0,0 +1 @@
|
|||
Hi there
|
||||
Loading…
Add table
Reference in a new issue