August 2010 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Announce the new wrapping operator used to approximate machine arithmetic.
by Roberto Bagnara 02 Aug '10

02 Aug '10

Module: ppl/ppl Branch: master Commit: 305a923ec95aedb8c603dec6a3aff84cc340a9d3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=305a923ec95a… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Aug 2 17:21:29 2010 +0200 Announce the new wrapping operator used to approximate machine arithmetic. --- NEWS | 7 +++++++ 1 files changed, 7 insertions(+), 0 deletions(-) diff --git a/NEWS b/NEWS index 45d77e1..d9508f0 100644 --- a/NEWS +++ b/NEWS @@ -31,6 +31,13 @@ o New support for termination analysis via the automatic synthesis of of all linear quasi-ranking functions, for use in conditional termination analysis. +o New support for approximating computations involving (bounded) + machine integers. A general wrapping operator is provided that is + parametric with respect to the set of space dimensions (variables) + to be wrapped, the width, representation and overflow behavior of + all these variables. An optional constraint system can, when + given, improve the precision. + o All the PPL semantic objects provide new methods void drop_some_non_integer_points(Complexity_Class)

1 0

[GIT] ppl/w3ppl(master): Updated for the release of PPL 0.11.
by Roberto Bagnara 02 Aug '10

02 Aug '10

Module: ppl/w3ppl Branch: master Commit: c6d91184f245d060ecb3fc4e726686c0221f69ef URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=c6d91184f2… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Aug 2 17:16:37 2010 +0200 Updated for the release of PPL 0.11. --- htdocs/news.raw | 15 +++++++++++++++ htdocs/ppl.raw | 51 +++++++++++++++++++++------------------------------ 2 files changed, 36 insertions(+), 30 deletions(-) diff --git a/htdocs/news.raw b/htdocs/news.raw index a23308a..5a0b644 100644 --- a/htdocs/news.raw +++ b/htdocs/news.raw @@ -10,6 +10,21 @@ of the Parma Polyhedra Library. <TABLE> <TR> + <TD VALIGN=TOP><TT>Aug 02, 2010</TT></TD> + <TD> + PPL 0.11 has been released + + This release features a brand new Parametric Integer Programming + (PIP) problem solver, "deterministic" timeout computation + facilities, support for termination analysis via the automatic + synthesis of linear ranking functions, support for the + approximation of computations involving (bounded) machine + integers, plus a number of other new minor features and + enhancements, including some speed improvements. + </TD> +</TR> + +<TR> <TD VALIGN=TOP><TT>Jun 12, 2009</TT></TD> <TD> The PPL has now a bug tracking system diff --git a/htdocs/ppl.raw b/htdocs/ppl.raw index e6379d3..2436a7d 100644 --- a/htdocs/ppl.raw +++ b/htdocs/ppl.raw @@ -17,8 +17,11 @@ complexity/precision tradeoffs; and grids which represent regularly spaced points that satisfy a set of linear congruence relations. The library also supports finite powersets and products of (any kind of) -polyhedra and grids and a mixed integer linear programming problem -solver using an exact-arithmetic version of the simplex algorithm. +polyhedra and grids, a mixed integer linear programming problem +solver using an exact-arithmetic version of the simplex algorithm, +a parametric integer programming solver, and primitives for +the termination analysis via the automatic synthesis of +linear ranking functions. (<A HREF="details">More details</A> are available on the PPL's internal mechanisms.) @@ -48,42 +51,30 @@ version 3</A> or any later version). <TABLE> <TR> - <TD VALIGN=TOP><TT>Jun 12, 2009</TT></TD> + <TD VALIGN=TOP><TT>Aug 02, 2010</TT></TD> <TD> - The PPL has now a bug tracking system + PPL 0.11 has been released - We have finally got round to setting up a - <A - HREF="https://www.cs.unipr.it/mantis/">bug tracking system for the PPL</A>. - Users and developers are now strongly encouraged to use it - for communicating, commenting and keeping track of all PPL issues. + This release features a brand new Parametric Integer Programming + (PIP) problem solver, "deterministic" timeout computation + facilities, support for termination analysis via the automatic + synthesis of linear ranking functions, support for the + approximation of computations involving (bounded) machine + integers, plus a number of other new minor features and + enhancements, including some speed improvements. </TD> </TR> <TR> - <TD VALIGN=TOP><TT>Apr 27, 2009</TT></TD> - <TD> - Elena graduated! - - Elena Mazzi got her Laurea degree in Mathematics with a - dissertation on correct widening operators for weakly-relational - numerical abstractions. The widening operators and algorithms - described and proved correct in her thesis are the ones used in - the <CODE>BD_Shape</CODE> and <CODE>Octagonal_Shape</CODE> classes - of the PPL. - - Congratulations, Dottoressa Mazzi! - </TD> -</TR> - -<TR> - <TD VALIGN=TOP><TT>Apr 18, 2009</TT></TD> + <TD VALIGN=TOP><TT>Jun 12, 2009</TT></TD> <TD> - PPL 0.10.2 has been released + The PPL has now a bug tracking system - This is a bugfix release. See the - <A HREF="Download/ftp/releases/0.10.2/NEWS">release notes</A> - for more information. + We have finally got round to setting up a + <A + HREF="https://www.cs.unipr.it/mantis/">bug tracking system for the PPL</A>. + Users and developers are now strongly encouraged to use it + for communicating, commenting and keeping track of all PPL issues. </TD> </TR>

1 0

[GIT] ppl/w3ppl(master): Updated.
by Roberto Bagnara 02 Aug '10

02 Aug '10

Module: ppl/w3ppl Branch: master Commit: 039a677d2c28a9ef9914423c7539013b25aaead1 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=039a677d2c… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Aug 2 16:57:52 2010 +0200 Updated. --- bin/ppl_release | 17 +++++++++++------ 1 files changed, 11 insertions(+), 6 deletions(-) diff --git a/bin/ppl_release b/bin/ppl_release index 28a653b..d47acb1 100755 --- a/bin/ppl_release +++ b/bin/ppl_release @@ -4,7 +4,7 @@ # # File: ppl_release # Authors: Roberto Bagnara, Jeffrey Law, Bernd Schmidt, Mark Mitchell -# Date: 2008-11-04 +# Date: 2010-08-02 # # Contents: # Script to create a PPL release. @@ -15,12 +15,16 @@ # Notes ######################################################################## -# Here is an example Usage of this script, to create a PPL 0.8 -# release: +# Here is an example Usage of this script, to create a PPL 0.11 +# release, first create the release branch with # -# ppl_release -f -r 0.8 sources -# ppl_release -f -r 0.8 tarfiles -# ppl_release -f -r 0.8 rpmfiles +# git push origin HEAD:refs/heads/ppl-0_11-branch +# +# Then: +# +# ppl_release -f -r 0.11 sources +# ppl_release -f -r 0.11 tarfiles +# ppl_release -f -r 0.11 rpmfiles # # This script will automatically use the head of the release branch # to generate the release. @@ -180,6 +184,7 @@ build_tarfiles() { mv -f ${SOURCE_DIRECTORY}/ppl-*.tar.gz ${WORKING_DIRECTORY} mv -f ${SOURCE_DIRECTORY}/ppl-*.tar.bz2 ${WORKING_DIRECTORY} mv -f ${SOURCE_DIRECTORY}/ppl-*.zip ${WORKING_DIRECTORY} + mv -f ${SOURCE_DIRECTORY}/ppl-*.lzma ${WORKING_DIRECTORY} } # Build the RPM packages for the release.

1 0

[GIT] ppl/ppl(ppl-0_11-branch): Updated.
by Roberto Bagnara 02 Aug '10

02 Aug '10

Module: ppl/ppl Branch: ppl-0_11-branch Commit: 080b21f5f3ec77e1325544f0d72508741b8b9060 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=080b21f5f3ec… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Aug 2 16:10:14 2010 +0200 Updated. --- ChangeLog | 395 ++++++++++++++++++++++++++++++++++++++++++++++++++-- Watchdog/ChangeLog | 290 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 673 insertions(+), 12 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=080b21f5…

1 0

[GIT] ppl/ppl(master): Updated.
by Roberto Bagnara 02 Aug '10

02 Aug '10

Module: ppl/ppl Branch: master Commit: 080b21f5f3ec77e1325544f0d72508741b8b9060 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=080b21f5f3ec… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Aug 2 16:10:14 2010 +0200 Updated. --- ChangeLog | 395 ++++++++++++++++++++++++++++++++++++++++++++++++++-- Watchdog/ChangeLog | 290 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 673 insertions(+), 12 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=080b21f5…

1 0

[GIT] ppl/ppl(master): Updated.
by Roberto Bagnara 02 Aug '10

02 Aug '10

Module: ppl/ppl Branch: master Commit: 1965e10801563a96cd4171912c22306fc86eb8f9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1965e1080156… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Aug 2 15:54:38 2010 +0200 Updated. --- CREDITS | 26 +++++++++++++------------- NEWS | 2 +- TODO | 14 -------------- Watchdog/NEWS | 2 +- 4 files changed, 15 insertions(+), 29 deletions(-) diff --git a/CREDITS b/CREDITS index 6ba8c92..c797359 100644 --- a/CREDITS +++ b/CREDITS @@ -35,23 +35,10 @@ Current Contributors: intervals. He also helps on several other design and implementation issues. - Roberto Amadini (student of the University of Parma) - is working on the PPL support for the approximation - of floating point computations. - - Fabio Biselli (student of the University of Parma) - is working on the PPL support for the approximation - of floating point computations. - Fabio Bossi (student of the University of Parma) is working on the PPL support for the approximation of floating point computations. - Andrea Cimino (former student of the University of Parma) - wrote most of the mixed integer programming - solver, and also most of the Java and OCaml - interfaces. - Francois Galea [*] (University of Versailles) is working at the implementation of the Parametric Integer Programming solver. @@ -70,12 +57,20 @@ Current Contributors: Past Contributors: ------------------ + Roberto Amadini (student of the University of Parma) + did some working on the PPL support for the + approximation of floating point computations. + Irene Bacchi (former student of the University of Parma) worked on a development branch where she implemented several variants of algorithms, checking whether or not the set-union of two polyhedra is the same as their poly-hull. + Fabio Biselli (student of the University of Parma) + did some work on the PPL support for the + approximation of floating point computations. + Danilo Bonardi (former student of the University of Parma) worked on a development branch where he experimented with the use of metaprogramming techniques @@ -88,6 +83,11 @@ Past Contributors: one of the four students with which the PPL project started. + Andrea Cimino (former student of the University of Parma) + wrote most of the mixed integer programming + solver, and also most of the Java and OCaml + interfaces. + Katy Dobson [6] (University of Leeds) worked on the formalization and definition of algorithms for rational grids and products of grids and diff --git a/NEWS b/NEWS index dd7aad4..45d77e1 100644 --- a/NEWS +++ b/NEWS @@ -4,7 +4,7 @@ Parma Polyhedra Library NEWS -- history of user-visible changes -------------------------------------------------------------------------- -NEWS for version 0.11 (released on August 4, 2010) +NEWS for version 0.11 (released on August 2, 2010) -------------------------------------------------------------------------- New and Changed Features diff --git a/TODO b/TODO index 199ef0e..0023df5 100644 --- a/TODO +++ b/TODO @@ -120,17 +120,3 @@ Efficiency Issues are concerned. - Provide a better implementation of computing squares in MIP_Problem's steepest-edge to avoid big numbers. - - -Debian packaging -================ - -- Add an interface package for each Prolog as a suitable version of - that Prolog appears in Debian. Control entries for these are in - control.prologs. -- Find out if /usr/lib/pkgconfig entries are required in any packages. -- libppl-dev is very large. Consider moving the docs to libppl-doc - and the other files into libppl. -- Verify the Build-Depends and Build-Depends-Indep settings, as per - the Debian Developers Reference section 5.10.1 point 1. -- Consider renaming libppl-pwl to libpwl. diff --git a/Watchdog/NEWS b/Watchdog/NEWS index ca9d361..986b025 100644 --- a/Watchdog/NEWS +++ b/Watchdog/NEWS @@ -4,7 +4,7 @@ Parma Watchdog Library NEWS -- history of user-visible changes -------------------------------------------------------------------------- -NEWS for version 0.8 (released date to be decided) +NEWS for version 0.8 (released on August 2, 2010) -------------------------------------------------------------------------- o The new class Threshold_Watcher allows to define, generically,

1 0

[GIT] ppl/ppl(master): Updated.
by Roberto Bagnara 02 Aug '10

02 Aug '10

Module: ppl/ppl Branch: master Commit: 2f4a9852b2ccaa1de77361797008c2e82d20eb91 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2f4a9852b2cc… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Aug 2 15:26:49 2010 +0200 Updated. --- NEWS | 10 ++++++---- 1 files changed, 6 insertions(+), 4 deletions(-) diff --git a/NEWS b/NEWS index 0dfcdf6..dd7aad4 100644 --- a/NEWS +++ b/NEWS @@ -4,7 +4,7 @@ Parma Polyhedra Library NEWS -- history of user-visible changes -------------------------------------------------------------------------- -NEWS for version 0.11 (to be released on May 8, 2010) +NEWS for version 0.11 (released on August 4, 2010) -------------------------------------------------------------------------- New and Changed Features @@ -14,13 +14,13 @@ o New class PIP_Problem provides a Parametric Integer Programming (PIP) problem solver (mainly based on P. Feautrier's specification). The implementation combines a parametric dual simplex algorithm using exact arithmetic with Gomory's cut - generation. Still under beta testing. + generation. o New "deterministic" timeout computation facilities: it is now possible to set computational bounds (on the library calls taking exponential time) that do not depend on the actual elapsed time and hence are independent from the actual computation environment (CPU, - operating system, etc.). Still under beta testing. + operating system, etc.). o New support for termination analysis via the automatic synthesis of linear ranking functions. Given a sound approximation of a loop, @@ -29,7 +29,7 @@ o New support for termination analysis via the automatic synthesis of witness for termination) and to compute the space of all such functions. In addition, methods are provided to obtain the space of all linear quasi-ranking functions, for use in conditional - termination analysis. Still under beta testing. + termination analysis. o All the PPL semantic objects provide new methods @@ -85,6 +85,8 @@ o The C and Java interfaces now support timeout computation facilities. o Implementation of general (C and NNC) polyhedra speeded up. +o Implementation of the MIP solver speeded up. + o When the PPL has been configured with CPPFLAGS="-DPPL_ARM_CAN_CONTROL_FPU=1", the library initialization procedure checks that the FPU can indeed be controlled and fails if

1 0

[GIT] ppl/ppl(master): Updated.
by Roberto Bagnara 02 Aug '10

02 Aug '10

Module: ppl/ppl Branch: master Commit: ec57cb1f01a45b198dde1c3dad3d6832373b50b4 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ec57cb1f01a4… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Aug 2 15:22:26 2010 +0200 Updated. --- README | 288 +++++++++++++++++++++++++++++++++++++++++-------------- Watchdog/README | 22 +++-- 2 files changed, 227 insertions(+), 83 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=ec57cb1f…

1 0

[GIT] ppl/ppl(master): Updated.
by Roberto Bagnara 02 Aug '10

02 Aug '10

Module: ppl/ppl Branch: master Commit: c7ff1fcda7cbabf18148b9a56270d0ed8c5f4c02 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c7ff1fcda7cb… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Aug 2 15:08:37 2010 +0200 Updated. --- README.configure | 22 ++++++++++------------ 1 files changed, 10 insertions(+), 12 deletions(-) diff --git a/README.configure b/README.configure index 930514e..5a09c82 100644 --- a/README.configure +++ b/README.configure @@ -141,28 +141,26 @@ It should be noted that no version of GCC prior to 4.0.3 is known to reliably compile PPL 0.10. Here is an example of a configuration that uses the Intel C/C++ compiler -version 10.1.x. Assuming you have configured GMP with a command like +version 11.1.x. Assuming you have configured GMP with a command like - CC=icc CXX=icpc /path/to/gmp-4.2.4/configure --enable-cxx \ - --prefix=/opt/intel/cce/10.1.018 + CC=icc CXX=icpc /path/to/gmp-5.0.1/configure --enable-cxx \ + --prefix=/opt/intel/Compiler/11.1/072 \ + --libdir=/opt/intel/Compiler/11.1/072/lib/intel64 you can configure the PPL with a command like - CPPFLAGS=-D_GCC_LIMITS_H_ /path/to/ppl-x.y/configure \ - --with-cxx=icpc --with-cc=icc \ + /path/to/ppl-x.y/configure --with-cxx=icpc --with-cc=icc \ --with-cxxflags=-pch \ - --with-gmp-prefix=/opt/intel/cce/10.1.018 + --with-gmp-prefix=/opt/intel/Compiler/11.1/072 -Notice that the `CPPFLAGS=-D_GCC_LIMITS_H_' environment variable -assignment is required in order to overcome a bug in the Intel C/C++ -compiler version 10.1.x. Notice also that the `--with-cxxflags' option -is not essential here and is only included to show how extra -compiler options can be passed to the configure script. +Notice that the `--with-cxxflags' option is not essential here and is +only included to show how extra compiler options can be passed to the +configure script. As another example, here is how you can compile the PPL with Comeau C/C++ 4.3.10.1. First configure GMP with a command like - CXX=como /path/to/gmp-4.2.4/configure --enable-cxx \ + CXX=como /path/to/gmp-5.0.1/configure --enable-cxx \ --disable-shared --prefix=/opt/comeau/local Then you can configure the PPL with a command like

1 0

[GIT] ppl/ppl(master): Updated.
by Roberto Bagnara 02 Aug '10

02 Aug '10

Module: ppl/ppl Branch: master Commit: de73fc626c082d0f94f277ef634c85c82d7ae5d3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=de73fc626c08… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Aug 2 15:03:33 2010 +0200 Updated. --- demos/ppl_lcdd/ppl_lcdd.1 | 2 +- demos/ppl_lpsol/ppl_lpsol.1 | 2 +- demos/ppl_pips/ppl_pips.1 | 2 +- doc/libppl.3 | 2 +- doc/libppl_c.3 | 2 +- doc/ppl-config.1 | 2 +- 6 files changed, 6 insertions(+), 6 deletions(-) diff --git a/demos/ppl_lcdd/ppl_lcdd.1 b/demos/ppl_lcdd/ppl_lcdd.1 index f3737cb..46908ca 100644 --- a/demos/ppl_lcdd/ppl_lcdd.1 +++ b/demos/ppl_lcdd/ppl_lcdd.1 @@ -1,5 +1,5 @@ .\" DO NOT MODIFY THIS FILE! It was generated by help2man 1.36. -.TH PPL_LCDD "1" "May 2010" "ppl_lcdd 0.11" "User Commands" +.TH PPL_LCDD "1" "August 2010" "ppl_lcdd 0.11" "User Commands" .SH NAME ppl_lcdd \- a PPL-based program for vertex/facet enumeration of convex polyhedra .SH SYNOPSIS diff --git a/demos/ppl_lpsol/ppl_lpsol.1 b/demos/ppl_lpsol/ppl_lpsol.1 index db6b5fd..3c33e93 100644 --- a/demos/ppl_lpsol/ppl_lpsol.1 +++ b/demos/ppl_lpsol/ppl_lpsol.1 @@ -1,5 +1,5 @@ .\" DO NOT MODIFY THIS FILE! It was generated by help2man 1.36. -.TH PPL_LPSOL "1" "May 2010" "ppl_lpsol 0.11" "User Commands" +.TH PPL_LPSOL "1" "August 2010" "ppl_lpsol 0.11" "User Commands" .SH NAME ppl_lpsol \- a PPL-based mixed integer programming problem solver .SH SYNOPSIS diff --git a/demos/ppl_pips/ppl_pips.1 b/demos/ppl_pips/ppl_pips.1 index 6b8806b..0302609 100644 --- a/demos/ppl_pips/ppl_pips.1 +++ b/demos/ppl_pips/ppl_pips.1 @@ -1,5 +1,5 @@ .\" DO NOT MODIFY THIS FILE! It was generated by help2man 1.36. -.TH PPL_PIPS "1" "May 2010" "ppl_pips 0.11" "User Commands" +.TH PPL_PIPS "1" "August 2010" "ppl_pips 0.11" "User Commands" .SH NAME ppl_pips \- a PPL-based parametric integer programming problem solver .SH SYNOPSIS diff --git a/doc/libppl.3 b/doc/libppl.3 index 0ff3e52..f8d6432 100644 --- a/doc/libppl.3 +++ b/doc/libppl.3 @@ -1,4 +1,4 @@ -.TH libppl "3" "April 2009" "PPL 0.11" "libppl overview" +.TH libppl "3" "August 2010" "PPL 0.11" "libppl overview" .SH NAME libppl \- the C++ interface of the Parma Polyhedra Library diff --git a/doc/libppl_c.3 b/doc/libppl_c.3 index d48f19d..9e8ee1c 100644 --- a/doc/libppl_c.3 +++ b/doc/libppl_c.3 @@ -1,4 +1,4 @@ -.TH libppl_c "3" "April 2009" "PPL 0.11" "libppl_c overview" +.TH libppl_c "3" "August 2010" "PPL 0.11" "libppl_c overview" .SH NAME libppl_c \- the C interface of the Parma Polyhedra Library diff --git a/doc/ppl-config.1 b/doc/ppl-config.1 index 5e54525..2e50341 100644 --- a/doc/ppl-config.1 +++ b/doc/ppl-config.1 @@ -1,5 +1,5 @@ .\" DO NOT MODIFY THIS FILE! It was generated by help2man 1.36. -.TH PPL-CONFIG "1" "May 2010" "ppl-config 0.11" "User Commands" +.TH PPL-CONFIG "1" "August 2010" "ppl-config 0.11" "User Commands" .SH NAME ppl-config \- obtain information about an installation of the Parma Polyhedra Library .SH SYNOPSIS

1 0