Email Gateway (Aug 19 2022 at 15:30): Email Gateway (Aug 19 2022 at 15:30):From: Lars Noschinski <noschinl@in.tum.de>
Something I noticed just now: On my machine (a quad-core i7), starting
sledgehammer (with 3 provers, from the panel) keeps the rest of the
prover from making progress. Processing the document only resumes when
sledgehammer finishes (I guess it completely exhausts the worker pool?).
Email Gateway (Aug 19 2022 at 15:30):From: Makarius <makarius@sketis.net>
As far as I understand sledgehammer it should use normal future forks
(via Par_List.map) and thus participate in the global worker thread pool.
The size of that is determined by the system option "threads", which is 0
by default, and thus determined from the hardware. You can use check this
in Isabelle/ML via Multithreading.max_threads_value. You should get 4
here, although there are i7 versions with only 2 cores.
The PIDE sledgehammer panel invokes it as "query operation", as can be
seen here:
This formally documents the particular modes and parameters given to
sledgehammer. Only Jasmin understands all details of that.
With 3 provers there should be at most 3 tasks per sledgehammer invocation
-- of course there could be more than one active sledgehammer panel. The
task priority is 0, and thus higher than the -1 for forked proofs. In
addition, there could be slow "print_state" tasks at priority 1 saturating
the queue.
Makarius
Email Gateway (Aug 19 2022 at 15:32):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
As far as I understand sledgehammer it should use normal future forks (via Par_List.map) and thus participate in the global worker thread pool.
With the Sledgehammer panel, all threads should participate in the global worker thread pool, with the potential exception of a single MaSh learning thread (occasionally -- e.g. the first time you launch Sledgehammer and MaSh has no accumulated state) -- the MaSh threads are managed using the old "asynchronous manager" mechanism, that is also used when invoking the "sledgehammer" command from the proof text.
It would be useful to know if the problem also occurs when (1) MaSh is not run and (2) no proofs are found (and hence no proof minimization etc. and hence no "Par_List" operations, IIRC). Adding
sledgehammer_params [mepo]
at the top of your theory should take care of (1).
Jasmin
Email Gateway (Aug 19 2022 at 15:33):From: Lars Noschinski <noschinl@in.tum.de>
When I add "sledgehammer_params [mepo]" before the place where I call
sledgehammer, the problem persists. Also, all provers timed out, so the
problem occurs also with (2).
Email Gateway (Aug 19 2022 at 15:33):From: Makarius <makarius@sketis.net>
On Fri, 22 Aug 2014, Lars Noschinski wrote:
On 22.08.2014 12:32, Jasmin Christian Blanchette wrote:
As far as I understand sledgehammer it should use normal future forks
(via Par_List.map) and thus participate in the global worker thread
pool.
With the Sledgehammer panel, all threads should participate in the
global worker thread pool, with the potential exception of a single
MaSh learning thread (occasionally -- e.g. the first time you launch
Sledgehammer and MaSh has no accumulated state) -- the MaSh threads are
managed using the old "asynchronous manager" mechanism, that is also
used when invoking the "sledgehammer" command from the proof text.
In the worst case that extra thread would suck up more CPU cycles than
specified in the nominal "threads" option, but it should not stop regular
future tasks from running, like the ones for forked proofs.
It would be useful to know if the problem also occurs when (1) MaSh is
not run and (2) no proofs are found (and hence no proof minimization
etc. and hence no "Par_List" operations, IIRC). Addingsledgehammer_params [mepo]
at the top of your theory should take care of (1).
When I add "sledgehammer_params [mepo]" before the place where I call
sledgehammer, the problem persists. Also, all provers timed out, so the
problem occurs also with (2).
It is still unclear to me what the problem is. What does
Multithreading.max_threads_value () say? How is the task farm pupulated?
The improved Monitor dockable in Isabelle2014-RC4 might provide some
clues.
We have only a few days left to figure out if there is a remaining problem
or not. The month of August ends next week, and the final roll-out of
Isabelle2014 will happen before that.
Makarius
Email Gateway (Aug 19 2022 at 15:34):From: Lars Noschinski <noschinl@in.tum.de>
Multithreading.max_threads_value () is 4. I made a video of what I am
experiencing. Notice that the pink background goes away immediately when
I cancel sledgehammer:
http://www21.in.tum.de/~noschinl/ml/sledgehammer-blocks.mp4
(Don't be alarmed by the mouse cursor offset problem -- it only occurs
in the video).
-- Lars
Email Gateway (Aug 19 2022 at 15:36):From: Makarius <makarius@sketis.net>
Thanks for the video. After watching it 2 times, I could see the pattern
when this sitation occurs, and managed to reproduce it without anything
particular from sledgehammer, just using some OS.Process.sleep dummies.
I am presently investigating the reasons for this behaviour of PIDE
document scheduling, which could well be just a normal consequence of
certain heuristics in task priorities that have accumulated over time.
For now: How would you rate the practical relevance and priority of this
issue? Is it just a minor oddity or outright a hindrance in practical
work?
Makarius
Email Gateway (Aug 19 2022 at 15:36):From: Lars Noschinski <noschinl@in.tum.de>
Somewhere in between. It is annoying since it essentially sequentializes
the behavior of the IDE, but it is no showstopper.
-- Lars
Email Gateway (Aug 19 2022 at 15:37):From: Makarius <makarius@sketis.net>
There is nothing special about the Isabelle2014 code base here. The
behaviour is the same in Isabelle2013-2.
It is a not fully finished aspect of parallel PIDE document processing:
some glimpses of that can be seen in my ITP 2014 paper, section 4 on the
"Execution Frontiers", which play on the safe side with linear semantic
concatenation of executions, giving away potential for parallelism.
Apart from some "asynchronous print functions" like Sledgehammer that come
out more sequential than anticipated, the bigger omission is the lack of
forked proofs that consist of more than a single 'by' command.
So the conclusion is that it is not a genuine problem, nor an erratic
breakdown. It just means that further improvements in that area are
postponed to a future release.
Makarius
Last updated: Apr 20 2024 at 08:16 UTC