mirror of
https://review.haiku-os.org/buildtools
synced 2025-01-18 20:38:39 +01:00
5873a060ca
* these are dependencies for gcc 4 Graphite engine build. * CLooG 0.18.0 includes ISL 0.11.1 which is the backend that the build script enables. * PPL is needed by GCC build even if it isn't the chosen backend.
434 lines
19 KiB
Plaintext
434 lines
19 KiB
Plaintext
|
|
Authors
|
|
=======
|
|
|
|
The Parma Polyhedra Library and its documentation is being designed,
|
|
extended, written, debugged, maintained and improved by the following
|
|
people:
|
|
|
|
|
|
Core Development Team:
|
|
----------------------
|
|
|
|
Roberto Bagnara [1] (University of Parma)
|
|
Patricia M. Hill [2] (University of Leeds)
|
|
Enea Zaffanella [3] (University of Parma)
|
|
|
|
|
|
Former Members of the Core Development Team:
|
|
--------------------------------------------
|
|
|
|
Elisa Ricci (former student of the University of Parma,
|
|
one of the four students with which the PPL
|
|
project started) has been a major contributor
|
|
to the development of the PPL, up until
|
|
December 2002.
|
|
|
|
|
|
Current Contributors:
|
|
---------------------
|
|
|
|
Abramo Bagnara (Opera Unica) rewrote and generalized the
|
|
support for checked coefficients. He also
|
|
wrote the support for extended numbers and is
|
|
currently writing a new implementation of
|
|
intervals. He also helps on several other
|
|
design and implementation issues.
|
|
|
|
Fabio Bossi (student of the University of Parma)
|
|
is working on the PPL support for the approximation
|
|
of floating point computations.
|
|
|
|
Francois Galea [*] (University of Versailles) is working
|
|
at the implementation of the Parametric Integer
|
|
Programming solver.
|
|
|
|
Marco Poletti (student of the University of Bologna)
|
|
implemented the sparse matrices that are used
|
|
in the MIP and PIP solvers of the PPL; he also
|
|
did experiments on the parallelization of the
|
|
sparse matrices' computations; he is now working
|
|
on improving the PPL's memory footprint and
|
|
on other improvements to the library.
|
|
|
|
Enric Rodriguez Carbonell [4] (Technical University of Catalonia) is
|
|
working on the implementation of polynomial spaces.
|
|
|
|
Alessandro Zaccagnini [5] (University of Parma) has helped with
|
|
the efficient implementation of GCD and LCM
|
|
for checked numbers. He is now working on the
|
|
definitions of interval arithmetic operations.
|
|
Alessandro is always a very valuable source of
|
|
mathematical advice.
|
|
|
|
|
|
Past Contributors:
|
|
------------------
|
|
|
|
Roberto Amadini (student of the University of Parma)
|
|
did some work 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
|
|
based on expression templates. The objective
|
|
of this work was to check the effectiveness of
|
|
these techniques for moving computations from
|
|
run-time to compile-time.
|
|
|
|
Sara Bonini (former student of the University of Parma) is
|
|
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] (former student of the University of Leeds)
|
|
worked on the formalization and definition of
|
|
algorithms for rational grids and products
|
|
of grids and polyhedra.
|
|
|
|
Giordano Fracasso (University of Parma) wrote the initial version
|
|
of the support for native and checked integer
|
|
coefficients.
|
|
|
|
Maximiliano Marchesi (former student of the University of Parma)
|
|
helped a little to improve the documentation for
|
|
bounded differences.
|
|
|
|
Elena Mazzi (University of Parma) worked on our implementation
|
|
of bounded differences and octagons. She also
|
|
participated in the theoretical and practical
|
|
work concerning widening operators for weakly
|
|
relational domains.
|
|
|
|
David Merchat (formerly at the University of Parma) helped us
|
|
with the generation of the library's documentation
|
|
using Doxygen.
|
|
|
|
Matthew Mundell [7] (formerly at the University of Leeds) worked
|
|
on the implementation of rational grids. He has
|
|
also helped on other implementation issues.
|
|
|
|
Andrea Pescetti (University of Parma) was one of the four students
|
|
with which the PPL project started. Later, he
|
|
helped a little with the library's documentation.
|
|
|
|
Barbara Quartieri (former student of the University of Parma) worked
|
|
on our implementation of bounded differences and
|
|
octagons.
|
|
|
|
Angela Stazzone (former student of the University of Parma)
|
|
worked on the library's documentation.
|
|
|
|
Fabio Trabucchi (University of Parma) worked on a development
|
|
branch where he added serializers for all the
|
|
objects of the PPL. Support for serialization
|
|
based on Fabio's work will be available in a
|
|
future release of the library.
|
|
|
|
Claudio Trento (former student of the University of Pisa) did
|
|
a small amount of work on an experimental OCaml
|
|
interface for the PPL.
|
|
|
|
Tatiana Zolo (former student of the University of Parma) is
|
|
one of the four students with which the PPL
|
|
project started.
|
|
|
|
|
|
|
|
Thanks!
|
|
=======
|
|
|
|
|
|
People:
|
|
-------
|
|
|
|
Lucia Alessandrini (University of Parma) provided 4 hour-long
|
|
lectures on convex polyhedra for the Italian
|
|
authors. This was crucial for us to acquire
|
|
and/or refresh the notions needed for
|
|
developing the PPL library.
|
|
|
|
|
|
Frederic Besson [8] provided useful comments and observations on
|
|
the ideas (about an extrapolation operator for
|
|
convex polyhedra) sketched in a paper he
|
|
coauthored in 1999.
|
|
|
|
Tevfik Bultan [9] (University of California, Santa Barbara)
|
|
suggested us to add support for generalized
|
|
affine transfer functions. Discussions with
|
|
Tevfik have been very useful.
|
|
|
|
Manuel Carro
|
|
Jose Morales [9, 10] members of the CLIP Group [12], helped us
|
|
to produce a Ciao Prolog [13] interface for the
|
|
library. The decisive (and memorable) debugging
|
|
session took place in Parma in the afternoon of
|
|
March 10th, 2003, with the participation of
|
|
Jose Manuel Gomez.
|
|
|
|
Marco Comini [14] (University of Udine) allows us to use his
|
|
Mac OS X machine to work on portability to
|
|
that platform.
|
|
|
|
Goran Frehse [15] (VERIMAG, formerly at Carnegie Mellon University)
|
|
provided very useful feedback while he was
|
|
developing PHAVer [16]. We are working with
|
|
Goran in order to include more polyhedra
|
|
simplification facilities in the PPL.
|
|
|
|
Denis Gopan [17] (University of Wisconsin-Madison) helped us
|
|
extend the library with the "expand space
|
|
dimension" and "fold space dimensions"
|
|
operations of the library.
|
|
|
|
Martin Guy [18] gave us access to his ARM machine: without
|
|
this possibility, porting the PPL to the ARM's
|
|
ABIs would have taken ages.
|
|
|
|
Bruno Haible [19] (ILOG) made it possible (by writing the
|
|
AC_LIB_LINKFLAGS macro and explaining how
|
|
to use it) to allow the use of versions of the
|
|
GMP library installed in nonstandard places.
|
|
|
|
Bertrand Jeannet [20] (IRISA) wrote the New Polka library [21]
|
|
and made it available. We had several
|
|
interesting exchanges with Bertrand concerning
|
|
various aspects of polyhedra manipulation.
|
|
|
|
Herve Le Verge (r.i.p.) wrote and published an implementation
|
|
[22] of the Chernikova's algorithm [23] that
|
|
has set the stage for subsequent
|
|
implementation work, including our own.
|
|
|
|
Francesco Logozzo [24] (formerly at Ecole Polytechnique) helped us
|
|
straighten out some portability issues on Cygwin.
|
|
|
|
Kenneth MacKenzie [25] provided very good bug reports that allowed
|
|
us to fix several problems in the OCaml interface.
|
|
|
|
Costantino Medori [26] (University of Parma) helped us on some
|
|
mathematical aspects of the development.
|
|
|
|
Fred Mesnard [27] (University of La Reunion), the main author
|
|
of cTI [28], has worked with us on one of the
|
|
first applications of the PPL: the "cTI"
|
|
data-flow analyzer, which performs a linear
|
|
size relation analysis using a domain of
|
|
convex polyhedra. The China data-flow
|
|
analyzer [29] uses the Parma Polyhedra Library
|
|
to perform the same analysis. We have been
|
|
running China against an old version of cTI
|
|
that did not use the PPL, using it to
|
|
analyze the same Prolog programs. Since these
|
|
systems did not share a single line of code,
|
|
this gave us excellent opportunities for our
|
|
initial testing and debugging work.
|
|
|
|
Ken Mixter (then at Carnegie Mellon University) provided
|
|
useful feedback while working on an
|
|
experimental version of the Action Language
|
|
Verifier [30] based on the PPL.
|
|
|
|
Sebastian Pop [31] (now at AMD). During his work on interfacing
|
|
CLooG [32] with the PPL, Sebastian provided
|
|
valuable feedback, particularly on the C
|
|
interface to the PPL. He also suggested the
|
|
addition of new functionality such as the
|
|
"simplify using context" operation.
|
|
|
|
Thomas Reps [33] (University of Wisconsin-Madison), on several
|
|
occasions we have had interesting discussions
|
|
with him both on the PPL and on the more
|
|
general topics of static analysis and
|
|
numerical abstractions.
|
|
|
|
Mooly Sagiv [34] (Tel-Aviv University) stimulated the development
|
|
of the PPL by providing, in particular,
|
|
interesting challenges related to precision
|
|
and scalability.
|
|
|
|
Sriram Sankaranarayanan [35] (NEC Laboratories America, formerly at
|
|
Stanford University) provided very useful feedback
|
|
while developing StInG [36] and LPInv [37].
|
|
|
|
Axel Simon [38] (ENS, formerly at the University of Kent
|
|
at Canterbury) wrote some PPL 0.9
|
|
bindings [44] for the Glasgow Haskell Compiler.
|
|
|
|
Fausto Spoto [39] (University of Verona) did useful beta testing
|
|
for the Java interface. He also suggested the
|
|
addition of the <EM>hash code</EM> operations.
|
|
|
|
Basile Starynkevitch [40] (CEA LIST/DTSI/SOL). Basile is the author
|
|
of MELT [41] and suggested several improvements
|
|
to the PPL.
|
|
|
|
|
|
Pedro Vasconcelos [42] (formerly at the University of St Andrews, UK)
|
|
provided useful feedback while developing his
|
|
size and cost analyzer for Core Hume [43].
|
|
Pedro also solved a problem of Axel Simon's
|
|
PPL 0.9 bindings for the GHC and makes them
|
|
publicly available [44].
|
|
|
|
Ralf Wildenhues [45] (University of Bonn) helped us with
|
|
several issues concerning the proper use of
|
|
the Autotools.
|
|
|
|
|
|
Organizations (and People Therein):
|
|
-----------------------------------
|
|
|
|
We are grateful for the following contributions:
|
|
|
|
- AMD Developer Central [46] has donated a bi-quad core machine with
|
|
the latest AMD Opteron 2384 "Shanghai" processors and 16GB of RAM.
|
|
This machine now hosts all the PPL data and services. Many thanks
|
|
to Christophe Harle and Sebastian Pop.
|
|
|
|
- The Computing Center of the University of Parma [47] allowed us to
|
|
test the portability of the library on a variety of platforms.
|
|
Fausto Pagani was especially helpful in this respect.
|
|
|
|
- The GCC Compile Farm Project [48] managed by FSF France provided
|
|
access to a number of machines that allowed us to test and improve
|
|
the portability of the library. Special thanks go to Laurent Guerby
|
|
for his kind assistance.
|
|
|
|
- The test cluster provided by Hewlett Packard and hosted by ESIEE [49]
|
|
allowed us to complete the porting of the PPL to the IA64 and PA-RISC
|
|
architectures. Many thanks to Thibaut Varene [50] and the PA-RISC
|
|
Linux community [51] for their kind assistance.
|
|
|
|
- HiPEAC [52] sponsored the participation of Roberto Bagnara to the
|
|
Graphite Workshop [53]. This was very helpful to discuss the needs
|
|
of Graphite [54] (a framework for high-level loop optimizations on
|
|
the polyhedral model) and, more generally, of GCC [55] in terms of
|
|
numerical abstractions and how the PPL can help. Special thanks go
|
|
to Albert Cohen [57] for this sponsorship.
|
|
|
|
- INRIA [56] is supporting Abramo Bagnara from January 1st to May 31st,
|
|
2009, to work on the PPL and its development infrastructure.
|
|
Many thanks go, in particular, to Albert Cohen [57].
|
|
|
|
|
|
Some of our research work has been partly supported by the following
|
|
projects and organizations:
|
|
|
|
- University of Parma's FIL scientific research project (ex 60%)
|
|
``Pure and Applied Mathematics'';
|
|
|
|
- MURST project ``Automatic Program Certification by Abstract
|
|
Interpretation'' [58];
|
|
|
|
- MURST project ``Abstract Interpretation, Type Systems and Control-Flow
|
|
Analysis'';
|
|
|
|
- MURST project ``Automatic Aggregate- and Number-Reasoning for Computing:
|
|
from Decision Algorithms to Constraint Programming with Multisets, Sets,
|
|
and Maps'' [59];
|
|
|
|
- MURST project ``Constraint Based Verification of Reactive Systems'' [60];
|
|
|
|
- MURST project ``AIDA - Abstract Interpretation: Design and
|
|
Applications'' [61];
|
|
|
|
- PRIN project ``AIDA 2007 - Abstract Interpretation: Design and
|
|
Applications'' [62];
|
|
|
|
- Royal Society Joint project 2004/R1-EU (UK-Italy)
|
|
``Automatic Detection of Unstable Numerical Computations'';
|
|
|
|
- EPSRC (UK) project EP/C520726/1
|
|
``Numerical Domains for Software Analysis'' [63];
|
|
|
|
- Royal Society International Outgoing Short Visit 2007/R4
|
|
``Finding and Verifying the Absence of Bugs in Imperative Programs'' [64];
|
|
|
|
- EPSRC (UK) project EP/G025177/1
|
|
``Geometric Abstractions for Scalable Program Analyzers'' [64].
|
|
|
|
--------
|
|
|
|
[1] http://www.cs.unipr.it/~bagnara/
|
|
[2] http://www.comp.leeds.ac.uk/hill/
|
|
[3] http://www.cs.unipr.it/~zaffanella/
|
|
[*] http://www.prism.uvsq.fr/~fgalea/
|
|
[4] http://www.lsi.upc.edu/~erodri/
|
|
[5] http://www.math.unipr.it/~zaccagni/
|
|
[6] http://www.comp.leeds.ac.uk/katyd/
|
|
[7] http://www.mundell.ukfsn.org/
|
|
[8] http://www.irisa.fr/lande/fbesson/fbesson.html
|
|
[9] http://www.cs.ucsb.edu/~bultan/
|
|
[10] http://www.clip.dia.fi.upm.es/~boris/
|
|
[11] http://clip.dia.fi.upm.es/~jfran/
|
|
[12] http://clip.dia.fi.upm.es/
|
|
[13] http://clip.dia.fi.upm.es/Software/Ciao/
|
|
[14] http://www.dimi.uniud.it/~comini/
|
|
[15] http://www-verimag.imag.fr/~frehse/
|
|
[16] http://www-verimag.imag.fr/~frehse/phaver_web/
|
|
[17] http://www.cs.wisc.edu/~gopan/
|
|
[18] http://martinwguy.co.uk/
|
|
[19] http://www.haible.de/bruno/
|
|
[20] http://www.irisa.fr/prive/Bertrand.Jeannet/
|
|
[21] http://www.irisa.fr/prive/Bertrand.Jeannet/newpolka.html
|
|
[22] http://www.cs.unipr.it/ppl/Documentation/chernikova.c
|
|
[23] http://www.cs.unipr.it/ppl/Documentation/bibliography#LeVerge92
|
|
[24] http://research.microsoft.com/~logozzo/
|
|
[25] http://homepages.inf.ed.ac.uk/kwxm/
|
|
[26] http://www.math.unipr.it/~medori/
|
|
[27] http://www.univ-reunion.fr/~fred/
|
|
[28] http://www.cs.unipr.it/cTI/
|
|
[29] http://www.cs.unipr.it/China/
|
|
[30] http://www.cs.ucsb.edu/~bultan/composite/
|
|
[31] http://www-rocq.inria.fr/~pop/
|
|
[32] http://www.cloog.org/
|
|
[33] http://www.cs.wisc.edu/~reps/
|
|
[34] http://www.math.tau.ac.il/~msagiv/
|
|
[35] http://www.nec-labs.com/~srirams/
|
|
[36] http://theory.stanford.edu/~srirams/Software/sting.html
|
|
[37] http://theory.stanford.edu/~srirams/Software/lpinv.html
|
|
[38] http://www.di.ens.fr/~simona/
|
|
[39] http://profs.sci.univr.it/~spoto/
|
|
[40] http://www.starynkevitch.net/Basile/index_en.html
|
|
[41] http://gcc.gnu.org/wiki/MiddleEndLispTranslator
|
|
[42] http://www.ncc.up.pt/~pbv/
|
|
[43] http://www.ncc.up.pt/~pbv/cgi/cost.cgi
|
|
[44] http://www.ncc.up.pt/~pbv/research/ppl/ghc.html
|
|
[45] http://wissrech.ins.uni-bonn.de/people/wildenhues.html
|
|
[46] http://developer.amd.com/
|
|
[47] http://www.siti.unipr.it/
|
|
[48] http://gcc.gnu.org/wiki/CompileFarm
|
|
[49] http://www.esiee.fr/
|
|
[50] http://www.parisc-linux.org/~varenet/
|
|
[51] http://www.parisc-linux.org/
|
|
[52] http://www.hipeac.net/
|
|
[53] http://gcc.gnu.org/wiki/Graphite_Workshop_Nov08
|
|
[54] http://gcc.gnu.org/wiki/Graphite
|
|
[55] http://gcc.gnu.org/
|
|
[56] http://www.inria.fr/
|
|
[57] http://www-rocq.inria.fr/~acohen/
|
|
[58] http://theory.sci.univr.it/p40/
|
|
[59] http://www.cs.unipr.it/Projects/COFIN01
|
|
[60] http://www.disi.unige.it/person/DelzannoG/cover/
|
|
[61] http://www.cs.unipr.it/Projects/AIDA/
|
|
[62] http://www.cs.unipr.it/Projects/AIDA2007/
|
|
[63] http://www.comp.leeds.ac.uk/hill/chiara/WWW/linda.html
|
|
[64] http://www.comp.leeds.ac.uk/hill/chiara/WWW/projects.html
|