July 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Use less simplistic weights.
by Roberto Bagnara 13 Jul '09

13 Jul '09

Module: ppl/ppl Branch: master Commit: 30c4076e092bff1bab33c1cf121f1100f1d73866 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=30c4076e092b… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Jul 13 21:48:50 2009 +0200 Use less simplistic weights. --- src/conversion.cc | 12 +++++++----- 1 files changed, 7 insertions(+), 5 deletions(-) diff --git a/src/conversion.cc b/src/conversion.cc index 13cd87e..1d8a373 100644 --- a/src/conversion.cc +++ b/src/conversion.cc @@ -409,7 +409,7 @@ PPL::Polyhedron::conversion(Linear_System& source, if (scalar_prod[index_non_zero] != 0) // The generator does not saturate the constraint. break; - WEIGHT_ADD(1); + WEIGHT_ADD(source_num_columns); // Check if the client has requested abandoning all expensive // computations. If so, the exception specified by the client // is thrown now. @@ -417,7 +417,7 @@ PPL::Polyhedron::conversion(Linear_System& source, } for (dimension_type i = index_non_zero + 1; i < dest_num_rows; ++i) { Scalar_Products::assign(scalar_prod[i], source_k, dest[i]); - WEIGHT_ADD(1); + WEIGHT_ADD(source_num_columns); // Check if the client has requested abandoning all expensive // computations. If so, the exception specified by the client // is thrown now. @@ -538,8 +538,8 @@ PPL::Polyhedron::conversion(Linear_System& source, dest_i.strong_normalize(); scalar_prod[i] = 0; // `dest' has already been set as non-sorted. + WEIGHT_ADD_MUL(4, dest_num_columns); } - WEIGHT_ADD(1); // Check if the client has requested abandoning all expensive // computations. If so, the exception specified by the client // is thrown now. @@ -711,6 +711,8 @@ PPL::Polyhedron::conversion(Linear_System& source, redundant = true; break; } + assert(bound >= num_lines_or_equalities); + WEIGHT_ADD(bound - num_lines_or_equalities); if (!redundant) { // Adding the new ray to `dest' and the corresponding // saturation row to `sat'. @@ -756,10 +758,10 @@ PPL::Polyhedron::conversion(Linear_System& source, scalar_prod[dest_num_rows] = Coefficient_zero(); // Increment the number of generators. ++dest_num_rows; - } + WEIGHT_ADD_MUL(4, dest_num_columns); + } // if (!redundant) } } - WEIGHT_ADD(1); // Check if the client has requested abandoning all expensive // computations. If so, the exception specified by the client // is thrown now.

1 0

[GIT] ppl/ppl(master): Comment improved.
by Roberto Bagnara 13 Jul '09

13 Jul '09

Module: ppl/ppl Branch: master Commit: f5b72e693fc901c6b03b4c735a8d0d85f4adbbbe URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f5b72e693fc9… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Jul 13 21:48:31 2009 +0200 Comment improved. --- src/assert.hh | 5 +++-- 1 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/assert.hh b/src/assert.hh index 54ae39a..f0eac9e 100644 --- a/src/assert.hh +++ b/src/assert.hh @@ -49,8 +49,9 @@ site: http://www.cs.unipr.it/ppl/ . */ } while(0) #endif -// The evaluation of asserted condition could have a non zero computational -// weight (i.e. the execution path could encounter a WEIGHT_ADD). +// The evaluation of asserted conditions could have a non zero +// computational weight (i.e., the execution path could contain an +// invocation of WEIGHT_ADD). #define PPL_ASSERT_HEAVY(cond__) \ do { \ ++Parma_Polyhedra_Library::Implementation::in_assert; \

1 0

[GIT] ppl/ppl(master): Added additional info about Traits template parameter.
by Abramo Bagnara 13 Jul '09

13 Jul '09

Module: ppl/ppl Branch: master Commit: f53a31830c3e65477d5856c92b2d3cb6f93ac1c5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f53a31830c3e… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Mon Jul 13 20:10:39 2009 +0200 Added additional info about Traits template parameter. --- Watchdog/src/Threshold_Watcher.defs.hh | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Watchdog/src/Threshold_Watcher.defs.hh b/Watchdog/src/Threshold_Watcher.defs.hh index 8d6200c..f5e67b2 100644 --- a/Watchdog/src/Threshold_Watcher.defs.hh +++ b/Watchdog/src/Threshold_Watcher.defs.hh @@ -31,8 +31,8 @@ site: http://www.cs.unipr.it/ppl/ . */ /*! \brief A class of watchdogs controlling the exceeding of a threshold. - \tparam Traits - FIXME + \tparam Traits class to set data types and functions for the + threshold handling. See \ref Weightwatch_Traits for an example. */ template <typename Traits> class Parma_Watchdog_Library::Threshold_Watcher {

1 0

[GIT] ppl/ppl(master): Converted weight threshold to unsigned long long.
by Abramo Bagnara 13 Jul '09

13 Jul '09

Module: ppl/ppl Branch: master Commit: a3b243ef0142dfb5e628301b64ec3095754cf297 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a3b243ef0142… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Mon Jul 13 18:46:47 2009 +0200 Converted weight threshold to unsigned long long. --- src/Weight_Profiler.defs.hh | 6 +++--- src/globals.defs.hh | 4 ++-- src/globals.inlines.hh | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Weight_Profiler.defs.hh b/src/Weight_Profiler.defs.hh index 5b67aa6..542156d 100644 --- a/src/Weight_Profiler.defs.hh +++ b/src/Weight_Profiler.defs.hh @@ -31,7 +31,7 @@ class Weight_Profiler { enum { DISCARDED = 0, VALID = 1 }; public: Weight_Profiler(const char* file, int line, - Weightwatch_Traits::Threshold delta, + Weightwatch_Traits::Delta delta, double tmin = 0, double tmax = 0) : file(file), line(line), delta(delta), tmin(tmin), tmax(tmax) { @@ -56,7 +56,7 @@ public: assert(r >= 0); } void end(unsigned int factor = 1) { - Weightwatch_Traits::weight += delta * factor; + Weightwatch_Traits::weight += (Weightwatch_Traits::Threshold) delta * factor; struct timespec start = stamp; begin(); double elapsed; @@ -87,7 +87,7 @@ public: private: const char *file; int line; - Weightwatch_Traits::Threshold delta; + Weightwatch_Traits::Delta delta; double tmin; double tmax; diff --git a/src/globals.defs.hh b/src/globals.defs.hh index ae45312..b36d575 100644 --- a/src/globals.defs.hh +++ b/src/globals.defs.hh @@ -95,10 +95,10 @@ compute_capacity(dimension_type requested_size, #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) struct Weightwatch_Traits { //! The type used to specify thresholds for computational weight. - typedef unsigned int Threshold; + typedef unsigned long long Threshold; //! The type used to specify increments of computational weight. - typedef unsigned int Delta; + typedef unsigned long long Delta; //! Returns the current computational weight. static const Threshold& get(); diff --git a/src/globals.inlines.hh b/src/globals.inlines.hh index b0f4d3c..fd1f749 100644 --- a/src/globals.inlines.hh +++ b/src/globals.inlines.hh @@ -40,7 +40,7 @@ Weightwatch_Traits::get() { inline bool Weightwatch_Traits::less_than(const Threshold& a, const Threshold& b) { - return b - a < 1U << (sizeof(Threshold)*8-1); + return b - a < 1ULL << (sizeof(Threshold)*8-1); } inline void

1 0

[GIT] ppl/ppl(master): Added weight profiler
by Abramo Bagnara 13 Jul '09

13 Jul '09

Module: ppl/ppl Branch: master Commit: f41bc98bc45b749497311b4a5a89678e3e96431c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f41bc98bc45b… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Mon Jul 13 18:36:51 2009 +0200 Added weight profiler --- src/Box.templates.hh | 1 + src/MIP_Problem.cc | 2 + src/Makefile.am | 2 + src/Weight_Profiler.cc | 74 +++++++++++++++++++++++++++++ src/Weight_Profiler.defs.hh | 109 +++++++++++++++++++++++++++++++++++++++++++ src/assert.hh | 3 + src/conversion.cc | 4 ++ src/globals.defs.hh | 52 ++++++++++++++++++++ src/globals.inlines.hh | 12 +---- 9 files changed, 248 insertions(+), 11 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=f41bc98b…

1 0

Re: [PPL-devel] Closed versus NNC polyhedra
by Roberto Bagnara 13 Jul '09

13 Jul '09

Tobias Grosser wrote: > On Thu, 2009-07-09 at 16:52 +0200, Michael Classen wrote: >>> They do not. However at the moment we are working on R^n. We should move >>> to integral polyhedron. >>> >>> Tobi >> You say that as if it is very easy... is there already a simple way of >> dealing with integral polyhedrons in PPL? If so, I should maybe tell >> Patricia that she shouldn't work too hard on this new datatype...? > > No. I am waiting for Patricia's work. I think this is the way to go. Hi there. Can you please explain what you mean by "integral polyhedron", "new datatype" and "Patricia's work"? Please do not be afraid to (re)state the obvious: I am sure there is one or more misunderstandings here. Cheers, Roberto -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

2 4

[GIT] ppl/ppl(master): In the Ocaml tests, timeouts are now reset unconditionally.
by Enea Zaffanella 13 Jul '09

13 Jul '09

Module: ppl/ppl Branch: master Commit: e5ea4dfdfcca314e4d9e1855868c560ac75ab6db URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e5ea4dfdfcca… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon Jul 13 17:39:45 2009 +0200 In the Ocaml tests, timeouts are now reset unconditionally. --- interfaces/OCaml/tests/test1.ml | 10 ++++++++++ 1 files changed, 10 insertions(+), 0 deletions(-) diff --git a/interfaces/OCaml/tests/test1.ml b/interfaces/OCaml/tests/test1.ml index 6acb1a0..5553cf1 100644 --- a/interfaces/OCaml/tests/test1.ml +++ b/interfaces/OCaml/tests/test1.ml @@ -419,6 +419,8 @@ and compute_timeout_hypercube dim_in dim_out = ) in ( begin + (* FIXME: in the following try/with, the timeouts should be reset + unconditionally. Is there a way to implement try/finally? *) try print_string_if_noisy "\nStarting ppl_reset_timeout test:\n"; ppl_set_timeout 100; @@ -427,9 +429,11 @@ in ( print_string_if_noisy "ppl_reset_timeout test succeeded.\n" with | PPL_timeout_exception -> + ppl_reset_timeout (); print_string_if_noisy "ppl_reset_timeout test seems to be failed:\n"; print_string_if_noisy "Unexpected PPL timeout exception caught.\n" | _ -> + ppl_reset_timeout (); print_string_if_noisy "ppl_reset_timeout test seems to be failed."; (* FIXME: print the contents of the exception. *) print_string_if_noisy "\n" @@ -443,9 +447,11 @@ in ( print_string_if_noisy "ppl_set_timeout test seems to be failed!\n" with | PPL_timeout_exception -> + ppl_reset_timeout (); print_string_if_noisy "ppl_set_timeout test succeded\n"; print_string_if_noisy "Expected PPL timeout exception caught.\n" | _ -> + ppl_reset_timeout (); print_string_if_noisy "ppl_set_timeout test failed:\n"; print_string_if_noisy "generic exception caught.\n" end; @@ -458,9 +464,11 @@ in ( print_string_if_noisy "ppl_reset_deterministic_timeout test succeeded.\n" with | PPL_timeout_exception -> + ppl_reset_deterministic_timeout (); print_string_if_noisy "ppl_reset_deterministic_timeout test seems to be failed:\n"; print_string_if_noisy "Unexpected PPL timeout exception caught.\n" | _ -> + ppl_reset_deterministic_timeout (); print_string_if_noisy "ppl_reset_deterministic_timeout test seems to be failed."; (* FIXME: print the contents of the exception. *) print_string_if_noisy "\n" @@ -474,9 +482,11 @@ in ( print_string_if_noisy "ppl_set_deterministic_timeout test seems to be failed!\n" with | PPL_timeout_exception -> + ppl_reset_deterministic_timeout (); print_string_if_noisy "ppl_set_deterministic_timeout test succeded\n"; print_string_if_noisy "Expected PPL timeout exception caught.\n" | _ -> + ppl_reset_deterministic_timeout (); print_string_if_noisy "ppl_set_deterministic_timeout test failed:\n"; print_string_if_noisy "generic exception caught.\n" end

1 0

[GIT] ppl/ppl(master): Drafted a few missing comments. To be completed ( by the author).
by Enea Zaffanella 13 Jul '09

13 Jul '09

Module: ppl/ppl Branch: master Commit: db905fa95a0e199beb2b9337869a2e27219060f8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=db905fa95a0e… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon Jul 13 16:21:35 2009 +0200 Drafted a few missing comments. To be completed (by the author). --- Watchdog/src/Watchdog.defs.hh | 38 +++++++++++++++++++++++++------------- 1 files changed, 25 insertions(+), 13 deletions(-) diff --git a/Watchdog/src/Watchdog.defs.hh b/Watchdog/src/Watchdog.defs.hh index 5031a98..1d68f30 100644 --- a/Watchdog/src/Watchdog.defs.hh +++ b/Watchdog/src/Watchdog.defs.hh @@ -52,28 +52,39 @@ public: template <typename Flag_Base, typename Flag> Watchdog(unsigned int units, const Flag_Base* volatile& holder, Flag& flag); + /*! \brief + Constructor: if not reset, the watchdog will trigger after \p units + hundreths of seconds, invoking handler \p function. + */ Watchdog(unsigned int units, void (*function)()); + + //! Destructor. ~Watchdog(); private: typedef Pending_List<Watchdog_Traits> WD_Pending_List; friend class Init; + + //! Static class initialization. static void initialize(); + //! Static class finalization. static void finalize(); + //! Whether or not this watchdog has expired. bool expired; + const Handler& handler; WD_Pending_List::Iterator pending_position; -private: - // Just to prevent their use. + // Private and not implemented: copy construction is not allowed. Watchdog(const Watchdog&); + // Private and not implemented: copy assignment is not allowed. Watchdog& operator=(const Watchdog&); // Pass this to getitimer(). static itimerval current_timer_status; - // Get the timer value. + //! Reads the timer value into \p time. static void get_timer(Time& time); // Pass this to setitimer(). @@ -82,13 +93,13 @@ private: // Last time value we set the timer to. static Time last_time_requested; - // Set the timer value. + //! Sets the timer value to \p time. static void set_timer(const Time& time); - // Stops the timer. + //! Stops the timer. static void stop_timer(); - // Quick reschedule to avoid race conditions. + //! Quick reschedule to avoid race conditions. static void reschedule(); // Used by the above. @@ -103,18 +114,19 @@ private: //! The actual signal handler. static void handle_timeout(int); - // Handle the addition of a new watchdog event. - static WD_Pending_List::Iterator new_watchdog_event(unsigned int units, - const Handler& handler, - bool& expired_flag); + //! Handles the addition of a new watchdog event. + static WD_Pending_List::Iterator + new_watchdog_event(unsigned int units, + const Handler& handler, + bool& expired_flag); - // Handle the removal of a watchdog event. + //! Handles the removal of the watchdog event referred by \p position. void remove_watchdog_event(WD_Pending_List::Iterator position); - // Whether the alarm clock is running. + //! Whether the alarm clock is running. static volatile bool alarm_clock_running; - // Whether we are changing data that is also changed by the signal handler. + //! Whether we are changing data that is also changed by the signal handler. static volatile bool in_critical_section; friend void PWL_handle_timeout(int signum);

1 0

[GIT] ppl/ppl(master): Added the documentation of some parameters.
by Roberto Bagnara 13 Jul '09

13 Jul '09

Module: ppl/ppl Branch: master Commit: 603691e1fc7d82330d43e3b0bdc43d74b0801f0e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=603691e1fc7d… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Jul 13 16:04:22 2009 +0200 Added the documentation of some parameters. --- src/BD_Shape.defs.hh | 4 ++++ src/Box.defs.hh | 4 ++++ src/Octagonal_Shape.defs.hh | 4 ++++ 3 files changed, 12 insertions(+), 0 deletions(-) diff --git a/src/BD_Shape.defs.hh b/src/BD_Shape.defs.hh index 2155704..477a6d3 100644 --- a/src/BD_Shape.defs.hh +++ b/src/BD_Shape.defs.hh @@ -1363,6 +1363,10 @@ public: Possibly tightens \p *this by dropping some points with non-integer coordinates for the space dimensions corresponding to \p vars. + \param vars + Points with non-integer coordinates for these variables/space-dimensions + can be discarded. + \param complexity The maximal complexity of any algorithms used. diff --git a/src/Box.defs.hh b/src/Box.defs.hh index 2981336..ff33df2 100644 --- a/src/Box.defs.hh +++ b/src/Box.defs.hh @@ -1255,6 +1255,10 @@ public: Possibly tightens \p *this by dropping some points with non-integer coordinates for the space dimensions corresponding to \p vars. + \param vars + Points with non-integer coordinates for these variables/space-dimensions + can be discarded. + \param complexity The maximal complexity of any algorithms used. diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh index 840b02f..5235902 100644 --- a/src/Octagonal_Shape.defs.hh +++ b/src/Octagonal_Shape.defs.hh @@ -1378,6 +1378,10 @@ public: Possibly tightens \p *this by dropping some points with non-integer coordinates for the space dimensions corresponding to \p vars. + \param vars + Points with non-integer coordinates for these variables/space-dimensions + can be discarded. + \param complexity The maximal complexity of any algorithms used.

1 0

[GIT] ppl/ppl(master): Doxygen reference fixed.
by Roberto Bagnara 13 Jul '09

13 Jul '09

Module: ppl/ppl Branch: master Commit: 2b5711e19f0b02703248d36416b87f227f581417 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2b5711e19f0b… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Jul 13 16:01:19 2009 +0200 Doxygen reference fixed. --- src/Affine_Space.defs.hh | 3 ++- 1 files changed, 2 insertions(+), 1 deletions(-) diff --git a/src/Affine_Space.defs.hh b/src/Affine_Space.defs.hh index 5d22ff7..23ed3ea 100644 --- a/src/Affine_Space.defs.hh +++ b/src/Affine_Space.defs.hh @@ -1597,7 +1597,8 @@ public: \p to_be_folded is a set of variables whose maximum space dimension is also less than or equal to \f$n\f$, and \p var is not a member of \p to_be_folded, then the space dimensions corresponding to - variables in \p to_be_folded are \ref Affine_Space_Fold_Space_Dimensions "folded" + variables in \p to_be_folded are + \ref Folding_Multiple_Dimensions_of_the_Vector_Space_into_One_Dimension "folded" into the \f$k\f$-th space dimension. */ void fold_space_dimensions(const Variables_Set& to_be_folded, Variable var);

1 0