TeamAmalgam / kodkod

Kodkod relational model finder
Other
3 stars 0 forks source link

Bounded GIA #31

Closed mhyee closed 11 years ago

mhyee commented 11 years ago

Fixes #25.

This is a first step to a larger parallelization effort. First, we have to find all the boundaries of the problem (ie with two objectives, we draw a "rectangle").

This is the basic algorithm:

The boundary finding is multithreaded. A thread pool is created with min(user value, number of cores, number of objectives) threads. The user value is currently hard-coded to 8; #30 aims to resolve this.

The thread pool is managed by an ExecutorCompletionService. Tasks are added to its work queue in the form of Callable<T> objects. (A Callable<T> is like a Runnable but it returns a result of type T.) Solutions are packaged as Futures and then added to a blocking queue. Thus, the algorithm thread (recall the algorithm thread is separate from the main thread) blocks until all results are available.

I'd like to merge this into master now, even though there's still a lot of related work left. I would rather send a pull request for a smallish self-contained change, rather than some enormous pull request.

Note also that this (currently) hard-codes the algorithm to PartitionedGIA; #17 is supposed to resolve this.

Reviewers: @AtulanZaman @cpkleynhans @joseph2625

AtulanZaman commented 11 years ago

Looks fine.

cpkleynhans commented 11 years ago

Just a couple of comments regarding defaults and choice of a regular solver

joseph39 commented 11 years ago

Looks good.

mhyee commented 11 years ago

I've pushed a few commits fixing this. PGIA is probably as good as IGIA now. I'll have to run more tests to be sure, but that should probably wait until the current batch is done.

Any more comments @cpkleynhans?

cpkleynhans commented 11 years ago

LGTM