Re: [isabelle-dev] Remaining uses of Proof General?
Thanks Makarius. A few of us at NICTA have ported this change to our various versions of Isabelle and begun playing with it. It seems to improve the situation sometimes, though we haven't yet got a feel for when in particular it helps. In fact, we haven't really understood what the change does. On 07/05/14 22:59, Makarius wrote: On Mon, 5 May 2014, Makarius wrote: Users running on batteries might also want a mode that restricts all threads to the behaviour above. Have you tried that with threads = 1 (there is also a special treatment for high-priority prints in that mode)? So far I guess that most people run with defaults, without any idea of the tuning parameters. See also: changeset: 56875:f6259d6fb565 user:wenzelm date:Tue May 06 16:05:14 2014 +0200 files: etc/options src/Pure/PIDE/command.ML description: explicit option parallel_print to downgrade parallel scheduling, which might occasionally help for big and heavy scripts; In principle this is an instance of the too many options syndrome, but here the implicit change of behaviour on 1 core is merely made explicit. Moreover, according to the waterbed-syndrome in its positive sense, it means that options added here inevitably cause other old/obsolete options to be removed faster. I completely agree that having too many options is a problem. There's no point having them if noone knows that they're there, or which ones to try. That said, I think it's a good path for performance adjustments which might or might not be helpful. I suspect you could get away with adding far more options than you plan to have in the end, and keep only the ones that end up with a quorum of users. I'm a bit of an optimist though. This sounds a bit too pragmatic and opportunistic to me. What is special about print tasks anyway, apart from their priority? The recent concept for asynchronous print functions makes print tasks rather general, and there are more automated provers or disprovers in that category than actual printing. What is even more important than prints, is the main protocol thread, which presently needs to work against the whole farm of worker threads to update certain administrative structures of the document model. If I knew a proper way to reduce the priority (or to pre-empt) worker threads for that, I would do it. But it probably needs some work by David Matthews on the ML thread infrastructure. Consider me an unashamed pragmatist. I see a similarity between task/thread scheduling in Isabelle and task/thread scheduling in operating systems. All modern operating systems are full of ad-hoc heuristics designed to bump up the priority of tasks that are likely to create I/O requests or update things for the user. A parallel make, for instance, will run much faster if the OS prioritises the compile tasks that are still reading files ahead of the ones that have begin compiling and computing. This keeps the disk working throughout the build. Windows raises the priority of in-focus windows, and Mac OS X pushes the audio threads of apps up to the highest priority, etcetera. I may have misspoken with regard to print task. I guess I meant task that will produce output which at some point the user has directly requested into their output panel, query panel etc. If we see the user as an external resource like a hard disk, these are the tasks we need to front-load to keep the external task running at full capacity. I see the some of the other output tasks, which possibly produce counterexamples or which produce squiggly lines which are possibly helpful, as lower priority. Preempting long-running tasks would change the tradeoffs a lot. Another possibility would be to introduce a yield-point (cooperative multitasking) which a task can execute, which will possibly cause its execution to be delayed in favour of a higher priority task. Adding that to the tactic combinators would make nearly all Isabelle workloads much finer-grained. Well, those are just my thoughts. Thanks for the adjustment, I hope it solves our responsiveness problems. Best wishes, Thomas. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of Proof General?
On Thu, 8 May 2014, Thomas Sewell wrote: If I knew a proper way to reduce the priority (or to pre-empt) worker threads for that, I would do it. But it probably needs some work by David Matthews on the ML thread infrastructure. Consider me an unashamed pragmatist. The important point is that a system like Isabelle cannot be built on the basis of pragmatism. It is occasionally helpful to recall the cultural foundations on which one is standing. The system can be used pragmatically, or rather practically, of course. I see a similarity between task/thread scheduling in Isabelle and task/thread scheduling in operating systems. All modern operating systems are full of ad-hoc heuristics designed to bump up the priority of tasks that are likely to create I/O requests or update things for the user. Definitely. I've introduced the slogan of Isabelle as logical operating system already in 2007, when the parallel batch mode with its ML threads was still new. Many years later that has become reality in PIDE interaction, but it was much harder to get there than anticipated. In recent years I have become more cautious in the ambitions of what the system is meant to do. It is already too far ahead of anything else in the ITP world, and hardly anyone understands how it really works. A parallel make, for instance, will run much faster if the OS prioritises the compile tasks that are still reading files ahead of the ones that have begin compiling and computing. This keeps the disk working throughout the build. Luckily Isabelle no longer depends on make and its many historical problems. The Isabelle build tool is fast, because it does not access all these files over and over again. Thus the need for extra tricks is avoided, by giving up old habits from the 1970-ies. Preempting long-running tasks would change the tradeoffs a lot. Another possibility would be to introduce a yield-point (cooperative multitasking) which a task can execute, which will possibly cause its execution to be delayed in favour of a higher priority task. Adding that to the tactic combinators would make nearly all Isabelle workloads much finer-grained. That sounds rather obvious, but also like even more complication. David Matthews has provided a nice simplified version of pthreads in Poly/ML. He could probably do more, but even on the more complex JVM the influence on thread scheduling is limited. My canonical approach in such situations is to ask: Is there a way to avoid the need for all that extra weight? It requires looking at concrete applications carefully, to disprove their approach as something that could be done differently, with less impact on resources. That is not pragmatic, but it is how genuine scientific progress usually works. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Isabelle root access
On Thu, 8 May 2014, mta-proj wrote: die Gruppe isabelle, in der Sie Mitglied sind, wurde mit desharna,fleury erweitert Membership of the isabelle Unix group means full root access to many administrative resources. Usually neither the one who grants the rights nor the one who receives them knows what that means. So just the canonical questions: Who is responsible for these users? What are their projects within Isabelle? 15 years ago, I started myself this strange tradition to re-use the one isabelle group for any kind of shared resource management within the network file-system at TUM. That was at a time with approx. 7 people total in 2-3 adjacent offices, so it was rather obvious who was responsible for what. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle root access
Hi Makarius, Am 08.05.2014 um 12:32 schrieb Makarius makar...@sketis.net: On Thu, 8 May 2014, mta-proj wrote: die Gruppe isabelle, in der Sie Mitglied sind, wurde mit desharna,fleury erweitert Membership of the isabelle Unix group means full root access to many administrative resources. Usually neither the one who grants the rights nor the one who receives them knows what that means. So just the canonical questions: Who is responsible for these users? What are their projects within Isabelle? I sent an email ahead of time, but now I realize I sent it to the wrong mailing list (isabelle-group instead of isabelle-dev). So here is the description: * * * The isabelle group has been (or will be shortly) extended with two new users, both of them working as summer interns under my (co)supervision: Martin Desharnais (co-supervisor: Dmitriy Traytel) Mathias Fleury They will need to push changes to the (co)datatypes resp. Sledgehammer. More specifically, Martin will enrich the list of theorems generated by the new (co)datatype package, and Mathias will integrate Sledgehammer better with some more exotic ATPs (e.g. Zipperposition, veriT, LEO-II, Satallax). * * * Sorry for the mixup. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of Proof General?
On 08/05/2014 11:25, Makarius wrote: On Thu, 8 May 2014, Thomas Sewell wrote: If I knew a proper way to reduce the priority (or to pre-empt) worker threads for that, I would do it. But it probably needs some work by David Matthews on the ML thread infrastructure. Preempting long-running tasks would change the tradeoffs a lot. Another possibility would be to introduce a yield-point (cooperative multitasking) which a task can execute, which will possibly cause its execution to be delayed in favour of a higher priority task. Adding that to the tactic combinators would make nearly all Isabelle workloads much finer-grained. That sounds rather obvious, but also like even more complication. David Matthews has provided a nice simplified version of pthreads in Poly/ML. He could probably do more, but even on the more complex JVM the influence on thread scheduling is limited. I've had a look at providing thread priority in the Poly/ML thread package and I may have a go at including something. Poly/ML leaves thread scheduling to the pthreads library which really means to the OS and what is available depends on the particular OS. In general pthreads allows control over both priority and scheduling policy. I've done some tests on what various OSs allow for user (i.e. non-privileged) threads. Linux. Does not allow either policy or priority to be changed. Mac OS X. Allows both policy and priority to be changed. Cygwin/Windows. Single scheduling policy. Allows priority to be changed. FreeBSD. Allows priority but not policy to be changed. What this means is that ML code that wants to set a thread priority is going to have to make some enquiries about the priority range allowed. It looks as though adding a yield function would not be hard. There's a question about whether you would really want to use it. There is a cost involved even if there is no other thread that can be scheduled so you wouldn't want to call it too often. David ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
