[isabelle-dev] Performance of datatype_new

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Fri Mar 14 01:42:16 CET 2014

I would like to add a fourth remark, mostly for the record:

>> macpro ad6bd8030d88
>> $ isabelle build -c -D Datatype_Test
>> Finished Datatype_Test_Old (0:14:31 elapsed time, 0:27:18 cpu time, factor 1.88)
>> Finished Datatype_Test_New (0:05:11 elapsed time, 0:10:47 cpu time, factor 2.08)
> [...]
>> The first observation is that datatype_new is actually faster!  Are there further observations from early adopters of what is actually a quite advanced definitional tool suite awaiting the release this summer.
> Here are some more observations:
> 3. But for nested datatypes, "datatype_new" is usually faster because of its truly modular approach to nesting. The IsaFoR benchmarks above are revealing in this respect. There's a 5-way mutual recursion in it, but with nesting. With the old "datatype", the nesting gets expanded into a 16-way mutual recursion (IIRC), which explains why "datatype_new" wins by such a margin.

4. If the user knows that there will never be any nested recursion through a type variable (in a close-world assumption), they can "kill" the type variable using the funny "-:" syntax. This speeds up the BNF operations, because each variable that is killed reduces the arity of the main involved BNFs by 1 (arity n = the map function takes n + 1 arguments, the relator takes n + 2 arguments, there are n set functions). In particular, if the user kills all type variables, the result is a trivial, nullary BNF, for which no closure properties need to be proved. For the IsaFoR benchmarks, it turns out that one can kill all three type variables in the biggest types (see attachment), and this truncates the processing time by more than half. Dmitriy's latest timings (from Wednesday, using an unidentified post-ad6bd8030d88 version of Isabelle) are given below:

    Running Datatype_Old ...
    Datatype_Old: theory IsaFoR_Datatypes
    Timing Datatype_Old (8 threads, 773.807s elapsed time, 1457.962s cpu time, 400.774s GC time, factor 1.88)
    Finished Datatype_Old (0:12:57 elapsed time, 0:24:20 cpu time, factor 1.87)

    Running Datatype_New ...
    Datatype_New: theory IsaFoR_Datatypes_New
    Timing Datatype_New (8 threads, 273.182s elapsed time, 610.462s cpu time, 208.571s GC time, factor 2.23)
    Finished Datatype_New (0:04:37 elapsed time, 0:10:13 cpu time, factor 2.21)

    Running Datatype_New_Kill ...
    Datatype_New_Kill: theory IsaFoR_Datatypes_New_Killed
    Timing Datatype_New_Kill (8 threads, 101.160s elapsed time, 235.433s cpu time, 32.940s GC time, factor 2.33)
    Finished Datatype_New_Kill (0:01:44 elapsed time, 0:03:58 cpu time, factor 2.28)


-------------- next part --------------
A non-text attachment was scrubbed...
Name: IsaFoR_Datatypes_New_Killed.thy
Type: application/octet-stream
Size: 19646 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140314/8771ce56/attachment-0002.obj>

More information about the isabelle-dev mailing list