*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] Problems with code generation for the reals*From*: Jesus Aransay <jesus-maria.aransay at unirioja.es>*Date*: Mon, 29 Apr 2013 17:53:57 +0200*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <517BCC93.50808@informatik.tu-muenchen.de>*References*: <CAL0S8BfPE0=UT6e-zryCwvYqXaL99E7rNnbMZxnHUASJ4tFwig@mail.gmail.com> <517BCC93.50808@informatik.tu-muenchen.de>*Sender*: jmaransay at gmail.com

Dear all, regarding the mail I sent to Florian, I just wanted to add some figures about the performance of our algorithm computing the reduced row echelon form of a matrix; the algorithm is refined to "iarrays" (http://isabelle.in.tum.de/library/HOL/HOL-Library/IArray.html) to represent matrices. We implemented the algorithm over fields, and generated the ML code associated to the algorithm. We used MLton to compile the code and execute it over some instances of matrices; the results obtained when profiling are the following ones. The following example is a randomly generated matrix of dimension 70*70 matrix with entries in the field "Z / 2Z"; these elements are generated to "0::IntInf.int" and "1::IntInf.int", and the field operations are defined by means of ad - hoc "fun" definitions (execution time is 0.02 seconds). (* 0.02 seconds of CPU time (0.00 seconds GC) function cur raw --------------------------- ----- ------- Sequence.tabulate 50.0% (0.01s) example_70_x_70_Z2.plus_z2a 50.0% (0.01s) *) The following are the results obtained for the very same matrix as in the previous example, but now the elements are labelled as being of type "real"; following the standard setup for code generation of reals they are generated in SML to fractions of "IntInf.int" (execution time gets multiplied by 100, most of the time is spent in computing quotients and remainders): (* 2.46 seconds of CPU time (0.03 seconds GC) function cur raw -------------------------------------------- ----- ------- Primitive.IntInf.bigQuot 28.1% (0.70s) Primitive.IntInf.bigRem 28.1% (0.70s) Primitive.IntInf.bigDivMod 12.4% (0.31s) Primitive.IntInf.make 12.0% (0.30s) example_70_x_70_binary_rat.abs_int 5.2% (0.13s) example_70_x_70_binary_rat.sgn_int 3.6% (0.09s) example_70_x_70_binary_rat.gcd_int 2.8% (0.07s) example_70_x_70_binary_rat.divmod_int 2.0% (0.05s) example_70_x_70_binary_rat.mod_int 1.6% (0.04s) <gc> 1.2% (0.03s) Sequence.tabulate 1.2% (0.03s) example_70_x_70_binary_rat.div_int 0.4% (0.01s) example_70_x_70_binary_rat.divmod_int.fn 0.4% (0.01s) example_70_x_70_binary_rat.apsnd 0.4% (0.01s) example_70_x_70_binary_rat.mult_iarray.fn.fn 0.4% (0.01s) *) Finally, this third example is the result of applying the algorithm to a randomly generated "70*70" matrix, but in this case of real numbers between 0 and 1000; they are again generated in SML to fractions of "IntInf.int": (* 46.14 seconds of CPU time (1.19 seconds GC) function cur raw --------------------------------- ----- -------- Primitive.IntInf.bigRem 32.5% (15.37s) Primitive.IntInf.bigQuot 24.2% (11.46s) Primitive.IntInf.make 11.3% (5.37s) Primitive.IntInf.bigDivMod 9.5% (4.51s) example_70_x_70_rat.sgn_int 7.6% (3.62s) example_70_x_70_rat.abs_int 6.1% (2.87s) example_70_x_70_rat.divmod_int 2.9% (1.35s) <gc> 2.5% (1.19s) example_70_x_70_rat.gcd_int 1.4% (0.65s) example_70_x_70_rat.mod_int 0.9% (0.43s) example_70_x_70_rat.divmod_int.fn 0.7% (0.34s) example_70_x_70_rat.apsnd 0.3% (0.12s) Sequence.sub 0.0% (0.01s) example_70_x_70_rat.plus_rata 0.0% (0.01s) example_70_x_70_rat.uminus_rata 0.0% (0.01s) example_70_x_70_rat.div_int 0.0% (0.01s) Primitive.IntInf.extdFromWord32 0.0% (0.01s) *) We thought that, in order to increase performance, it could be a good idea to try to use the SML "Real" type (as proposed in http://isabelle.in.tum.de/library/HOL/HOL-Library/Code_Real_Approx_By_Float.html), instead of fractions of "IntInf.int". Any other ideas would be also warmly welcome. Any suggestions are welcome, Jesus On Sat, Apr 27, 2013 at 3:03 PM, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote: > Hi Jesus, >... > > To get back to your original observation: > >> we had been doing some experiments with >> real numbers represented in SML by fractions of elements of type >> "IntInf.int", but doing some profiling we detected that most of the >> execution time was spent in computing the functions "gcd", "divmod", >> "quotrem", "normalize" and so on, instead of on performing the >> operations over matrices that were really interesting for us. > > It is indeed questionable whether it is a good idea to normalize > quotients always. What do others implementations do here (e.g. Ocaml)? > The implementation of rational numbers can be changed in user space > using the usual mechanisms of datatype refinement (see the tutorial on > code generation and the upcoming ITP paper > http://isabelle.in.tum.de/~haftmann/pdf/data_refinement_haftmann_kuncar_krauss_nipkow.pdf). > > Hope this helps, > Florian > > -- > > PGP available: > http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de > -- Jesús María Aransay Azofra Universidad de La Rioja Dpto. de Matemáticas y Computación tlf.: (+34) 941299438 fax: (+34) 941299460 mail: jesus-maria.aransay at unirioja.es ; web: http://www.unirioja.es/cu/jearansa Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logroño, España

**References**:**Re: [isabelle] Problems with code generation for the reals***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] No tail-recursive code equation for List.map
- Next by Date: [isabelle] Probelm with the "definition" command
- Previous by Thread: Re: [isabelle] Problems with code generation for the reals
- Next by Thread: [isabelle] Probelm with the "definition" command
- Cl-isabelle-users April 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list