January 2005 - PPL-devel - BUGSENG Mailman

ppl/src Makefile.am
by Roberto Bagnara 27 Jan '05

27 Jan '05

CVSROOT: /cvs/ppl Module name: ppl Changes by: roberto(a)cs.unipr.it 2005-01-27 15:33:19 Modified files: src : Makefile.am Log message: Include the declaration and definition of E_NIT and E_Rational into ppl.hh. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Makefile.am.diff?cvsroot=…

1 0

w3ppl/htdocs/Documentation ppl_citations.bib
by Roberto Bagnara 27 Jan '05

27 Jan '05

CVSROOT: /cvs/ppl Module name: w3ppl Changes by: roberto(a)cs.unipr.it 2005-01-27 10:13:37 Modified files: htdocs/Documentation: ppl_citations.bib Log message: Spurious booktitle field removed. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/w3ppl/htdocs/Documentation/ppl_ci…

1 0

w3ppl/htdocs/Documentation ppl.bib
by Roberto Bagnara 27 Jan '05

27 Jan '05

CVSROOT: /cvs/ppl Module name: w3ppl Changes by: roberto(a)cs.unipr.it 2005-01-27 10:12:46 Modified files: htdocs/Documentation: ppl.bib Log message: BagnaraHZ03b improved. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/w3ppl/htdocs/Documentation/ppl.bi…

1 0

w3ppl/htdocs/Documentation ppl_citations.bib
by Roberto Bagnara 27 Jan '05

27 Jan '05

CVSROOT: /cvs/ppl Module name: w3ppl Changes by: roberto(a)cs.unipr.it 2005-01-27 10:09:35 Modified files: htdocs/Documentation: ppl_citations.bib Log message: Added SankaranarayananSM05. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/w3ppl/htdocs/Documentation/ppl_ci…

1 0

ppl/tests/Polyhedron Makefile.am memory2.cc
by Roberto Bagnara 27 Jan '05

27 Jan '05

CVSROOT: /cvs/ppl Module name: ppl Changes by: roberto(a)cs.unipr.it 2005-01-27 09:22:28 Modified files: tests/Polyhedron: Makefile.am memory2.cc Log message: Now memory2 fails only if a memory leak is detected. Check for possible memory leaks caused by any type of exception. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/tests/Polyhedron/Makefile.am.… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/tests/Polyhedron/memory2.cc.d…

1 0

w3ppl/htdocs/Documentation ppl_citations.bib
by Roberto Bagnara 27 Jan '05

27 Jan '05

CVSROOT: /cvs/ppl Module name: w3ppl Changes by: roberto(a)cs.unipr.it 2005-01-27 07:45:30 Modified files: htdocs/Documentation: ppl_citations.bib Log message: Frehse05 added. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/w3ppl/htdocs/Documentation/ppl_ci…

1 0

ppl/tests/Polyhedron Makefile.am memory2.cc
by Roberto Bagnara 27 Jan '05

27 Jan '05

CVSROOT: /cvs/ppl Module name: ppl Changes by: roberto(a)cs.unipr.it 2005-01-27 00:20:35 Modified files: tests/Polyhedron: Makefile.am memory2.cc Log message: Added much more serious tests to guard against the introduction of memory leaks. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/tests/Polyhedron/Makefile.am.… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/tests/Polyhedron/memory2.cc.d…

1 0

Re: Benchmarks for PPL 0.6.1 -> 0.7 and HSCC paper
by Roberto Bagnara 27 Jan '05

27 Jan '05

Goran Frehse wrote: > thank you for another improvement of the PPL! > This time it took me a while to upgrade, because I was a little > cautious about the necessary renaming. But in the end it wasn't a > problem at all. > So here are some results of a recompilation: > > 1) Verification of a 3-dimensional system, i.e., several 10000 > computations with 3--6-dimensional polyhedra > - PPL 0.6.1: 61.46 s user time, Max VSize = 36724KB > - PPL 0.7 : 59.24 s user time, Max VSize = 37112KB > > 2) Verification of a 4-dim. system, i.e., several 10000 computations > with 4--8-dimensional polyhedra > - PPL 0.6.1: 228.73 s user time, Max VSize = 109888KB > - PPL 0.7 : 204.39 s user time, Max VSize = 110124KB > > Again, you managed to improve the speed by more than 10% (for higher > dimensions), I'm impressed! > > Also, I've attached a paper (to appear in March) on the verification > tool that I'm developing. Using the PPL, it performs quite well > against tools that only use floating point computations -- quite > astonishing, really, and a certificate of quality for the PPL. > > In analyzing systems of higher complexity, the exact computations > quickly reach coefficients of 100000 bits or more, and hundreds of > constraints. In the paper, I'm addressing this issue with a > guaranteed overapproximation, using the linear programming algorithm > of the PPL on top of the normal polyhedral operations. For systems > where an exact computation is still possible, the gain in speed is > more than tenfold. More complex systems are simply impossible to > analyze without limiting the number of bits and constraints (see the > section in the paper on "Managing Complexity of Polyhedra"). > > In my current implementation of the algorithms limiting the number > of bits and constraints, the polyhedra are reconstructed constraint > by constraint, which is very costly, and I think there is a lot of > overhead because I have no access to the non-public methods and data > structures of the PPL. Since these methods to limit complexity have > a quite general range of applications, might it be worthwhile to > consider adopting them in the PPL? > > Again, I applaud the ongoing good work you're doing with the PPL, > and thank you for the developments. Dear Goran, thank you very much for your message. I really want to share it with all the PPL developers, since it is thanks to their hard work that the library begins to be applicable to real problems. Your encouragement gives us even more incentive to continue doing our best. I skimmed through the paper and I think it is very interesting. I have read the sections where you describe the techniques for limiting the number of bits in the coefficients and the number of constraints in polyhedra and I agree with you that these techniques ought to be added to the library. We will discuss this possibility as soon as possible While we are at papers, please help us to complete the bibliography in http://www.cs.unipr.it/ppl/Documentation/ppl_citations.bib: we miss page numbers for your former two papers and an entry for this paper you sent (BTW, I will pass it to the other developers). I have also checked the web page of PHAVer at http://www.cs.ru.nl/~goranf/. I was looking for the sources because I wanted to test the impact of some improvements we are making to the library, but could not find them. Notice that, in order to comply with the GNU General Public License (the license under which you are using the PPL) you should make the sources available. See point 3 of the GPL for the gory details. As far as I know, however, bundling the full sources with the package is, by far, the most convenient solution. All the best, and thanks again, 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

1 0

ppl/src Checked_Number.inlines.hh checked_ext. ...
by Abramo Bagnara 26 Jan '05

26 Jan '05

CVSROOT: /cvs/ppl Module name: ppl Changes by: abramo(a)cs.unipr.it 2005-01-26 19:13:05 Modified files: src : Checked_Number.inlines.hh checked_ext.inlines.hh checked_mpq.inlines.hh checked_mpz.inlines.hh Log message: Bug fixes for checked numbers I/O. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Checked_Number.inlines.hh… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/checked_ext.inlines.hh.di… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/checked_mpq.inlines.hh.di… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/checked_mpz.inlines.hh.di…

1 0

ppl/tests/Polyhedron memory2.cc
by Roberto Bagnara 26 Jan '05

26 Jan '05

CVSROOT: /cvs/ppl Module name: ppl Changes by: roberto(a)cs.unipr.it 2005-01-26 16:32:31 Modified files: tests/Polyhedron: memory2.cc Log message: Corrected and generalized. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/tests/Polyhedron/memory2.cc.d…

1 0