Re: [isabelle] Failing afp-2015 build

We have analysed the problem:
It appears in both, Isabelle2015 and Isabelle 40ca618e1b2d.

  The behaviour of PARALLEL_GOALS may differ depending on whether there
is one or more threads. It seems nowhere documented what are the
constraints such that the behaviour for the parallel and sequential case
matches, except a NEWS-file entry from 2011, which talks about no
schematic variables and "uniform" behaviour.

The "vcg_jackhammer" tactic implemented in ConcurrentGC seems to run in
one of the cases with different behaviour, and thus triggers the
observed error.

It is unclear whether the problem lies in the jackhammer-tactic or the
PARALLEL_GOALS combinator. In any case, the current state is very
unfortunate, as proof methods may behave differently depending on the
number of threads. 

In my opinion, the PARALLEL_GOALS-tactics should completely hide the
effects of parallelism from the user, even if this means some slowdown
in the sequential case (Note: Removing the optimization for the
sequential case in PARALLEL_GOALS, and using the same map-reduce
approach with retrofitting as in the parallel case, fixes the problem in


On Mi, 2015-11-11 at 22:17 +0100, Lars Hupel wrote:
> > * it's still running on my machine, but the build has progressed well
> > beyond "TSO"
> Update: Build has finished on my quad-core Core i7.
> Timing ConcurrentGC (4 threads, 3055.987s elapsed time, 7458.113s cpu
> time, 643.593s GC time, factor 2.44)
> Finished ConcurrentGC (0:51:48 elapsed time, 2:05:59 cpu time, factor 2.43)
> Finished at Wed Nov 11 21:58:23 CET 2015
> 0:51:52 elapsed time, 2:06:15 cpu time, factor 2.43
> It is still running on an 8 core "cloud" machine, but that one has also
> progressed beyond "TSO".

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.