Dagstuhl Seminar 08021
Numerical Validation in Current Hardware Architectures
( Jan 06 – Jan 11, 2008 )
Permalink
Organizers
- Annie Cuyt (University of Antwerp, BE)
- Walter Krämer (Bergische Universität Wuppertal, DE)
- Wolfram Luther (Universität Duisburg-Essen, DE)
- Peter Markstein (HP Labs - Palo Alto, US)
Contact
- Simone Schilke (for administrative matters)
The major emphasis of the seminar concentrated on numerical validation in current hardware architectures and software environments. The general idea was to bring together experts who are concerned with computer arithmetic in systems with actual processor architectures and scientists who develop, use and need techniques from verified computation in their applications. Topics of the seminar therefore included
- The ongoing revision of the IEEE 754/854 standard for floating-point arithmetic
- Feasible ways to implement multiple precision (multiword) arithmetic and to compute the actual precision at run-time according to the needs of input data
- The achievement of a similar behaviour of fixed-point, floating-point and interval arithmetic across language compliant implementations
- The design of robust and efficient numerical programs portable from diverse computers to those that adhere to the IEEE standard.
- The development and propagation of validated special purpose software in different application areas
- Error analysis in several contexts
- Certification of numerical programs, verification and validation assessment.
Computer arithmetic plays an important role at the hardware and software level, when microprocessors, embedded systems or grids are designed. The reliability of numerical software strongly depends on the compliance with the corresponding floating-point norms. Standard CISC processors follow the 1985 IEEE-754 Standard which is actually under revision, but the new highly performing CELL processor is not fully IEEE compliant. The draft standard IEEE 754r guarantees that “systems perform floating-point computation that yields results independent of whether the processing is done in hardware, software, or a combination of the two. For operations specified in this standard, numerical results and exceptions are uniquely determined by the values of the input data, sequence of operations, and destination formats, all under user control.” There was a broad consensus that the standard should include interval arithmetic.
The discussion focused on decimal number formats, faithful rounding, longer mantissa lengths, higher precision standard functions and linking of numerical and symbolic algebraic computation. This work is accompanied by new vector, matrix and elementary or special function libraries (i.e. complex functions and continued fractions) with guaranteed precision within their domains. Functions should be correctly rounded and even last bit accuracy is available for standard functions. Important discussion points were additional features like fast interval arithmetic, staggered correction arithmetic or a fast and accurate multiply and accumulate instruction by pipelining. The latter is the key operation for a fast multiple precision arithmetic. An exact dot product (implemented in pipelined hardware) for floating point vectors would provide operations in vector spaces with accurate results without any time penalty. Correctly rounded results in these vector spaces go hand in hand with correctly rounded elementary functions. The new norm will be based on solid and interesting theoretical studies in integrated or reconfigurable circuit design, mathematics and computer science.
In parallel to the ongoing IEEE committee discussions, the seminar aimed at highlighting design decisions on floating-point computations at runtime over the whole execution process under the silent consensus that there are features defined by the hardware standard, language defined or deferred to the implementation for several reasons.
Hardware and software should support several (user defined) number types, i.e. fixed width, binary or decimal floating-point numbers or interval arithmetic. A serious effort is actually made to standardize the use of intervals especially in the programming language C. Developers are encouraged to write efficient numerical programs that are easily portable with small revisions to other platforms. C-XSC is a C++ Library for Extended Scientific Computing to develop numerical software with result verification. This library is permanently enlarged and enhanced as highlighted in several talks.
However, depending on the requirements on speed, input and output range or precision, special purpose-processors also use other number systems, i.e. fixed-point or logarithmic number systems and non-standard mantissa length. Interesting reported examples were a 16-bit interval arithmetic on the FPGA (Field Programmable Gate Array) based NIOS-II soft processor and an online-arithmetic with rational numbers. Therefore, research on reliable computing includes a wide range of current hardware and software platforms and compilers.
Standardization is also asked for inhomogeneous computer networks. The verification step should validate the partial results coming from the owners of parcels before combining them to the final result.
Our insights and the implemented systems should be used by people with various numerical problems to solve these problems in a comprehensible and reliable way and by people incorporating validated software tools into other systems or providing interfaces to these tools.
So we want to create an increasing awareness of interval tools, the validated modeling and simulation systems and computer-based proofs in science and engineering.
- Götz Alefeld (KIT - Karlsruher Institut für Technologie, DE)
- Ekaterina Auer (Universität Duisburg-Essen, DE)
- Gerd Bohlender (KIT - Karlsruher Institut für Technologie, DE)
- Annie Cuyt (University of Antwerp, BE) [dblp]
- Gregorio de Miguel Casado (University of Zaragoza, ES)
- Tom Docx (University of Antwerp, BE)
- Eva Dyllong (Universität Duisburg-Essen, DE)
- Andreas Frommer (Bergische Universität Wuppertal, DE) [dblp]
- Markus Grimmer (Bergische Universität Wuppertal, DE)
- Werner Hofschuster (Bergische Universität Wuppertal, DE)
- Carlos Hölbig (Universidade de Passo Fundo - Brasil, BR)
- Di Jiang (University of Montréal, CA)
- Ralph Baker Kearfott (Univ. of Louisiana - Lafayette, US)
- Christian Keil (TU Hamburg-Harburg, DE)
- Michel Kieffer (INRIA Parietal - Gif-sur-Yvette, FR)
- Rudi Klatte (KIT - Karlsruher Institut für Technologie, DE)
- Walter Krämer (Bergische Universität Wuppertal, DE)
- Ulrich W. Kulisch (KIT - Karlsruher Institut für Technologie, DE)
- Jean-Luc Lamotte (UPMC - Paris, FR)
- Bruno Lang (Bergische Universität Wuppertal, DE)
- Vincent Lefèvre (ENS - Lyon, FR) [dblp]
- Rudolf Lohner (KIT - Karlsruher Institut für Technologie, DE)
- Nicolas Louvet (ENS - Lyon, FR)
- Mariana Luderitz Kolberg (PUCRS - Porto Alegre, BR)
- Wolfram Luther (Universität Duisburg-Essen, DE) [dblp]
- Peter Markstein (HP Labs - Palo Alto, US)
- Guillaume Melquiond (INRIA-MSR - Orsay, FR) [dblp]
- Jean-Michel Muller (ENS - Lyon, FR) [dblp]
- Markus Neher (KIT - Karlsruher Institut für Technologie, DE) [dblp]
- Shin'ichi Oishi (Waseda University - Tokyo, JP) [dblp]
- Evgenija D. Popova (Bulgarian Academy of Sciences, BG)
- John D. Pryce (Swindon - Wiltshire, GB) [dblp]
- Andreas Rauh (Universität Rostock, DE)
- Nathalie Revol (ENS - Lyon, FR) [dblp]
- Siegfried M. Rump (TU Hamburg-Harburg, DE) [dblp]
- Neil Stewart (Université de Montréal, CA)
- Joris van Deun (University of Antwerp, BE)
- Jürgen Wolff von Gudenberg (Universität Würzburg, DE)
- Michael Zimmer (Bergische Universität Wuppertal, DE)
- Paul Zimmermann (INRIA Lorraine - Nancy, FR) [dblp]
Classification
- hardware
- programming languages / compiler
- semantics / specification / formal methods
- interdisciplinary with non-informatics-topic own classification = Reliable algorithms
Keywords
- Computer arithmetic
- arbitrary precision
- floating-point arithmetic standardization
- language support
- reliable libraries
- high-precision special functions
- reliablealgorithms
- reliable floating-point and interval computing on different platforms