- PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Copyright years bumped.
by Roberto Bagnara 01 Jan '17

01 Jan '17

1 0

Rational polyhedra
by Stefan Schupp 24 Nov '16

24 Nov '16

Hi, I am using PPL for my project which is related to verification. In this context I require my computations to be exact or, if that is not possible, to be over-approximating. From what I read in the documentation, PPL ensures such an over-approximation, which is nice. I am using C_Polyhedron as my data type and currently interested in using rational arithmetic (mpq_class) in combination with that. From what I see, you can use the mpz_class type for C_Polyhedron, but not mpq_class directly. Is there a way intended to overcome this problem? In my current setup I use the double interface, but this requires conversion and most probably introduces rounding errors. Furthermore a usage question: Is there an intended way on how to compute a linear transformation of a polyhedron with a matrix? Best regards, Stefan -- Stefan Schupp M.Sc. RWTH Aachen University Computer Science Department, Informatik 2 D-52056 Aachen, Germany http://ths.rwth-aachen.de/people/stefan-schupp/ Tel.: +49 241 80 21244

2 5

[GIT] ppl/ppl(devel): Tests renamed.
by Enea Zaffanella 06 Nov '16

06 Nov '16

Module: ppl/ppl Branch: devel Commit: 90b459f699f8cc7f5d341aeb1b938e4c7cb6a551 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=90b459f699f8… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sun Nov 6 16:17:53 2016 +0100 Tests renamed. --- tests/Polyhedron/mapspacedims1.cc | 24 ++++++++++++------------ 1 files changed, 12 insertions(+), 12 deletions(-) diff --git a/tests/Polyhedron/mapspacedims1.cc b/tests/Polyhedron/mapspacedims1.cc index 129b4ad..86ab9fe 100644 --- a/tests/Polyhedron/mapspacedims1.cc +++ b/tests/Polyhedron/mapspacedims1.cc @@ -137,7 +137,7 @@ test04() { } bool -test06() { +test05() { Variable A(0); Variable B(1); @@ -167,7 +167,7 @@ test06() { } bool -test09() { +test06() { Partial_Function function; function.insert(0, 1); function.insert(1, 0); @@ -189,7 +189,7 @@ test09() { } bool -test10() { +test07() { Variable x(0); Variable y(1); Variable z(2); @@ -259,7 +259,7 @@ test10() { } bool -test11() { +test08() { Variable A(0); Variable B(1); Variable C(2); @@ -292,7 +292,7 @@ test11() { } bool -test12() { +test09() { Variable A(0); Variable B(1); @@ -325,14 +325,14 @@ BEGIN_MAIN DO_TEST(test02); DO_TEST(test03); DO_TEST(test04); - DO_TEST(test06); - DO_TEST(test09); - // test10() only fails when using C_Polyhedron and 8 bit coefficients. + DO_TEST(test05); + DO_TEST(test07); + // test07() only fails when using C_Polyhedron and 8 bit coefficients. #ifdef DERIVED_TEST - DO_TEST(test10); + DO_TEST(test07); #else - DO_TEST_F8(test10); + DO_TEST_F8(test07); #endif // !defined(DERIVED_TEST) - DO_TEST(test11); - DO_TEST(test12); + DO_TEST(test08); + DO_TEST(test09); END_MAIN

1 0

[GIT] ppl/ppl(devel): Removed tests 05, 07, 08 and 13.
by Enea Zaffanella 06 Nov '16

06 Nov '16

Module: ppl/ppl Branch: devel Commit: cefb3aef4ce31c9b8e53e43d7d7f722968d2a534 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cefb3aef4ce3… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sun Nov 6 16:13:20 2016 +0100 Removed tests 05, 07, 08 and 13. These tests were checking the behavior of map_space_dimension() beyond its own specification (the partial function given as input was *adding* space dimensions). --- tests/Polyhedron/mapspacedims1.cc | 144 ------------------------------------- 1 files changed, 0 insertions(+), 144 deletions(-) diff --git a/tests/Polyhedron/mapspacedims1.cc b/tests/Polyhedron/mapspacedims1.cc index 2ebfd8d..129b4ad 100644 --- a/tests/Polyhedron/mapspacedims1.cc +++ b/tests/Polyhedron/mapspacedims1.cc @@ -137,38 +137,6 @@ test04() { } bool -test05() { - Variable A(0); - Variable B(1); - - Partial_Function function; - function.insert(2, 0); - function.insert(3, 2); - function.insert(4, 1); - - Generator_System gs; - gs.insert(point()); - gs.insert(ray(A)); - gs.insert(ray(B)); - - C_Polyhedron ph1(gs); - - print_function(function, "*** function ***"); - print_generators(ph1, "*** ph1 ***"); - - ph1.map_space_dimensions(function); - - C_Polyhedron known_result(3, EMPTY); - known_result.add_generator(point()); - - bool ok = (ph1 == known_result); - - print_generators(ph1, "*** after ph1.map_space_dimensions(function) ***"); - - return ok; -} - -bool test06() { Variable A(0); Variable B(1); @@ -199,77 +167,6 @@ test06() { } bool -test07() { - Variable A(0); - Variable B(1); - - Partial_Function function; - function.insert(0, 1); - function.insert(1, 0); - function.insert(2, 2); - function.insert(3, 3); - - Generator_System gs; - gs.insert(point()); - gs.insert(point(A)); - gs.insert(point(2*B)); - gs.insert(point(A + 2*B)); - - C_Polyhedron ph1(gs); - - print_function(function, "*** function ***"); - print_generators(ph1, "*** ph1 ***"); - - ph1.map_space_dimensions(function); - - C_Polyhedron known_result(4, EMPTY); - known_result.add_generator(point()); - known_result.add_generator(point(B)); - known_result.add_generator(point(2*A)); - known_result.add_generator(point(2*A + B)); - - bool ok = (ph1 == known_result); - - print_generators(ph1, "*** after ph1.map_space_dimensions(function) ***"); - - return ok; -} - -bool -test08() { - Variable A(0); - Variable B(1); - - Partial_Function function; - function.insert(0, 0); - function.insert(2, 1); - function.insert(3, 2); - - Generator_System gs; - gs.insert(point()); - gs.insert(point(A)); - gs.insert(ray(B)); - gs.insert(ray(A + B)); - - C_Polyhedron ph1(gs); - - print_function(function, "*** function ***"); - print_generators(ph1, "*** ph1 ***"); - - ph1.map_space_dimensions(function); - - C_Polyhedron known_result(3, EMPTY); - known_result.add_generator(point()); - known_result.add_generator(ray(A)); - - bool ok = (ph1 == known_result); - - print_generators(ph1, "*** after ph1.map_space_dimensions(function) ***"); - - return ok; -} - -bool test09() { Partial_Function function; function.insert(0, 1); @@ -421,43 +318,6 @@ test12() { return ok; } -bool -test13() { - Variable A(0); - Variable B(1); - Variable C(2); - Variable D(3); - - Partial_Function function; - function.insert(0, 2); - function.insert(1, 3); - - Generator_System gs; - gs.insert(point()); - gs.insert(point(A)); - gs.insert(point(2*B)); - gs.insert(point(A + 2*B)); - - C_Polyhedron ph1(gs); - - print_function(function, "*** function ***"); - print_generators(ph1, "*** ph1 ***"); - - ph1.map_space_dimensions(function); - - C_Polyhedron known_result(4, EMPTY); - known_result.add_generator(point()); - known_result.add_generator(point(C)); - known_result.add_generator(point(2*D)); - known_result.add_generator(point(C + 2*D)); - - bool ok = (ph1 == known_result); - - print_generators(ph1, "*** after ph1.map_space_dimensions(function) ***"); - - return ok; -} - } // namespace BEGIN_MAIN @@ -465,10 +325,7 @@ BEGIN_MAIN DO_TEST(test02); DO_TEST(test03); DO_TEST(test04); - DO_TEST(test05); DO_TEST(test06); - DO_TEST(test07); - DO_TEST(test08); DO_TEST(test09); // test10() only fails when using C_Polyhedron and 8 bit coefficients. #ifdef DERIVED_TEST @@ -478,5 +335,4 @@ BEGIN_MAIN #endif // !defined(DERIVED_TEST) DO_TEST(test11); DO_TEST(test12); - DO_TEST(test13); END_MAIN

1 0

Thread Safety (continued)
by John Paulson 29 Oct '16

29 Oct '16

Hi Enea and Roberto, Thank you very much for all of the work you have done on threading with PPL. I have a couple of questions about the current status of the thread safety. A project I am currently working on needs to have multiple threads working simultaneously on distinct PPL objects. Is that possible with the new thread safe version? I made an implementation of my current project where I fork processes instead of using multiple threads. However, if I fork and have two processes manipulating distinct PPL objects, I do not get a speedup by a factor of two like I would expect. Is there anyway to get that type of speedup? Best, John C. Paulson

2 3

[GIT] ppl/ppl(devel): Improved thread-safety for the mechanism for abandoning expensive computations .
by Enea Zaffanella 06 Oct '16

06 Oct '16

Module: ppl/ppl Branch: devel Commit: ff54802bc0227620b61c7f840a4b51705c2b3dd0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ff54802bc022… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Oct 6 15:02:00 2016 +0200 Improved thread-safety for the mechanism for abandoning expensive computations. Added helper make_interruptible() to allow for the creation of threads executing PPL-related computations that can be interrupted. Note: it is up to the library user to do what is needed in order to propagate the exceptions from the (interrupted) worker thread to the (interrupting) master thread. See tests/Polyhedron/threadsafe2.cc for an example. Note: the mechanism is only available in the C++ interface. --- interfaces/C/ppl_c_implementation_common.cc | 19 ++++- interfaces/Java/jni/ppl_java_common.cc | 6 ++ interfaces/Java/jni/ppl_java_globals.cc | 27 ++++++ src/Makefile.am | 1 + src/globals.cc | 5 +- src/globals_defs.hh | 16 ++++- src/make_threadable.cc | 79 ++++++++++++++++++ src/make_threadable.hh | 81 ++++++++++++++++-- tests/Polyhedron/Makefile.am | 4 +- tests/Polyhedron/threadsafe2.cc | 118 +++++++++++++++++++++++++++ 10 files changed, 342 insertions(+), 14 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=ff54802b…

1 0

Thread Safety
by John Paulson 22 Sep '16

22 Sep '16

Hi Developers, I have been using PPL for a couple of years, and I have just become interested in parallelizing an application I wrote that calls it. I tried to do this (using a parallel_for loop from TBB), but I ran into varied errors at run time. I noticed that in the TODO file of the PPL distribution that it has "Make the library thread-safe" on the list. Has this been done yet? Would the lack of thread safety lead to strange run time errors? Best, John C. Paulson

3 3

[GIT] ppl/ppl(devel): Let it compile cleanly in single-thread mode.
by Enea Zaffanella 27 Aug '16

27 Aug '16

Module: ppl/ppl Branch: devel Commit: 2488d53f08997e4b525f838627337736a1437241 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2488d53f0899… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Aug 27 13:32:58 2016 +0200 Let it compile cleanly in single-thread mode. --- demos/ppl_lpsol/ppl_lpsol.c | 39 ++++++++++++++++++++++++++------------- 1 files changed, 26 insertions(+), 13 deletions(-) diff --git a/demos/ppl_lpsol/ppl_lpsol.c b/demos/ppl_lpsol/ppl_lpsol.c index f42fde1..5483c71 100644 --- a/demos/ppl_lpsol/ppl_lpsol.c +++ b/demos/ppl_lpsol/ppl_lpsol.c @@ -679,7 +679,7 @@ maybe_check_results(args_t* args, if (!check_results) return; - if (no_mip || num_integer_variables == 0) + if (no_mip || args->num_integer_variables == 0) treat_as_lp = 1; glp_set_obj_dir(glpk_lp, (maximize ? GLP_MAX : GLP_MIN)); @@ -1246,9 +1246,11 @@ process_args(void* vp) { mpz_clear(args->den_lcm); assert(args->output_file == output_file); fclose(output_file); + output_file = NULL; free(args); } +#ifdef PPL_LPSOL_MULTI_THREADED static void* thread_process_args(void* vp) { ppl_thread_initialize(); @@ -1256,6 +1258,7 @@ thread_process_args(void* vp) { ppl_thread_finalize(); return NULL; } +#endif /* defined(PPL_LPSOL_MULTI_THREADED) */ static void error_handler(enum ppl_enum_error_code code, @@ -1296,6 +1299,8 @@ glpk_message_interceptor(void* info, char* msg) { #endif /* defined(NDEBUG) */ + +#ifdef PPL_LPSOL_MULTI_THREADED static const char* get_output_name(const char* input_name) { /* FIXME: to be made platform independent. */ @@ -1327,6 +1332,7 @@ get_output_name(const char* input_name) { strcat(output_name, extension); return output_name; } +#endif /* defined(PPL_LPSOL_MULTI_THREADED) */ static void set_output_file(const char* file_name) { @@ -1337,6 +1343,8 @@ set_output_file(const char* file_name) { if (output_file == NULL) fatal("cannot open output file `%s'", output_name); #else /* !defined(PPL_LPSOL_MULTI_THREADED) */ + /* In single threaded mode, output name does not depend on input name. */ + (void) file_name; if (output_argument) { output_file = fopen(output_argument, "w"); if (output_file == NULL) @@ -1369,7 +1377,6 @@ prepare_args(const char* file_name) { set_output_file(file_name); - glpk_lp = glp_create_prob(); glp_init_mpscp(&glpk_mpscp); if (verbosity == 0) { @@ -1577,7 +1584,6 @@ prepare_args(const char* file_name) { args->saved_ru_utime = saved_ru_utime; mpz_clear(den_lcm); - glp_delete_prob(glpk_lp); return args; } @@ -1652,23 +1658,28 @@ main(int argc, char* argv[]) { #ifndef PPL_LPSOL_MULTI_THREADED - while (optind < argc) { - if (check_results) - check_results_failed = 0; - file_name = argv[optind++]; - args = prepare_args(file_name); - process_args(args); - if (check_results && check_results_failed) - break; - } + /* Initialize glpk_lp (only once). */ + glpk_lp = glp_create_prob(); + assert(optind + 1 == argc); + if (check_results) + check_results_failed = 0; + file_name = argv[optind]; + args = prepare_args(file_name); + process_args(args); + /* Finalize glpk_lp (only once). */ + glp_delete_prob(glpk_lp); #else /* defined(PPL_LPSOL_MULTI_THEADED) */ /* Span all threads (MAX_THREADS at most). */ num_threads = 0; while (optind < argc && num_threads < MAX_THREADS) { + /* Initialize glpk_lp (once per thread). */ + glpk_lp = glp_create_prob(); file_name = argv[optind++]; args = prepare_args(file_name); + /* Finalize glpk_lp (once per thread). */ + glp_delete_prob(glpk_lp); /* Closing output_file is up to thread_process_args. */ output_file = NULL; worker = &threads[num_threads++]; @@ -1694,8 +1705,10 @@ main(int argc, char* argv[]) { mpz_clear(tmp_z); /* Close output file, if any. */ - if (output_file) + if (output_file) { fclose(output_file); + output_file = NULL; + } #ifdef PPL_LPSOL_SUPPORTS_CHECK_OPTION my_exit((check_results && check_results_failed) ? 1 : 0);

1 0

[GIT] ppl/ppl(devel): Added thread-safety support to the Java interface.
by Enea Zaffanella 27 Aug '16

27 Aug '16

Module: ppl/ppl Branch: devel Commit: 57895cf11406edbc38447cdbd0adaf212fc2bb37 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=57895cf11406… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Aug 27 12:38:42 2016 +0200 Added thread-safety support to the Java interface. --- interfaces/Java/jni/ppl_java_common.cc | 76 ++++++++++---- interfaces/Java/jni/ppl_java_common_defs.hh | 40 ++++++- interfaces/Java/jni/ppl_java_common_inlines.hh | 44 ++++++++ interfaces/Java/jni/ppl_java_globals.cc | 44 ++++---- .../Parma_Polyhedra_Library.java | 31 +++++ .../Java/parma_polyhedra_library/Variable.java | 5 +- .../Java/tests/Custom_Variable_Stringifier.java | 8 +- interfaces/Java/tests/Makefile.am | 17 +++- interfaces/Java/tests/Variable_Output_test1.java | 2 +- .../Java/tests/Variable_Output_thread_safe1.java | 117 ++++++++++++++++++++ 10 files changed, 330 insertions(+), 54 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=57895cf1…

1 0

[GIT] ppl/ppl(devel): New commits
by Roberto Bagnara 25 Aug '16

25 Aug '16

URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9df657b33342… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Aug 25 18:20:00 2016 +0200 The ppl_lpsol demo program now supports thread safety. If multiple input files are given as input, each of them is processed by a separate thread. Note: the file reading phase, which used glpk, is performed by the master thread (since glpk is not thread safe). The maximum number of threads is fixed at compilation time (MAX_THREADS = 8). In multi-threaded mode the meaning of option -o is modified to specify the output *directory*. Commit partially based on previous work by Maxim Gaina. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=50b0bf678467… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Aug 25 18:16:22 2016 +0200 Added thread-safety support to the C interface. Commit mostly based on previous work by Maxim Gaina except that, as done for the C++ interface, library initialization also includes the main thread initialization. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e54f91f433a5… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Wed Aug 24 11:51:06 2016 +0200 Avoid warning (when compiling with -std=c++11). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c33bf839ea7d… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Wed Aug 24 11:29:07 2016 +0200 Got rid of deprecated std::auto_ptr. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=80790f19fb86… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Wed Aug 24 10:23:57 2016 +0200 Avoid data races on the Init counter. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=60ca8522be71… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Wed Aug 24 10:12:35 2016 +0200 Let the timing utilities be thread-safe.

1 0