[PPL-devel] Bugs in OCaml interface
Kenneth MacKenzie
kwxm at inf.ed.ac.uk
Thu Apr 2 16:40:38 CEST 2009
Enea Zaffanella writes:
>
> The snapshot with the corrections is now ready:
> ftp://ftp.cs.unipr.it/pub/ppl/snapshots/
Hi Enea,
The problems with the OCaml interface have now gone away (thanks!),
and I can confirm that my problem with the
ppl_Polyhedron_BHRZ03_widening_assign function has nothing to do with
the OCaml interface. I extracted the polyhedra that were causing
problems (they have 60 and 81 constraints) and fed them to the C++
version of the widening function. It's now been running for 14 hours
without terminating. However, your suggestion of using a timer to
escape and use the H79 widening instead seems to work well.
I did have a couple of problems with the snapshot. I changed to the
ppl/doc directory and tried
[5~ make ppl-user-configured-ocaml-interface-0.10.1pre10-html
but it failed because it couldn't find something it needed from gmp.
This is due to the fact that I had to install gmp in a subdirectory of
my home directory, but the makefile was looking in one of the
standard directories:
OCAMLDOC_HTML_OPTIONS = \
-I +gmp -I $(top_builddir)/interfaces/OCaml -html
OCAMLDOC_LATEX_OPTIONS = \
-I +gmp -I $(top_builddir)/interfaces/OCaml \
-latex -noheader -notrailer -notoc
I changed the +gmp to the location of my version of gmp and it worked
properly. I had other problems for the same reason a while ago and
someone added --with-libgmp and --with-libgmpxx-prefix options to the
top-level configure script, so presumably these should also be used
here.
I also ran "make check", and it failed after 4 hours with
make check-TESTS
make[6]: Entering directory
`/disk/scratch/ppl-0.10.1pre10/interfaces/OCaml/tests'
./test1: error while loading shared libraries: libgmpxx.so.4: cannot
open shared object file: No such file or directory
FAIL: test1
./ppl_ocaml_generated_test: error while loading shared libraries:
libgmpxx.so.4: cannot open shared object file: No such file or
directory
FAIL: ppl_ocaml_generated_test
./test1_opt: error while loading shared libraries: libgmpxx.so.4:
cannot open shared object file: No such file or directory
FAIL: test1_opt
./ppl_ocaml_generated_test_opt: error while loading shared libraries:
libgmpxx.so.4: cannot open shared object file: No such file or
directory
FAIL: ppl_ocaml_generated_test_opt
======================================
4 of 4 tests failed
Please report to ppl-devel at cs.unipr.it
======================================
make[6]: *** [check-TESTS] Error 1
make[6]: Leaving directory
`/disk/scratch/ppl-0.10.1pre10/interfaces/OCaml/tests'
make[5]: *** [check-am] Error 2
make[5]: Leaving directory
`/disk/scratch/ppl-0.10.1pre10/interfaces/OCaml/tests'
make[4]: *** [check-recursive] Error 1
make[4]: Leaving directory
`/disk/scratch/ppl-0.10.1pre10/interfaces/OCaml'
make[3]: *** [check] Error 2
make[3]: Leaving directory
`/disk/scratch/ppl-0.10.1pre10/interfaces/OCaml'
make[2]: *** [check-recursive] Error 1
make[2]: Leaving directory `/disk/scratch/ppl-0.10.1pre10/interfaces'
make[1]: *** [check] Error 2
make[1]: Leaving directory `/disk/scratch/ppl-0.10.1pre10/interfaces'
make: *** [check-recursive] Error 1
Again, it appears that it's not looking in the right place.
Here's my config.log if you need it:
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
-------------- next part --------------
Best wishes,
Kenneth
[In reply to this:]
> > --------------------------------------------------------------------------------
> >
> > 1. The OCaml 'unit' type has only a single value, denoted (); this is
> > represented internally by a pointer to a single preallocated value.
> > However, many of the functions in the PPL interface return the wrong value.
> [...]
> > Every function returning a unit value (it looks like there are 509 of
> > them) should look like this. I don't think this bug is very harmful
> > unless one uses unit values in unusual ways.
>
> This should be fixed now (I counted and corrected 520 occurrences, if I
> remember well.)
>
> > 2. Certain functions can lead to segmentation errors. Here's a
> > program which creates a polyhedron and then loops round adding
> > constraints one by one.
>
> This should be fixed too: we are now almost systematic in registering
> values to the GC ... even when there is no actual need (up to my
> understanding).
>
> > 3. I've also had problems with ppl_Polyhedron_BHRZ03_widening_assign.
> > Occasionally my compiler locks up with a lot of CPU usage when
> > ppl_Polyhedron_BHRZ03_widening_assign is called. I didn't have any
> > probelms using the H79 widening instead. I'm not sure what's causing
> > this: ppl_Polyhedron_BHRZ03_widening_assign does have the problem with
> > units mentioned in (1) above, but I don't think that should do any
> > damage. It's possible that I have some malformed data structures from
> > (2) which are causing problems.
>
> In this case I am not sure it was a problem of the OCaml interface.
>
> Depending on the input polyhedra (hence, not easily predictable), the
> BHRZ03 widening might bump into an exponential computation that is
> avoided by the H79 widening: it that is the case, you could observe wild
> variations on the overall computation times. Note that even the opposite
> case is possible (even though it should occur much less often), since a
> chain of widening computations does not respect the usual monotonicity
> properties, so that a more precise widening could result in a less
> precise final post-fixpoint and computation times become quite
> unpredictable.
>
> Now that we also have the timeout functions available, I can suggest the
> following approach:
>
> 1) copy the polyhedron ph to be widened to ph_copy;
> 2) set a timeout;
> 3) try using the BHRZ03 widening on ph;
> 4) if the computation stops before the timeout expires, reset the
> timeout and get rid of the previous copy (now useless);
> 5) otherwise, if the timeout expires, you will obtain a
> PPL_timeout_exception; you can then replace the polyhedron ph with the
> copy you saved in step 1 and re-try using the H79 widening.
>
> We tried this (in C++) and in our context was working fairly well.
>
> The code for using the timeout is similar to the following
> (apologies for the awfully looking and untested OCaml code ... I never
> coded in OCaml before):
>
> print_string "Set timeout and use BHRZ03\n";
> ppl_set_timeout 100; (* 100 hsec *)
> try
> compute_something_using_BHRZ03 ph;
> ppl_reset_timeout ();
> print_string "BHRZ03 computation succeeded\n"
> with
> | PPL_timeout_exception ->
> ppl_reset_timeout ();
> print_string "Timeout expired: retrying using H79\n";
> ppl_Polyhedron_swap ph, ph_copy;
> compute_something_using_H79 ph
> | _ ->
> print_string "Unexpected exception\n"
>
> Also see PPL test file interfaces/OCaml/tests/test1.ml, looking for the
> code below the comment (* Testing timeouts *).
>
>
> > 4. While looking at the code for
> > ppl_Polyhedron_BHRZ03_widening_assign I noticed a bug in
> > ppl_Polyhedron_BHRZ03_widening_assign_with_tokens, which is repeated
> > in all the widening-with-tokens functions:
>
> Should be fixed (thanks a lot for the detailed explanation).
>
>
> > 5. It's not really a bug, but I'm a little confused by the way
> > the code is divided into modules. Ppl_ocaml_globals contains
> > the type definitions for various datatypes, but why does it also
> > contain all the MIP functions? I see that the OCamldoc-generated
> > documentation only contains information about Ppl_ocaml_globals,
> > but Ppl_ocaml is missing, so there's no information available
> > about the types of the polyhedron functions and other things
> > in Ppl_ocaml.
>
> I have added a note to the manual in this respect.
> Briefly, since we do not want to force people to install the OCaml
> tools, we have two manuals: a configuration dependent and a
> configuration independent one. In the configuration independent one we
> only list those features that are available no matter what domain
> instances are selected (when the Ocaml interface is enabled): this also
> includes MIP_Problem. Hence, I suggest you look to the configuration
> dependent manual. In order to build it, you should cd into the ppl/doc
> directory and issue
>
> make ppl-user-configured-ocaml-interface-0.10.1pre10-html
>
> Also note that the Ppl_ocaml_globals module is automatically included in
> module Ppl_ocaml.
>
> > Also, the documentation for the OCaml interface (for example, at
> >
> > http://www.cs.unipr.it/ppl/Documentation/user/ppl-user-ocaml-interface-0.10-html/ )
> >
> > refers to a number of functions such as ppl_reset_timeout which
> > don't actually occur in the interface.
>
> You are right, these were missing.
> We now have added them (together with a few others).
>
> Let us know how it goes.
>
> Cheers,
> Enea.
>
>
More information about the PPL-devel
mailing list