Re: [isabelle] Failing afp-2015 build



On Tue, 17 Nov 2015, Lars Hupel wrote:

(What is the point of running single-threaded these days?)

I only discovered that as part of my investigations into how to reliably build the AFP. There are essentially two axes for parallelism: Internal to a session (multi-threaded, e.g. parallel proofs, parallel theories) and between sessions (multi-process, i.e. independent AFP sessions can be run in parallel).

Sequentialism is indeed a very atypical situation, more than 10 years of multicore hardware becoming mainstream.


In the various different isatest configurations for main Isabelle (not AFP) we do indeed test normal situations, like threads=4 or threads=8, alongside with abnormal ones like threads=1 or skip_proofs=true.

Such tests provide empirical evidence that the "physics" of a highly-complex parallel ML and proof engine comes out as reliably "mathematics", i.e. results are determined. Asking for determinism in every respect is a bit much.


Gerwin and I suspect that it would be most efficient to exploit the latter on the cost of the former, since the AFP dependency graph is quite sparse.

What always happens in such situations is that the total runtime converges to the longest sequential task. That used to be JinjaThreads, now it is AODV or ConcurrentGC. These take many hours CPU time. With a good multicore machine of 2015, it should be possible to run all of Isabelle + AFP in approximately 1h elapsed time, maybe even less after some tweaking.


	Makarius





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