Re: [isabelle] Problems with code generation for the reals



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.