TeamAmalgam / kodkod

Kodkod relational model finder
Other
3 stars 0 forks source link

Solution Deduplicator and Overlapped GIA #36

Closed joseph39 closed 11 years ago

joseph39 commented 11 years ago

This pull request now includes the checking of exclusion constraints between different threads.

Reviewers: @mhyee @cpkleynhans @AtulanZaman

mhyee commented 11 years ago

So it looks like the ExecutorService is to schedule tasks to threads, and when you submit a task, you put the returned Future in a waitQueue, so you can wait until all tasks are done.

Java has something called an ExecutorCompletionService which is an abstraction of what you're trying to do. It takes an ExecutorService and has its own queue for results. However, it takes Callables instead of Runnables (the difference is that a Callable is a Runnable with some return value.)

So it might not be a perfect fit, but I'm suggesting it because you pass both the ExecutorService and waitQueue to the SolverSubtask, when passing only an ExecutorCompletionService provides better encapsulation, ie the SolverSubtask should not be able to shut down the ExecutorService.

cpkleynhans commented 11 years ago

Other than defaulting to OGIA, LGTM. Make sure to resolve the merge conflicts.