* Makarius <makar...@sketis.net> [2014-11-26 21:43 +0100]: > On Wed, 26 Nov 2014, Florian Haftmann wrote: > >How long is session AODV expected to run on a machine such as lxbroy10? > >It seems to exceed JinjaThreads significantly… > > Quite impressive, isn't it? One of my local caches has this timing: > elapsed=10142.147 cpu=38679.631 gc=3478.939
Sadly, the cause of this long runtime is not very satisfactory. The development includes a single main model with associated invariant proofs and five variant models each with updated proofs. The protocol model only changes slightly in each variant and only a few lemmas usually require updating to reestablish the main property. We untangled as many dependencies as we could, but ultimately we did not find a better solution than copy-paste-modify. We tried to minimize changes between the variants so that a diff only shows relevant changes. This idea of variant models seems quite natural to me—one of the advantages of mechanising such models and proofs is the ease of experimenting with variations to the model—and I think it would be worthwhile to solve the problem properly but I do not have any good ideas for the present. That said, the basic proof is itself quite computationally intensive. There are two causes: 1. The invariant approach produces a subgoal for each 'significant' subterm in the model (~130). These subgoals are independent (no schematic variables), and the proof time was reduced from about 4 hours to about 25 minutes by exploiting PARALLEL_GOALS and some other simple optimisations (like running a 'shallow' simplification pass) in a custom tactic. The parallelization in Isabelle is a boon for (Floyd/Manna/Pnueli-style) invariant proofs of reactive systems models. 2. A handful of the sledgehammer generated proofs are quite intensive. I would like to fix these by doing more manual work (i.e., more steps in Isar), I just have to find the time. Tim.
signature.asc
Description: Digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
