[isabelle-dev] Duraraion of AFP session AODV
tim at tbrk.org
Thu Nov 27 09:43:50 CET 2014
* Makarius <makarius at 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
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
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 473 bytes
Desc: Digital signature
More information about the isabelle-dev