July 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/w3ppl(master): Removed several spurious colons (':').
by Roberto Bagnara 25 Jul '09

25 Jul '09

Module: ppl/w3ppl Branch: master Commit: 09ff40b15530f17700d99c22805a9d18e9a3adb3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=09ff40b155… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Jul 25 15:18:56 2009 +0200 Removed several spurious colons (':'). --- htdocs/Download/Git.raw | 14 +++++++------- 1 files changed, 7 insertions(+), 7 deletions(-) diff --git a/htdocs/Download/Git.raw b/htdocs/Download/Git.raw index 3ec3b90..4ac7448 100644 --- a/htdocs/Download/Git.raw +++ b/htdocs/Download/Git.raw @@ -101,10 +101,10 @@ world via HTTP (possibly with the intermediation of a proxy), you can use the alternative commands </P> <BLOCKQUOTE> - <CODE>git clone http://www.cs.unipr.it:/git/ppl/ppl.git</CODE> + <CODE>git clone http://www.cs.unipr.it/git/ppl/ppl.git</CODE> </BLOCKQUOTE> <BLOCKQUOTE> - <CODE>git clone http://www.cs.unipr.it:/git/ppl/w3ppl.git</CODE> + <CODE>git clone http://www.cs.unipr.it/git/ppl/w3ppl.git</CODE> </BLOCKQUOTE> @@ -157,10 +157,10 @@ solve this problem first. Issue the command </P> <BLOCKQUOTE> - <CODE>git clone ssh://myusername@git.cs.unipr.it:/git/ppl/ppl.git ppl</CODE> + <CODE>git clone ssh://myusername@git.cs.unipr.it/git/ppl/ppl.git ppl</CODE> </BLOCKQUOTE> <BLOCKQUOTE> - <CODE>git clone ssh://myusername@git.cs.unipr.it:/git/ppl/w3ppl.git w3ppl</CODE> + <CODE>git clone ssh://myusername@git.cs.unipr.it/git/ppl/w3ppl.git w3ppl</CODE> </BLOCKQUOTE> <P> to clone the PPL source or the PPL web repositories, respectively. @@ -170,7 +170,7 @@ to clone the PPL source or the PPL web repositories, respectively. After the initial checkout, you can change into one of the project's directories and execute most Git commands omitting -the <CODE>ssh://myusername@git.cs.unipr.it:/git/ppl/ppl.git</CODE> argument. +the <CODE>ssh://myusername@git.cs.unipr.it/git/ppl/ppl.git</CODE> argument. For example, whenever you want to merge with the latest code changes, <CODE>cd</CODE> into your <CODE>ppl</CODE> directory and issue </P> @@ -292,7 +292,7 @@ basic CVS commands and their Git counterparts. <PRE> cvs -d ssh://myusername@git.cs.unipr.it/cvs/ppl checkout ppl | -+---> git clone ssh://myusername@git.cs.unipr.it:/git/ppl/ppl.git ++---> git clone ssh://myusername@git.cs.unipr.it/git/ppl/ppl.git </PRE> @@ -300,7 +300,7 @@ cvs -d ssh://myusername@git.cs.unipr.it/cvs/ppl checkout ppl <PRE> cvs -d ssh://myusername@git.cs.unipr.it:/cvs/ppl checkout -r products ppl | -+---> git clone ssh://myusername@git.cs.unipr.it:/git/ppl/ppl.git ++---> git clone ssh://myusername@git.cs.unipr.it/git/ppl/ppl.git git checkout -b products origin/products </PRE>

1 0

[GIT] ppl/w3ppl(master): Added PerezRS09.
by Roberto Bagnara 20 Jul '09

20 Jul '09

Module: ppl/w3ppl Branch: master Commit: 5fc29ef41ba85ef5ebe4baf355f697c694439544 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=5fc29ef41b… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Jul 20 21:57:22 2009 +0200 Added PerezRS09. --- htdocs/Documentation/ppl_citations.bib | 40 ++++++++++++++++++++++++++++++++ 1 files changed, 40 insertions(+), 0 deletions(-) diff --git a/htdocs/Documentation/ppl_citations.bib b/htdocs/Documentation/ppl_citations.bib index 52b0992..03983e9 100644 --- a/htdocs/Documentation/ppl_citations.bib +++ b/htdocs/Documentation/ppl_citations.bib @@ -1971,6 +1971,46 @@ analyser." } +@Inproceedings{PerezRS09, + Author = "J. A. {Navarro P{\'e}rez} and A. Rybalchenko and A. Singh", + Title = "Cardinality Abstraction for Declarative Networking Applications", + Booktitle = "Computer Aided Verification, + Proceedings of the 21st International Conference (CAV 2009)", + Address = "Grenoble, France", + Editor = "A. Bouajjani and O. Maler", + Publisher = "Springer", + Series = "Lecture Notes in Computer Science", + Volume = 5643, + Pages = "584--598", + Year = 2009, + ISBN = "978-3-642-02657-7", + Abstract = "Declarative Networking is a recent, viable approach to + make distributed programming easier, which is becoming + increasingly popular in systems and networking + community. It offers the programmer a declarative, + rule-based language, called P2, for writing distributed + applications in an abstract, yet expressive way. This + approach, however, imposes new challenges on analysis + and verification methods when they are applied to P2 + programs. Reasoning about P2 computations is beyond the + scope of existing tools since it requires handling of + program states defined in terms of collections of + relations, which store the application data, together + with multisets of tuples, which represent communication + events in-flight. In this paper, we propose a + cardinality abstraction technique that can be used to + analyze and verify P2 programs. It keeps track of the + size of relations (together with projections thereof) + and multisets defining P2 states, and provides an + appropriate treatment of declarative operations, e.g., + indexing, unification, variable binding, and + negation. Our cardinality abstraction-based verifier + successfully proves critical safety properties of a P2 + implementation of the Byzantine fault tolerance protocol + Zyzzyva, which is a representative and complex + declarative networking application." +} + @Techreport{Pop06, Author = "S. Pop and G.-A. Silber and A. Cohen and C. Bastoul and S. Girbal and N. Vasilache",

1 0

[GIT] ppl/w3ppl(master): Added JeannetM09.
by Roberto Bagnara 17 Jul '09

17 Jul '09

Module: ppl/w3ppl Branch: master Commit: 95045abb6a4016d2b88d7ec0cb80edef5b995740 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=95045abb6a… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jul 17 20:37:16 2009 +0200 Added JeannetM09. --- htdocs/Documentation/ppl_citations.bib | 30 ++++++++++++++++++++++++++++-- 1 files changed, 28 insertions(+), 2 deletions(-) diff --git a/htdocs/Documentation/ppl_citations.bib b/htdocs/Documentation/ppl_citations.bib index d3e8d14..52b0992 100644 --- a/htdocs/Documentation/ppl_citations.bib +++ b/htdocs/Documentation/ppl_citations.bib @@ -1181,7 +1181,7 @@ Author = "D. Gopan and T. W. Reps", Title = "Lookahead Widening", Booktitle = "Computer Aided Verification: - Proceedings of the 18th International Conference", + Proceedings of the 18th International Conference (CAV 2006)", Address = "Seattle, Washington, USA", Editor = "T. Ball and R. B. Jones", Publisher = "Springer-Verlag, Berlin", @@ -1205,7 +1205,7 @@ Author = "D. Gopan and T. W. Reps", Title = "Low-Level Library Analysis and Summarization", Booktitle = "Computer Aided Verification: - Proceedings of the 19th International Conference", + Proceedings of the 19th International Conference (CAV 2007)", Address = "Berlin, Germany", Editor = "W. Damm and H. Holger", Publisher = "Springer-Verlag, Berlin", @@ -1536,6 +1536,32 @@ techniques." } +@Inproceedings{JeannetM09, + Author = "B. Jeannet and A. Min{\'e}", + Title = "Apron: A Library of Numerical Abstract Domains for Static + Analysis", + Booktitle = "Computer Aided Verification, + Proceedings of the 21st International Conference (CAV 2009)", + Address = "Grenoble, France", + Editor = "A. Bouajjani and O. Maler", + Publisher = "Springer", + Series = "Lecture Notes in Computer Science", + Volume = 5643, + Pages = "661--667", + Year = 2009, + ISBN = "978-3-642-02657-7", + Abstract = "This article describes \textsc{Apron}, a freely + available library dedicated to the static analysis of + the numerical variables of programs by abstract + interpretation. Its goal is threefold: provide analysis + implementers with ready-to-use numerical abstractions + under a unified API, encourage the research in numerical + abstract domains by providing a platform for integration + and comparison, and provide teaching and demonstration + tools to disseminate knowledge on abstract + interpretation." +} + @Incollection{KimGR07, Author = "D. Kim and G. Gupta and S. V. Rajopadhye", Title = "On Control Signals for Multi-Dimensional Time",

1 0

[GIT] ppl/w3ppl(master): Halbwachs93 completed.
by Roberto Bagnara 17 Jul '09

17 Jul '09

Module: ppl/w3ppl Branch: master Commit: e3a5b77e3df140ebc7889f24f2d4abba0e143468 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=e3a5b77e3d… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jul 17 20:37:07 2009 +0200 Halbwachs93 completed. --- htdocs/Documentation/ppl.bib | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/htdocs/Documentation/ppl.bib b/htdocs/Documentation/ppl.bib index 3567d69..cdd3d58 100644 --- a/htdocs/Documentation/ppl.bib +++ b/htdocs/Documentation/ppl.bib @@ -1511,7 +1511,7 @@ Title = "Delay Analysis in Synchronous Programs", Pages = "333--346", Booktitle = "Computer Aided Verification: - Proceedings of the 5th International Conference", + Proceedings of the 5th International Conference (CAV'93)", Address = "Elounda, Greece", Editor = "C. Courcoubetis", Publisher = "Springer-Verlag, Berlin",

1 0

[GIT] ppl/w3ppl(master): BagnaraHZ09 updated and renamed BagnaraHZ09FMSD.
by Roberto Bagnara 17 Jul '09

17 Jul '09

Module: ppl/w3ppl Branch: master Commit: 6f04404a0804078d6db9974c9b974ff32ea6d81c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=6f04404a08… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jul 17 20:16:10 2009 +0200 BagnaraHZ09 updated and renamed BagnaraHZ09FMSD. --- htdocs/Documentation/ppl.bib | 5 +++-- 1 files changed, 3 insertions(+), 2 deletions(-) diff --git a/htdocs/Documentation/ppl.bib b/htdocs/Documentation/ppl.bib index cdf6073..3567d69 100644 --- a/htdocs/Documentation/ppl.bib +++ b/htdocs/Documentation/ppl.bib @@ -896,14 +896,15 @@ URL = "http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ09TCS.pdf" } -@Article{BagnaraHZ09, +@Article{BagnaraHZ09FMSD, Author = "R. Bagnara and P. M. Hill and E. Zaffanella", Title = "Weakly-Relational Shapes for Numeric Abstractions: Improved Algorithms and Proofs of Correctness", Journal = "Formal Methods in System Design", Publisher = "Springer-Verlag, Berlin", Year = 2009, - Note = "To appear.", + Note = "Available online at + \url{http://www.springerlink.com/content/d40842574t1r5877/}", Abstract = "Weakly-relational numeric constraints provide a compromise between complexity and expressivity that is adequate for several applications in the field of formal

1 0

[GIT] ppl/w3ppl(master): Added LimeRST09.
by Roberto Bagnara 17 Jul '09

17 Jul '09

Module: ppl/w3ppl Branch: master Commit: b0ce01d269794daf1457615b868609fe7a120ad1 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=b0ce01d269… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jul 17 20:15:51 2009 +0200 Added LimeRST09. --- htdocs/Documentation/ppl_citations.bib | 36 +++++++++++++++++++++++++++++++- 1 files changed, 35 insertions(+), 1 deletions(-) diff --git a/htdocs/Documentation/ppl_citations.bib b/htdocs/Documentation/ppl_citations.bib index 562223a..d3e8d14 100644 --- a/htdocs/Documentation/ppl_citations.bib +++ b/htdocs/Documentation/ppl_citations.bib @@ -151,10 +151,10 @@ of Systems (TACAS 2007)", Address = "Braga, Portugal", Editor = "O. Grumberg and M. Huth", - Pages = "373--388", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 4424, + Pages = "373--388", Year = 2007, ISBN = "3-540-71208-4", Abstract = "In previous work we presented a model checking procedure @@ -1701,6 +1701,40 @@ \url{http://www.irisa.fr/manifestations/2006/CSTVA06/}." } +@Inproceedings{LimeRST09, + Author = "D. Lime and O. H. Roux and C. Seidner and L.-M. Traonouez", + Title = "Romeo: A Parametric Model-Checker for {Petri} Nets + with Stopwatches", + Booktitle = "Proceedings of the 15th International Conference + Tools and Algorithms for the Construction and Analysis + of Systems (TACAS 2009)", + Address = "York, UK", + Editor = "S. Kowalewski and A. Philippou", + Publisher = "Springer-Verlag, Berlin", + Series = "Lecture Notes in Computer Science", + Volume = 5505, + Pages = "54--57", + Year = 2009, + ISBN = "978-3-642-00767-5", + Abstract = "Last time we reported on Romeo, analyses with this tool + were mostly based on translations to other tools. This + new version provides an integrated TCTL model-checker + and has gained in expressivity with the addition of + parameters. Although there exists other tools to compute + the state-space of stopwatch models, Romeo is the first + one that performs TCTL model-checking on stopwatch + models. Moreover, it is the first tool that performs + TCTL model-checking on timed parametric models. Indeed, + Romeo now features an efficient model-checking of time + Petri nets using the Uppaal DBM Library, the + model-checking of stopwatch Petri nets and parametric + stopwatch Petri nets using the Parma Polyhedra Library + and a graphical editor and simulator of these + models. Furthermore, its audience has increased leading + to several industrial contracts. This paper reports on + these recent developments of Romeo." +} + @Inproceedings{LogozzoF08, Author = "F. Logozzo and M. F{\"a}hndrich", Title = "Pentagons: A Weakly Relational Abstract Domain for the

1 0

[Fwd: Re: [ppl 0.10.2] gmp not found when compiled shared for mingw32 host (-> .dll.a)]
by Roberto Bagnara 17 Jul '09

17 Jul '09

-------- Original Message -------- Subject: Re: [PPL-devel] [ppl 0.10.2] gmp not found when compiled shared for mingw32 host (-> .dll.a) Date: 17 Jul 2009 08:36:20 +0200 From: Heiko Lechner <Heiko.Lechner(a)ruhr-uni-bochum.de> To: Roberto Bagnara <bagnara(a)cs.unipr.it> References: <4A5EEC4A.7060706(a)ruhr-uni-bochum.de> <4A5FFA47.3050702(a)cs.unipr.it> Hi! I compiled ppl with: CPPFLAGS="-fexceptions" ../ppl-0.10.2/configure\ --host=i686-pc-mingw32 --target=i686-pc-mingw32\ --prefix=/home/heiko/mw32htools\ --with-libgmp-prefix=/home/heiko/mw32htools\ It didn't recognize the shared libs, because of the .dll.a, and so didn't add "/home/heiko/mw32htools/include" to the include path . After adding the path manually it could not compile, because the linker didn't find libgmpxx (maybe because it is called libgmpxx.dll.a- could be a libtool issue?). Heiko. Roberto Bagnara schrieb: > Hello Heiko, > > generally speaking, it is not enough to set CPPFLAGS. You should rather > configure with something like > > --with-libgmpxx-prefix=/home/heiko/mw32htools > > See README.configure for more details. > All the best, > > Roberto > > P.S. Note that in the next PPL release the --with-libgmpxx-prefix will > be substituted with --with-gmp-prefix. > -- 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 0.10.2] gmp not found when compiled shared for mingw32 host (-> .dll.a)
by Heiko Lechner 17 Jul '09

17 Jul '09

Hi! I compiled gmp for mingw32: CPPFLAGS=-fexceptions ../gmp-4.3.1/configure\ --host=i686-pc-mingw32 --target=i686-pc-mingw32\ --prefix=/home/heiko/mw32htools\ --enable-cxx --disable-static --enable-shared And after that I tried to compile ppl, but it didn't find gmp. Configure does not add the include path "/home/heiko/mw32htools/include" to the flags. I guess that it is because the shared libs are named "libgmp.dll.a" and "libgmpxx.dll.a". I now added the include path via CPPFLAGS, and build fails because ld can not find -lgmpxx... I think a shared gmp is not quite a good idea... Any suggestions? TIA, Heiko.

2 1

Re: [PPL-devel] cray_pointers_2.f90
by Roberto Bagnara 17 Jul '09

17 Jul '09

Konrad Trifunovic wrote: > - the error that I get are random! Yes, that is a nightmare. I suppose > it's memory allocation problem (or probably a memory leak). All the > errors come from PPL routines. The problem is that sometimes it > crashes on 10th invokation of the dependence analyser, sometimes on > 200th. > > I would be investigating for a possible memory leak inside dependence > analyser (I hope not in PPL). Hi Konrad, we routinely test PPL with the help of Valgrind, but something may of course escape. Please let us know if you narrow down the problem to something that is likely to be a bug in PPL. All the best, 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

3 4

[GIT] ppl/ppl(master): Adjusted weight thresholds.
by Enea Zaffanella 15 Jul '09

15 Jul '09

Module: ppl/ppl Branch: master Commit: d276a484e1cb5cf8eb4eb4bf5952038c61570f9a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d276a484e1cb… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Wed Jul 15 14:04:49 2009 +0200 Adjusted weight thresholds. --- tests/Polyhedron/weightwatch1.cc | 6 +++--- 1 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/Polyhedron/weightwatch1.cc b/tests/Polyhedron/weightwatch1.cc index 292e428..571725a 100644 --- a/tests/Polyhedron/weightwatch1.cc +++ b/tests/Polyhedron/weightwatch1.cc @@ -104,7 +104,7 @@ bool test01() { print_constraints(ph, "*** ph ***"); try { - Weightwatch ww(400, too_fat); + Weightwatch ww(2500000, too_fat); // Thanks to the blind relaxation of the strict inequality constraint, // polyhedron ph is easily seen to contain an integer point. const bool contains = ph.contains_integer_point(); @@ -170,7 +170,7 @@ bool test02() { print_constraints(ph, "*** ph ***"); try { - Weightwatch ww(400, too_fat); + Weightwatch ww(2500000, too_fat); // The branch-and-bound heuristics of the MIP solver behaves badly // on this particular example, causing timeout to expire. const bool contains = ph.contains_integer_point(); @@ -207,7 +207,7 @@ bool test03() { print_constraints(ph, "*** ph ***"); try { - Weightwatch ww(400, too_fat); + Weightwatch ww(1000000000, too_fat); // Polyhedron ph is the projection of the polyehdron of test01 // onto a lower dimensional space: the performance issue of previous // test does not depend on high dimension vector space.

1 0