[isabelle-dev] Duraraion of AFP session AODV

[Timothy Bourke]

* 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
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.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 473 bytes
Desc: Digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20141127/844bdb6e/attachment.sig>