In the OGIA, if a thread is trying to find a new Pareto point and gets an UNSAT call, that means, based on its knowledge of the shared queue of global Pareto points and what it knows locally, all Pareto points have been found.*
Thus, any remaining tasks searching for Pareto points (whether they're throwing new darts or climbing up to the Pareto front) can be cancelled. However, we do not want to cancel any existing magnifier tasks.
Currently, we wait until all threads have gotten their UNSAT calls. So effectively, we wait for the slowest thread to finish.
*I'm pretty sure this argument is correct, but I could be wrong.
In the OGIA, if a thread is trying to find a new Pareto point and gets an UNSAT call, that means, based on its knowledge of the shared queue of global Pareto points and what it knows locally, all Pareto points have been found.*
Thus, any remaining tasks searching for Pareto points (whether they're throwing new darts or climbing up to the Pareto front) can be cancelled. However, we do not want to cancel any existing magnifier tasks.
Currently, we wait until all threads have gotten their UNSAT calls. So effectively, we wait for the slowest thread to finish.
*I'm pretty sure this argument is correct, but I could be wrong.