Module: ppl/ppl Branch: master Commit: 8da16bedab3920240eb1f25bafe9178ea53cefbe URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8da16bedab392...

Author: Enea Zaffanella zaffanella@cs.unipr.it Date: Mon Jul 13 13:02:56 2009 +0200

Added determinisitc timeout functionality to the Ocaml interface.

---

interfaces/OCaml/OCaml_interface.dox | 20 ++++++++++ interfaces/OCaml/ppl_ocaml_common.cc | 56 +++++++++++++++++++++++++++++ interfaces/OCaml/ppl_ocaml_common.defs.hh | 20 +++++++++- interfaces/OCaml/ppl_ocaml_globals.ml | 6 +++ interfaces/OCaml/ppl_ocaml_globals.mli | 6 +++ interfaces/OCaml/tests/test1.ml | 31 ++++++++++++++++ 6 files changed, 137 insertions(+), 2 deletions(-)

diff --git a/interfaces/OCaml/OCaml_interface.dox b/interfaces/OCaml/OCaml_interface.dox index 6cbb1b9..1262e94 100644 --- a/interfaces/OCaml/OCaml_interface.dox +++ b/interfaces/OCaml/OCaml_interface.dox @@ -210,6 +210,26 @@ included with all instantiations of the OCaml interfaces. Resets the timeout time so that the computation is not interrupted. An exception is thrown if the PPL Watchdog library is not enabled.

+<H2><CODE> ppl_set_deterministic_timeout weight </CODE></H2> + Computations taking exponential time will be interrupted some time + after reaching the <CODE>weight</CODE> complexity threshold. + If the computation is interrupted that way, a timeout exception + will be thrown. + An exception is immediately thrown if <CODE>hsecs</CODE> is not strictly + greater than zero, or if the PPL Watchdog library is not enabled. + <EM>NOTE:</EM> This "timeout" checking functionality is said to be + <EM>deterministic</EM> because it is not based on actual elapsed time. + Its behavior will only depend on (some of the) computations performed + in the PPL library and it will be otherwise independent from the + computation environment (CPU, operating system, compiler, etc.). + The weight mechanism is under alpha testing: client applications + should be ready to reconsider the tuning of these weight thresholds + when upgrading to newer version of the PPL. + +<H2><CODE> ppl_reset_deterministic_timeout </CODE></H2> + Resets the timeout time so that the computation is not interrupted. + An exception is thrown if the PPL Watchdog library is not enabled. + <H2><CODE> ppl_set_rounding_for_PPL </CODE></H2> Sets the FPU rounding mode so that the PPL abstractions based on floating point numbers work correctly. diff --git a/interfaces/OCaml/ppl_ocaml_common.cc b/interfaces/OCaml/ppl_ocaml_common.cc index dffe40b..3b4cce6 100644 --- a/interfaces/OCaml/ppl_ocaml_common.cc +++ b/interfaces/OCaml/ppl_ocaml_common.cc @@ -83,6 +83,12 @@ class PFunc {

Parma_Watchdog_Library::Watchdog* p_timeout_object = 0;

+typedef +Parma_Watchdog_Library::Threshold_Watcher +<Parma_Polyhedra_Library::Weightwatch_Traits> Weightwatch; + +Weightwatch* p_deterministic_timeout_object = 0; + #endif // PPL_WATCHDOG_LIBRARY_ENABLED

void @@ -96,6 +102,17 @@ reset_timeout() { #endif // PPL_WATCHDOG_LIBRARY_ENABLED }

+void +reset_deterministic_timeout() { +#ifdef PPL_WATCHDOG_LIBRARY_ENABLED + if (p_deterministic_timeout_object) { + delete p_deterministic_timeout_object; + p_deterministic_timeout_object = 0; + abandon_expensive_computations = 0; + } +#endif // PPL_WATCHDOG_LIBRARY_ENABLED +} + namespace {

inline mpz_ptr @@ -737,6 +754,11 @@ unregistered_value_p_MIP_Problem(const MIP_Problem& ph) { using namespace Parma_Polyhedra_Library; using namespace Parma_Polyhedra_Library::Interfaces::OCaml;

+#ifdef PPL_WATCHDOG_LIBRARY_ENABLED +template <> Weightwatch::Initialize +Weightwatch::init = Weightwatch::Initialize(); +#endif // PPL_WATCHDOG_LIBRARY_ENABLED + extern "C" CAMLprim value ppl_new_MIP_Problem_from_space_dimension(value d) try { @@ -1254,3 +1276,37 @@ ppl_reset_timeout(value unit) try { #endif // PPL_WATCHDOG_LIBRARY_ENABLED } CATCH_ALL + +extern "C" +CAMLprim value +ppl_set_deterministic_timeout(value weight) try { + CAMLparam1(weight); +#ifndef PPL_WATCHDOG_LIBRARY_ENABLED + const char* what = "PPL OCaml interface usage error:\n" + "ppl_set_deterministic_timeout: the PPL Watchdog library is not enabled."; + throw std::runtime_error(what); +#else + // In case a timeout was already set. + reset_deterministic_timeout(); + unsigned cpp_weight = value_to_unsigned<unsigned>(weight); + static deterministic_timeout_exception e; + p_deterministic_timeout_object + = new Weightwatch(cpp_weight, abandon_expensive_computations, e); + CAMLreturn(Val_unit); +#endif // PPL_WATCHDOG_LIBRARY_ENABLED +} +CATCH_ALL + +extern "C" +CAMLprim value +ppl_reset_deterministic_timeout(value unit) try { + CAMLparam1(unit); +#ifndef PPL_WATCHDOG_LIBRARY_ENABLED + throw std::runtime_error("PPL OCaml interface error:\n" + "the PPL Watchdog library is not enabled."); +#else + reset_deterministic_timeout(); + CAMLreturn(Val_unit); +#endif // PPL_WATCHDOG_LIBRARY_ENABLED +} +CATCH_ALL diff --git a/interfaces/OCaml/ppl_ocaml_common.defs.hh b/interfaces/OCaml/ppl_ocaml_common.defs.hh index 9b8bbe1..41b312f 100644 --- a/interfaces/OCaml/ppl_ocaml_common.defs.hh +++ b/interfaces/OCaml/ppl_ocaml_common.defs.hh @@ -158,7 +158,8 @@ private: std::vector<dimension_type> vec; };

-class timeout_exception : public Parma_Polyhedra_Library::Throwable { +class timeout_exception + : public Parma_Polyhedra_Library::Throwable { public: void throw_me() const { throw *this; @@ -166,12 +167,23 @@ public: int priority() const { return 0; } - timeout_exception() { +}; + +class deterministic_timeout_exception + : public Parma_Polyhedra_Library::Throwable { +public: + void throw_me() const { + throw *this; + } + int priority() const { + return 0; } };

void reset_timeout();

+void reset_deterministic_timeout(); + } // namespace OCaml

} // namespace Interfaces @@ -201,6 +213,10 @@ catch(timeout_exception&) { \ reset_timeout(); \ caml_raise_constant(*caml_named_value("PPL_timeout_exception")); \ } \ +catch(deterministic_timeout_exception&) { \ + reset_deterministic_timeout(); \ + caml_raise_constant(*caml_named_value("PPL_timeout_exception")); \ +} \ catch(...) { \ caml_raise_constant(*caml_named_value("PPL_unexpected_error")); \ } diff --git a/interfaces/OCaml/ppl_ocaml_globals.ml b/interfaces/OCaml/ppl_ocaml_globals.ml index bd2549e..4ebc003 100644 --- a/interfaces/OCaml/ppl_ocaml_globals.ml +++ b/interfaces/OCaml/ppl_ocaml_globals.ml @@ -170,6 +170,12 @@ int -> unit = "ppl_set_timeout" external ppl_reset_timeout: unit -> unit = "ppl_reset_timeout"

+external ppl_set_deterministic_timeout: +int -> unit = "ppl_set_deterministic_timeout" + +external ppl_reset_deterministic_timeout: +unit -> unit = "ppl_reset_deterministic_timeout" + external ppl_new_MIP_Problem_from_space_dimension: int -> mip_problem = "ppl_new_MIP_Problem_from_space_dimension"

diff --git a/interfaces/OCaml/ppl_ocaml_globals.mli b/interfaces/OCaml/ppl_ocaml_globals.mli index 3640dd5..f2bd23a 100644 --- a/interfaces/OCaml/ppl_ocaml_globals.mli +++ b/interfaces/OCaml/ppl_ocaml_globals.mli @@ -155,6 +155,12 @@ val ppl_set_timeout: val ppl_reset_timeout: unit -> unit

+val ppl_set_deterministic_timeout: + int -> unit + +val ppl_reset_deterministic_timeout: + unit -> unit + type mip_problem

val ppl_new_MIP_Problem_from_space_dimension: diff --git a/interfaces/OCaml/tests/test1.ml b/interfaces/OCaml/tests/test1.ml index 9c23116..6acb1a0 100644 --- a/interfaces/OCaml/tests/test1.ml +++ b/interfaces/OCaml/tests/test1.ml @@ -448,6 +448,37 @@ in ( | _ -> print_string_if_noisy "ppl_set_timeout test failed:\n"; print_string_if_noisy "generic exception caught.\n" + end; + begin + try + print_string_if_noisy "\nStarting ppl_reset_deterministic_timeout test:\n"; + ppl_set_deterministic_timeout 2000; + compute_timeout_hypercube 0 2; + ppl_reset_deterministic_timeout (); + print_string_if_noisy "ppl_reset_deterministic_timeout test succeeded.\n" + with + | PPL_timeout_exception -> + print_string_if_noisy "ppl_reset_deterministic_timeout test seems to be failed:\n"; + print_string_if_noisy "Unexpected PPL timeout exception caught.\n" + | _ -> + 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" + end; + begin + try + print_string_if_noisy "\nStarting ppl_set_deterministic_timeout test:\n"; + ppl_set_deterministic_timeout 2000; + compute_timeout_hypercube 0 100; + ppl_reset_deterministic_timeout (); + print_string_if_noisy "ppl_set_deterministic_timeout test seems to be failed!\n" + with + | PPL_timeout_exception -> + print_string_if_noisy "ppl_set_deterministic_timeout test succeded\n"; + print_string_if_noisy "Expected PPL timeout exception caught.\n" + | _ -> + print_string_if_noisy "ppl_set_deterministic_timeout test failed:\n"; + print_string_if_noisy "generic exception caught.\n" end );;