> The parallelization strategy that I ended up with is speculation along > the "failed" branch of the search tree. So what C-Reduce does it to > keep, at all times, $NPROCS concurrent delta tests running along this > branch. As long as transformations fail to produce interesting results, > this is all good. As soon as an interesting result is found (i.e., > C-Reduce prints "success") all speculative processes are killed and a > fresh batch are forked off.
When I run Berkley delta, I often see that success results are clustered, i.e. there are sequences of success results interleaved with sequences of failures. I think your strategy might be suboptimal for this case. Also you probably should switch to sequential execution when predicate becomes fast (e.g., faster than hard-coded or configurable threshold) -- Regards, Konstantin
