Skip to content

Cancel Pareto-searching threads in OGIA if all Pareto points have already been found #43

@mhyee

Description

@mhyee

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.

Metadata

Metadata

Assignees

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions